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	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
	bnj849.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
	bnj849.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
	bnj849.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
	bnj849.5	⊢ ( 𝜒 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) )
	bnj849.6	⊢ ( 𝜃 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
	bnj849.7	⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
	bnj849.8	⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
	bnj849.9	⊢ ( 𝜃′ ↔ [ 𝑔 / 𝑓 ] 𝜃 )
	bnj849.10	⊢ ( 𝜏 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
Assertion	bnj849	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )

Proof

Step	Hyp	Ref	Expression
1		bnj849.1	⊢ ( 𝜑 ↔ ( 𝑓 ‘ ∅ ) = pred ( 𝑋 , 𝐴 , 𝑅 ) )
2		bnj849.2	⊢ ( 𝜓 ↔ ∀ 𝑖 ∈ ω ( suc 𝑖 ∈ 𝑛 → ( 𝑓 ‘ suc 𝑖 ) = ∪ 𝑦 ∈ ( 𝑓 ‘ 𝑖 ) pred ( 𝑦 , 𝐴 , 𝑅 ) ) )
3		bnj849.3	⊢ 𝐷 = ( ω ∖ { ∅ } )
4		bnj849.4	⊢ 𝐵 = { 𝑓 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) }
5		bnj849.5	⊢ ( 𝜒 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) )
6		bnj849.6	⊢ ( 𝜃 ↔ ( 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓 ) )
7		bnj849.7	⊢ ( 𝜑′ ↔ [ 𝑔 / 𝑓 ] 𝜑 )
8		bnj849.8	⊢ ( 𝜓′ ↔ [ 𝑔 / 𝑓 ] 𝜓 )
9		bnj849.9	⊢ ( 𝜃′ ↔ [ 𝑔 / 𝑓 ] 𝜃 )
10		bnj849.10	⊢ ( 𝜏 ↔ ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) )
11	1 2 3 5 6	bnj865	⊢ ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 )
12	4 7 8	bnj873	⊢ 𝐵 = { 𝑔 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) }
13		df-rex	⊢ ( ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ↔ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) )
14		19.29	⊢ ( ( ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → ∃ 𝑛 ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) )
15		an12	⊢ ( ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) ↔ ( 𝑛 ∈ 𝐷 ∧ ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) )
16		df-3an	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) )
17	10	anbi1i	⊢ ( ( 𝜏 ∧ 𝑛 ∈ 𝐷 ) ↔ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) ∧ 𝑛 ∈ 𝐷 ) )
18	16 5 17	3bitr4i	⊢ ( 𝜒 ↔ ( 𝜏 ∧ 𝑛 ∈ 𝐷 ) )
19		id	⊢ ( 𝜒 → 𝜒 )
20	6 7 8 9	bnj581	⊢ ( 𝜃′ ↔ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
21	9 20	bitr3i	⊢ ( [ 𝑔 / 𝑓 ] 𝜃 ↔ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) )
22	1 2 3 5 6	bnj864	⊢ ( 𝜒 → ∃! 𝑓 𝜃 )
23		df-rex	⊢ ( ∃ 𝑓 ∈ 𝑤 𝜃 ↔ ∃ 𝑓 ( 𝑓 ∈ 𝑤 ∧ 𝜃 ) )
24		exancom	⊢ ( ∃ 𝑓 ( 𝑓 ∈ 𝑤 ∧ 𝜃 ) ↔ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) )
25	23 24	sylbb	⊢ ( ∃ 𝑓 ∈ 𝑤 𝜃 → ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) )
26		nfeu1	⊢ Ⅎ 𝑓 ∃! 𝑓 𝜃
27		nfe1	⊢ Ⅎ 𝑓 ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 )
28	26 27	nfan	⊢ Ⅎ 𝑓 ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) )
29		nfsbc1v	⊢ Ⅎ 𝑓 [ 𝑔 / 𝑓 ] 𝜃
30		nfv	⊢ Ⅎ 𝑓 𝑔 ∈ 𝑤
31	29 30	nfim	⊢ Ⅎ 𝑓 ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 )
32	28 31	nfim	⊢ Ⅎ 𝑓 ( ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) ) → ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 ) )
33		sbceq1a	⊢ ( 𝑓 = 𝑔 → ( 𝜃 ↔ [ 𝑔 / 𝑓 ] 𝜃 ) )
34		elequ1	⊢ ( 𝑓 = 𝑔 → ( 𝑓 ∈ 𝑤 ↔ 𝑔 ∈ 𝑤 ) )
35	33 34	imbi12d	⊢ ( 𝑓 = 𝑔 → ( ( 𝜃 → 𝑓 ∈ 𝑤 ) ↔ ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 ) ) )
36	35	imbi2d	⊢ ( 𝑓 = 𝑔 → ( ( ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) ) → ( 𝜃 → 𝑓 ∈ 𝑤 ) ) ↔ ( ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) ) → ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 ) ) ) )
37		eupick	⊢ ( ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) ) → ( 𝜃 → 𝑓 ∈ 𝑤 ) )
38	32 36 37	chvarfv	⊢ ( ( ∃! 𝑓 𝜃 ∧ ∃ 𝑓 ( 𝜃 ∧ 𝑓 ∈ 𝑤 ) ) → ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 ) )
39	22 25 38	syl2an	⊢ ( ( 𝜒 ∧ ∃ 𝑓 ∈ 𝑤 𝜃 ) → ( [ 𝑔 / 𝑓 ] 𝜃 → 𝑔 ∈ 𝑤 ) )
40	21 39	biimtrrid	⊢ ( ( 𝜒 ∧ ∃ 𝑓 ∈ 𝑤 𝜃 ) → ( ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) → 𝑔 ∈ 𝑤 ) )
41	40	ex	⊢ ( 𝜒 → ( ∃ 𝑓 ∈ 𝑤 𝜃 → ( ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) → 𝑔 ∈ 𝑤 ) ) )
42	19 41	embantd	⊢ ( 𝜒 → ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) → ( ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) → 𝑔 ∈ 𝑤 ) ) )
43	42	impd	⊢ ( 𝜒 → ( ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑔 ∈ 𝑤 ) )
44	18 43	sylbir	⊢ ( ( 𝜏 ∧ 𝑛 ∈ 𝐷 ) → ( ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑔 ∈ 𝑤 ) )
45	44	expimpd	⊢ ( 𝜏 → ( ( 𝑛 ∈ 𝐷 ∧ ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
46	15 45	biimtrid	⊢ ( 𝜏 → ( ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
47	46	exlimdv	⊢ ( 𝜏 → ( ∃ 𝑛 ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
48	14 47	syl5	⊢ ( 𝜏 → ( ( ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
49	48	expdimp	⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑔 ∈ 𝑤 ) )
50	13 49	biimtrid	⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → ( ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) → 𝑔 ∈ 𝑤 ) )
51	50	abssdv	⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → { 𝑔 ∣ ∃ 𝑛 ∈ 𝐷 ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) } ⊆ 𝑤 )
52	12 51	eqsstrid	⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → 𝐵 ⊆ 𝑤 )
53		vex	⊢ 𝑤 ∈ V
54	53	ssex	⊢ ( 𝐵 ⊆ 𝑤 → 𝐵 ∈ V )
55	52 54	syl	⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → 𝐵 ∈ V )
56	55	ex	⊢ ( 𝜏 → ( ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) → 𝐵 ∈ V ) )
57	56	exlimdv	⊢ ( 𝜏 → ( ∃ 𝑤 ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) → 𝐵 ∈ V ) )
58	11 57	mpi	⊢ ( 𝜏 → 𝐵 ∈ V )
59	10 58	sylbir	⊢ ( ( 𝑅 FrSe 𝐴 ∧ 𝑋 ∈ 𝐴 ) → 𝐵 ∈ V )