Metamath Proof Explorer

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 syl5bir ⊢ ( ( 𝜒 ∧ ∃ 𝑓 ∈ 𝑤 𝜃 ) → ( ( 𝑔 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 syl5bi ⊢ ( 𝜏 → ( ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
47 46 exlimdv ⊢ ( 𝜏 → ( ∃ 𝑛 ( ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
48 14 47 syl5 ⊢ ( 𝜏 → ( ( ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ∧ ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) ) → 𝑔 ∈ 𝑤 ) )
49 48 expdimp ⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → ( ∃ 𝑛 ( 𝑛 ∈ 𝐷 ∧ ( 𝑔 Fn 𝑛 ∧ 𝜑′ ∧ 𝜓′ ) ) → 𝑔 ∈ 𝑤 ) )
50 13 49 syl5bi ⊢ ( ( 𝜏 ∧ ∀ 𝑛 ( 𝜒 → ∃ 𝑓 ∈ 𝑤 𝜃 ) ) → ( ∃ 𝑛 ∈ 𝐷 ( 𝑔 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 )