Theorem 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	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
	bnj849.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
	bnj849.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
	bnj849.4	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
	bnj849.5	$$⊢\chi \leftrightarrow \left(RFrSeA\wedge X\in A\wedge n\in D\right)$$
	bnj849.6	$$⊢\theta \leftrightarrow \left(fFnn\wedge \phi \wedge \psi \right)$$
	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	$$⊢\tau \leftrightarrow \left(RFrSeA\wedge X\in A\right)$$
Assertion	bnj849	$$⊢\left(RFrSeA\wedge X\in A\right)\to B\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		bnj849.1	$$⊢\phi \leftrightarrow f\left(\varnothing \right)=pred\left(X,A,R\right)$$
2		bnj849.2	$$⊢\psi \leftrightarrow \forall i\in \mathrm{\omega }\left(\mathrm{suc}i\in n\to f\left(\mathrm{suc}i\right)=\bigcup _{y\in f\left(i\right)}pred\left(y,A,R\right)\right)$$
3		bnj849.3	$$⊢D=\mathrm{\omega }\setminus \left\{\varnothing \right\}$$
4		bnj849.4	$$⊢B=\left\{f|\exists n\in D\left(fFnn\wedge \phi \wedge \psi \right)\right\}$$
5		bnj849.5	$$⊢\chi \leftrightarrow \left(RFrSeA\wedge X\in A\wedge n\in D\right)$$
6		bnj849.6	$$⊢\theta \leftrightarrow \left(fFnn\wedge \phi \wedge \psi \right)$$
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	$$⊢\tau \leftrightarrow \left(RFrSeA\wedge X\in A\right)$$
11	1 2 3 5 6	bnj865	$$⊢\exists w\forall n\left(\chi \to \exists f\in w\theta \right)$$
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	$$⊢\left(RFrSeA\wedge X\in A\wedge n\in D\right)\leftrightarrow \left(\left(RFrSeA\wedge X\in A\right)\wedge n\in D\right)$$
17	10	anbi1i	$$⊢\left(\tau \wedge n\in D\right)\leftrightarrow \left(\left(RFrSeA\wedge X\in A\right)\wedge n\in D\right)$$
18	16 5 17	3bitr4i	$$⊢\chi \leftrightarrow \left(\tau \wedge n\in D\right)$$
19		id	$$⊢\chi \to \chi$$
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	$$⊢\chi \to \exists !f\theta$$
23		df-rex	$$⊢\exists f\in w\theta \leftrightarrow \exists f\left(f\in w\wedge \theta \right)$$
24		exancom	$$⊢\exists f\left(f\in w\wedge \theta \right)\leftrightarrow \exists f\left(\theta \wedge f\in w\right)$$
25	23 24	sylbb	$$⊢\exists f\in w\theta \to \exists f\left(\theta \wedge f\in w\right)$$
26		nfeu1	$$⊢Ⅎf\exists !f\theta$$
27		nfe1	$$⊢Ⅎf\exists f\left(\theta \wedge f\in w\right)$$
28	26 27	nfan	$$⊢Ⅎf\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)$$
29		nfsbc1v	$$⊢Ⅎf\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta$$
30		nfv	$$⊢Ⅎfg\in w$$
31	29 30	nfim	$$⊢Ⅎf\left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)$$
32	28 31	nfim	$$⊢Ⅎf\left(\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)\to \left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)\right)$$
33		sbceq1a	$$⊢f=g\to \left(\theta \leftrightarrow \underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \right)$$
34		elequ1	$$⊢f=g\to \left(f\in w\leftrightarrow g\in w\right)$$
35	33 34	imbi12d	$$⊢f=g\to \left(\left(\theta \to f\in w\right)\leftrightarrow \left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)\right)$$
36	35	imbi2d	$$⊢f=g\to \left(\left(\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)\to \left(\theta \to f\in w\right)\right)\leftrightarrow \left(\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)\to \left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)\right)\right)$$
37		eupick	$$⊢\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)\to \left(\theta \to f\in w\right)$$
38	32 36 37	chvarfv	$$⊢\left(\exists !f\theta \wedge \exists f\left(\theta \wedge f\in w\right)\right)\to \left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)$$
39	22 25 38	syl2an	$$⊢\left(\chi \wedge \exists f\in w\theta \right)\to \left(\underset{\dot{}}{[}g/f\underset{\dot{}}{]}\theta \to g\in w\right)$$
40	21 39	syl5bir	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	syl5bi	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	syl5bi	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	$$⊢\left(\tau \wedge \forall n\left(\chi \to \exists f\in w\theta \right)\right)\to B\subseteq w$$
53		vex	$$⊢w\in \mathrm{V}$$
54	53	ssex	$$⊢B\subseteq w\to B\in \mathrm{V}$$
55	52 54	syl	$$⊢\left(\tau \wedge \forall n\left(\chi \to \exists f\in w\theta \right)\right)\to B\in \mathrm{V}$$
56	55	ex	$$⊢\tau \to \left(\forall n\left(\chi \to \exists f\in w\theta \right)\to B\in \mathrm{V}\right)$$
57	56	exlimdv	$$⊢\tau \to \left(\exists w\forall n\left(\chi \to \exists f\in w\theta \right)\to B\in \mathrm{V}\right)$$
58	11 57	mpi	$$⊢\tau \to B\in \mathrm{V}$$
59	10 58	sylbir	$$⊢\left(RFrSeA\wedge X\in A\right)\to B\in \mathrm{V}$$