bnj849

Description: Technical lemma for bnj69 . This lemma may no longer be used or have become an indirect lemma of the theorem in question (i.e. a lemma of a lemma... of the theorem). (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (Proof shortened by Mario Carneiro, 22-Dec-2016) (New usage is discouraged.)

	Ref	Expression
Hypotheses	bnj849.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
	bnj849.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
	bnj849.3	$⊢ D = ω ∖ \{\emptyset\}$
	bnj849.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
	bnj849.5	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
	bnj849.6	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
	bnj849.7	No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
	bnj849.8	No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
	bnj849.9	No typesetting found for \|- ( th' <-> [. g / f ]. th ) with typecode \|-
	bnj849.10	$⊢ τ \leftrightarrow (R FrSe A \land X \in A)$
Assertion	bnj849	$⊢ (R FrSe A \land X \in A) \to B \in V$

Proof

Step	Hyp	Ref	Expression
1		bnj849.1	$⊢ φ \leftrightarrow f (\emptyset) = pred (X, A, R)$
2		bnj849.2	$⊢ ψ \leftrightarrow \forall i \in ω (suc i \in n \to f (suc i) = ⋃_{y \in f (i)} pred (y, A, R))$
3		bnj849.3	$⊢ D = ω ∖ \{\emptyset\}$
4		bnj849.4	$⊢ B = \{f \| \exists n \in D (f Fn n \land φ \land ψ)\}$
5		bnj849.5	$⊢ χ \leftrightarrow (R FrSe A \land X \in A \land n \in D)$
6		bnj849.6	$⊢ θ \leftrightarrow (f Fn n \land φ \land ψ)$
7		bnj849.7	Could not format ( ph' <-> [. g / f ]. ph ) : No typesetting found for \|- ( ph' <-> [. g / f ]. ph ) with typecode \|-
8		bnj849.8	Could not format ( ps' <-> [. g / f ]. ps ) : No typesetting found for \|- ( ps' <-> [. g / f ]. ps ) with typecode \|-
9		bnj849.9	Could not format ( th' <-> [. g / f ]. th ) : No typesetting found for \|- ( th' <-> [. g / f ]. th ) with typecode \|-
10		bnj849.10	$⊢ τ \leftrightarrow (R FrSe A \land X \in A)$
11	1 2 3 5 6	bnj865	$⊢ \exists w \forall n (χ \to \exists f \in w θ)$
12	4 7 8	bnj873	Could not format B = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } : No typesetting found for \|- B = { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } with typecode \|-
13		df-rex	Could not format ( E. n e. D ( g Fn n /\ ph' /\ ps' ) <-> E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) : No typesetting found for \|- ( E. n e. D ( g Fn n /\ ph' /\ ps' ) <-> E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) with typecode \|-
14		19.29	Could not format ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) ) : No typesetting found for \|- ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) ) with typecode \|-
15		an12	Could not format ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) <-> ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) ) : No typesetting found for \|- ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) <-> ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) ) with typecode \|-
16		df-3an	$⊢ (R FrSe A \land X \in A \land n \in D) \leftrightarrow ((R FrSe A \land X \in A) \land n \in D)$
17	10	anbi1i	$⊢ (τ \land n \in D) \leftrightarrow ((R FrSe A \land X \in A) \land n \in D)$
18	16 5 17	3bitr4i	$⊢ χ \leftrightarrow (τ \land n \in D)$
19		id	$⊢ χ \to χ$
20	6 7 8 9	bnj581	Could not format ( th' <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( th' <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode \|-
21	9 20	bitr3i	Could not format ( [. g / f ]. th <-> ( g Fn n /\ ph' /\ ps' ) ) : No typesetting found for \|- ( [. g / f ]. th <-> ( g Fn n /\ ph' /\ ps' ) ) with typecode \|-
22	1 2 3 5 6	bnj864	$⊢ χ \to \exists! f θ$
23		df-rex	$⊢ \exists f \in w θ \leftrightarrow \exists f (f \in w \land θ)$
24		exancom	$⊢ \exists f (f \in w \land θ) \leftrightarrow \exists f (θ \land f \in w)$
25	23 24	sylbb	$⊢ \exists f \in w θ \to \exists f (θ \land f \in w)$
26		nfeu1	$⊢ Ⅎ f \exists! f θ$
27		nfe1	$⊢ Ⅎ f \exists f (θ \land f \in w)$
28	26 27	nfan	$⊢ Ⅎ f (\exists! f θ \land \exists f (θ \land f \in w))$
29		nfsbc1v	$⊢ Ⅎ f \underset{˙}{[} g / f \underset{˙}{]} θ$
30		nfv	$⊢ Ⅎ f g \in w$
31	29 30	nfim	$⊢ Ⅎ f (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w)$
32	28 31	nfim	$⊢ Ⅎ f ((\exists! f θ \land \exists f (θ \land f \in w)) \to (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w))$
33		sbceq1a	$⊢ f = g \to (θ \leftrightarrow \underset{˙}{[} g / f \underset{˙}{]} θ)$
34		elequ1	$⊢ f = g \to (f \in w \leftrightarrow g \in w)$
35	33 34	imbi12d	$⊢ f = g \to ((θ \to f \in w) \leftrightarrow (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w))$
36	35	imbi2d	$⊢ f = g \to (((\exists! f θ \land \exists f (θ \land f \in w)) \to (θ \to f \in w)) \leftrightarrow ((\exists! f θ \land \exists f (θ \land f \in w)) \to (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w)))$
37		eupick	$⊢ (\exists! f θ \land \exists f (θ \land f \in w)) \to (θ \to f \in w)$
38	32 36 37	chvarfv	$⊢ (\exists! f θ \land \exists f (θ \land f \in w)) \to (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w)$
39	22 25 38	syl2an	$⊢ (χ \land \exists f \in w θ) \to (\underset{˙}{[} g / f \underset{˙}{]} θ \to g \in w)$
40	21 39	biimtrrid	Could not format ( ( ch /\ E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) : No typesetting found for \|- ( ( ch /\ E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) with typecode \|-
41	40	ex	Could not format ( ch -> ( E. f e. w th -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) ) : No typesetting found for \|- ( ch -> ( E. f e. w th -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) ) with typecode \|-
42	19 41	embantd	Could not format ( ch -> ( ( ch -> E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) ) : No typesetting found for \|- ( ch -> ( ( ch -> E. f e. w th ) -> ( ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) ) with typecode \|-
43	42	impd	Could not format ( ch -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) : No typesetting found for \|- ( ch -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) with typecode \|-
44	18 43	sylbir	Could not format ( ( ta /\ n e. D ) -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) : No typesetting found for \|- ( ( ta /\ n e. D ) -> ( ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) with typecode \|-
45	44	expimpd	Could not format ( ta -> ( ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) : No typesetting found for \|- ( ta -> ( ( n e. D /\ ( ( ch -> E. f e. w th ) /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) with typecode \|-
46	15 45	biimtrid	Could not format ( ta -> ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) : No typesetting found for \|- ( ta -> ( ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) with typecode \|-
47	46	exlimdv	Could not format ( ta -> ( E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) : No typesetting found for \|- ( ta -> ( E. n ( ( ch -> E. f e. w th ) /\ ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) with typecode \|-
48	14 47	syl5	Could not format ( ta -> ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) : No typesetting found for \|- ( ta -> ( ( A. n ( ch -> E. f e. w th ) /\ E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) ) -> g e. w ) ) with typecode \|-
49	48	expdimp	Could not format ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) : No typesetting found for \|- ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n ( n e. D /\ ( g Fn n /\ ph' /\ ps' ) ) -> g e. w ) ) with typecode \|-
50	13 49	biimtrid	Could not format ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n e. D ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) : No typesetting found for \|- ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> ( E. n e. D ( g Fn n /\ ph' /\ ps' ) -> g e. w ) ) with typecode \|-
51	50	abssdv	Could not format ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } C_ w ) : No typesetting found for \|- ( ( ta /\ A. n ( ch -> E. f e. w th ) ) -> { g \| E. n e. D ( g Fn n /\ ph' /\ ps' ) } C_ w ) with typecode \|-
52	12 51	eqsstrid	$⊢ (τ \land \forall n (χ \to \exists f \in w θ)) \to B \subseteq w$
53		vex	$⊢ w \in V$
54	53	ssex	$⊢ B \subseteq w \to B \in V$
55	52 54	syl	$⊢ (τ \land \forall n (χ \to \exists f \in w θ)) \to B \in V$
56	55	ex	$⊢ τ \to (\forall n (χ \to \exists f \in w θ) \to B \in V)$
57	56	exlimdv	$⊢ τ \to (\exists w \forall n (χ \to \exists f \in w θ) \to B \in V)$
58	11 57	mpi	$⊢ τ \to B \in V$
59	10 58	sylbir	$⊢ (R FrSe A \land X \in A) \to B \in V$

Metamath Proof Explorer

Theorem bnj849

Proof