Metamath Proof Explorer


Theorem axcclem

Description: Lemma for axcc . (Contributed by Mario Carneiro, 2-Feb-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axcclem.1 𝐴 = ( 𝑥 ∖ { ∅ } )
axcclem.2 𝐹 = ( 𝑛 ∈ ω , 𝑦 𝐴 ↦ ( 𝑓𝑛 ) )
axcclem.3 𝐺 = ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) )
Assertion axcclem ( 𝑥 ≈ ω → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )

Proof

Step Hyp Ref Expression
1 axcclem.1 𝐴 = ( 𝑥 ∖ { ∅ } )
2 axcclem.2 𝐹 = ( 𝑛 ∈ ω , 𝑦 𝐴 ↦ ( 𝑓𝑛 ) )
3 axcclem.3 𝐺 = ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) )
4 isfinite2 ( 𝐴 ≺ ω → 𝐴 ∈ Fin )
5 1 eleq1i ( 𝐴 ∈ Fin ↔ ( 𝑥 ∖ { ∅ } ) ∈ Fin )
6 undif1 ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) = ( 𝑥 ∪ { ∅ } )
7 snfi { ∅ } ∈ Fin
8 unfi ( ( ( 𝑥 ∖ { ∅ } ) ∈ Fin ∧ { ∅ } ∈ Fin ) → ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin )
9 7 8 mpan2 ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → ( ( 𝑥 ∖ { ∅ } ) ∪ { ∅ } ) ∈ Fin )
10 6 9 eqeltrrid ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → ( 𝑥 ∪ { ∅ } ) ∈ Fin )
11 ssun1 𝑥 ⊆ ( 𝑥 ∪ { ∅ } )
12 ssfi ( ( ( 𝑥 ∪ { ∅ } ) ∈ Fin ∧ 𝑥 ⊆ ( 𝑥 ∪ { ∅ } ) ) → 𝑥 ∈ Fin )
13 10 11 12 sylancl ( ( 𝑥 ∖ { ∅ } ) ∈ Fin → 𝑥 ∈ Fin )
14 5 13 sylbi ( 𝐴 ∈ Fin → 𝑥 ∈ Fin )
15 dcomex ω ∈ V
16 isfiniteg ( ω ∈ V → ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω ) )
17 15 16 ax-mp ( 𝑥 ∈ Fin ↔ 𝑥 ≺ ω )
18 sdomnen ( 𝑥 ≺ ω → ¬ 𝑥 ≈ ω )
19 17 18 sylbi ( 𝑥 ∈ Fin → ¬ 𝑥 ≈ ω )
20 4 14 19 3syl ( 𝐴 ≺ ω → ¬ 𝑥 ≈ ω )
21 20 con2i ( 𝑥 ≈ ω → ¬ 𝐴 ≺ ω )
22 sdomentr ( ( 𝐴𝑥𝑥 ≈ ω ) → 𝐴 ≺ ω )
23 22 expcom ( 𝑥 ≈ ω → ( 𝐴𝑥𝐴 ≺ ω ) )
24 21 23 mtod ( 𝑥 ≈ ω → ¬ 𝐴𝑥 )
25 vex 𝑥 ∈ V
26 difss ( 𝑥 ∖ { ∅ } ) ⊆ 𝑥
27 1 26 eqsstri 𝐴𝑥
28 ssdomg ( 𝑥 ∈ V → ( 𝐴𝑥𝐴𝑥 ) )
29 25 27 28 mp2 𝐴𝑥
30 24 29 jctil ( 𝑥 ≈ ω → ( 𝐴𝑥 ∧ ¬ 𝐴𝑥 ) )
31 bren2 ( 𝐴𝑥 ↔ ( 𝐴𝑥 ∧ ¬ 𝐴𝑥 ) )
32 30 31 sylibr ( 𝑥 ≈ ω → 𝐴𝑥 )
33 entr ( ( 𝐴𝑥𝑥 ≈ ω ) → 𝐴 ≈ ω )
34 32 33 mpancom ( 𝑥 ≈ ω → 𝐴 ≈ ω )
35 ensym ( 𝐴 ≈ ω → ω ≈ 𝐴 )
36 bren ( ω ≈ 𝐴 ↔ ∃ 𝑓 𝑓 : ω –1-1-onto𝐴 )
37 f1of ( 𝑓 : ω –1-1-onto𝐴𝑓 : ω ⟶ 𝐴 )
38 peano1 ∅ ∈ ω
39 ffvelrn ( ( 𝑓 : ω ⟶ 𝐴 ∧ ∅ ∈ ω ) → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
40 37 38 39 sylancl ( 𝑓 : ω –1-1-onto𝐴 → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
41 eldifn ( ( 𝑓 ‘ ∅ ) ∈ ( 𝑥 ∖ { ∅ } ) → ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } )
42 41 1 eleq2s ( ( 𝑓 ‘ ∅ ) ∈ 𝐴 → ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } )
43 fvex ( 𝑓 ‘ ∅ ) ∈ V
44 43 elsn ( ( 𝑓 ‘ ∅ ) ∈ { ∅ } ↔ ( 𝑓 ‘ ∅ ) = ∅ )
45 44 notbii ( ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } ↔ ¬ ( 𝑓 ‘ ∅ ) = ∅ )
46 neq0 ( ¬ ( 𝑓 ‘ ∅ ) = ∅ ↔ ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) )
47 45 46 bitr2i ( ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) ↔ ¬ ( 𝑓 ‘ ∅ ) ∈ { ∅ } )
48 42 47 sylibr ( ( 𝑓 ‘ ∅ ) ∈ 𝐴 → ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) )
49 40 48 syl ( 𝑓 : ω –1-1-onto𝐴 → ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) )
50 elunii ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ ( 𝑓 ‘ ∅ ) ∈ 𝐴 ) → 𝑐 𝐴 )
51 40 50 sylan2 ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto𝐴 ) → 𝑐 𝐴 )
52 37 ffvelrnda ( ( 𝑓 : ω –1-1-onto𝐴𝑛 ∈ ω ) → ( 𝑓𝑛 ) ∈ 𝐴 )
53 difabs ( ( 𝑥 ∖ { ∅ } ) ∖ { ∅ } ) = ( 𝑥 ∖ { ∅ } )
54 1 difeq1i ( 𝐴 ∖ { ∅ } ) = ( ( 𝑥 ∖ { ∅ } ) ∖ { ∅ } )
55 53 54 1 3eqtr4i ( 𝐴 ∖ { ∅ } ) = 𝐴
56 pwuni 𝐴 ⊆ 𝒫 𝐴
57 ssdif ( 𝐴 ⊆ 𝒫 𝐴 → ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∖ { ∅ } ) )
58 56 57 ax-mp ( 𝐴 ∖ { ∅ } ) ⊆ ( 𝒫 𝐴 ∖ { ∅ } )
59 55 58 eqsstrri 𝐴 ⊆ ( 𝒫 𝐴 ∖ { ∅ } )
60 59 sseli ( ( 𝑓𝑛 ) ∈ 𝐴 → ( 𝑓𝑛 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
61 60 ralrimivw ( ( 𝑓𝑛 ) ∈ 𝐴 → ∀ 𝑦 𝐴 ( 𝑓𝑛 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
62 52 61 syl ( ( 𝑓 : ω –1-1-onto𝐴𝑛 ∈ ω ) → ∀ 𝑦 𝐴 ( 𝑓𝑛 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
63 62 ralrimiva ( 𝑓 : ω –1-1-onto𝐴 → ∀ 𝑛 ∈ ω ∀ 𝑦 𝐴 ( 𝑓𝑛 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) )
64 2 fmpo ( ∀ 𝑛 ∈ ω ∀ 𝑦 𝐴 ( 𝑓𝑛 ) ∈ ( 𝒫 𝐴 ∖ { ∅ } ) ↔ 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
65 63 64 sylib ( 𝑓 : ω –1-1-onto𝐴𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
66 65 adantl ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto𝐴 ) → 𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) )
67 25 difexi ( 𝑥 ∖ { ∅ } ) ∈ V
68 1 67 eqeltri 𝐴 ∈ V
69 68 uniex 𝐴 ∈ V
70 69 axdc4 ( ( 𝑐 𝐴𝐹 : ( ω × 𝐴 ) ⟶ ( 𝒫 𝐴 ∖ { ∅ } ) ) → ∃ ( : ω ⟶ 𝐴 ∧ ( ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
71 51 66 70 syl2anc ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto𝐴 ) → ∃ ( : ω ⟶ 𝐴 ∧ ( ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
72 3simpb ( ( : ω ⟶ 𝐴 ∧ ( ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) → ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
73 72 eximi ( ∃ ( : ω ⟶ 𝐴 ∧ ( ‘ ∅ ) = 𝑐 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) → ∃ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
74 71 73 syl ( ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) ∧ 𝑓 : ω –1-1-onto𝐴 ) → ∃ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
75 74 ex ( 𝑐 ∈ ( 𝑓 ‘ ∅ ) → ( 𝑓 : ω –1-1-onto𝐴 → ∃ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) )
76 75 exlimiv ( ∃ 𝑐 𝑐 ∈ ( 𝑓 ‘ ∅ ) → ( 𝑓 : ω –1-1-onto𝐴 → ∃ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) )
77 49 76 mpcom ( 𝑓 : ω –1-1-onto𝐴 → ∃ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) )
78 velsn ( 𝑧 ∈ { ∅ } ↔ 𝑧 = ∅ )
79 78 necon3bbii ( ¬ 𝑧 ∈ { ∅ } ↔ 𝑧 ≠ ∅ )
80 1 eleq2i ( 𝑧𝐴𝑧 ∈ ( 𝑥 ∖ { ∅ } ) )
81 eldif ( 𝑧 ∈ ( 𝑥 ∖ { ∅ } ) ↔ ( 𝑧𝑥 ∧ ¬ 𝑧 ∈ { ∅ } ) )
82 80 81 sylbbr ( ( 𝑧𝑥 ∧ ¬ 𝑧 ∈ { ∅ } ) → 𝑧𝐴 )
83 79 82 sylan2br ( ( 𝑧𝑥𝑧 ≠ ∅ ) → 𝑧𝐴 )
84 simpl ( ( 𝑓 : ω –1-1-onto𝐴𝑧𝐴 ) → 𝑓 : ω –1-1-onto𝐴 )
85 f1ofo ( 𝑓 : ω –1-1-onto𝐴𝑓 : ω –onto𝐴 )
86 foelrn ( ( 𝑓 : ω –onto𝐴𝑧𝐴 ) → ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓𝑖 ) )
87 85 86 sylan ( ( 𝑓 : ω –1-1-onto𝐴𝑧𝐴 ) → ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓𝑖 ) )
88 suceq ( 𝑘 = 𝑖 → suc 𝑘 = suc 𝑖 )
89 88 fveq2d ( 𝑘 = 𝑖 → ( ‘ suc 𝑘 ) = ( ‘ suc 𝑖 ) )
90 id ( 𝑘 = 𝑖𝑘 = 𝑖 )
91 fveq2 ( 𝑘 = 𝑖 → ( 𝑘 ) = ( 𝑖 ) )
92 90 91 oveq12d ( 𝑘 = 𝑖 → ( 𝑘 𝐹 ( 𝑘 ) ) = ( 𝑖 𝐹 ( 𝑖 ) ) )
93 89 92 eleq12d ( 𝑘 = 𝑖 → ( ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ↔ ( ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( 𝑖 ) ) ) )
94 93 rspcv ( 𝑖 ∈ ω → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( 𝑖 ) ) ) )
95 94 3ad2ant3 ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( 𝑖 ) ) ) )
96 95 imp ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) → ( ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( 𝑖 ) ) )
97 96 3adant3 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( ‘ suc 𝑖 ) ∈ ( 𝑖 𝐹 ( 𝑖 ) ) )
98 eqcom ( 𝑧 = ( 𝑓𝑖 ) ↔ ( 𝑓𝑖 ) = 𝑧 )
99 f1ocnvfv ( ( 𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( ( 𝑓𝑖 ) = 𝑧 → ( 𝑓𝑧 ) = 𝑖 ) )
100 98 99 syl5bi ( ( 𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( 𝑧 = ( 𝑓𝑖 ) → ( 𝑓𝑧 ) = 𝑖 ) )
101 100 3adant1 ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( 𝑧 = ( 𝑓𝑖 ) → ( 𝑓𝑧 ) = 𝑖 ) )
102 101 imp ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝑓𝑧 ) = 𝑖 )
103 102 eqcomd ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → 𝑖 = ( 𝑓𝑧 ) )
104 103 3adant2 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → 𝑖 = ( 𝑓𝑧 ) )
105 suceq ( 𝑖 = ( 𝑓𝑧 ) → suc 𝑖 = suc ( 𝑓𝑧 ) )
106 104 105 syl ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → suc 𝑖 = suc ( 𝑓𝑧 ) )
107 106 fveq2d ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( ‘ suc 𝑖 ) = ( ‘ suc ( 𝑓𝑧 ) ) )
108 simpr ( ( : ω ⟶ 𝐴𝑖 ∈ ω ) → 𝑖 ∈ ω )
109 ffvelrn ( ( : ω ⟶ 𝐴𝑖 ∈ ω ) → ( 𝑖 ) ∈ 𝐴 )
110 fveq2 ( 𝑛 = 𝑖 → ( 𝑓𝑛 ) = ( 𝑓𝑖 ) )
111 eqidd ( 𝑦 = ( 𝑖 ) → ( 𝑓𝑖 ) = ( 𝑓𝑖 ) )
112 fvex ( 𝑓𝑖 ) ∈ V
113 110 111 2 112 ovmpo ( ( 𝑖 ∈ ω ∧ ( 𝑖 ) ∈ 𝐴 ) → ( 𝑖 𝐹 ( 𝑖 ) ) = ( 𝑓𝑖 ) )
114 108 109 113 syl2anc ( ( : ω ⟶ 𝐴𝑖 ∈ ω ) → ( 𝑖 𝐹 ( 𝑖 ) ) = ( 𝑓𝑖 ) )
115 114 3adant2 ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( 𝑖 𝐹 ( 𝑖 ) ) = ( 𝑓𝑖 ) )
116 115 3ad2ant1 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝑖 𝐹 ( 𝑖 ) ) = ( 𝑓𝑖 ) )
117 97 107 116 3eltr3d ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( ‘ suc ( 𝑓𝑧 ) ) ∈ ( 𝑓𝑖 ) )
118 37 ffvelrnda ( ( 𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( 𝑓𝑖 ) ∈ 𝐴 )
119 118 3adant1 ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( 𝑓𝑖 ) ∈ 𝐴 )
120 119 3ad2ant1 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝑓𝑖 ) ∈ 𝐴 )
121 eleq1 ( 𝑧 = ( 𝑓𝑖 ) → ( 𝑧𝐴 ↔ ( 𝑓𝑖 ) ∈ 𝐴 ) )
122 121 3ad2ant3 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝑧𝐴 ↔ ( 𝑓𝑖 ) ∈ 𝐴 ) )
123 120 122 mpbird ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → 𝑧𝐴 )
124 fveq2 ( 𝑤 = 𝑧 → ( 𝑓𝑤 ) = ( 𝑓𝑧 ) )
125 suceq ( ( 𝑓𝑤 ) = ( 𝑓𝑧 ) → suc ( 𝑓𝑤 ) = suc ( 𝑓𝑧 ) )
126 124 125 syl ( 𝑤 = 𝑧 → suc ( 𝑓𝑤 ) = suc ( 𝑓𝑧 ) )
127 126 fveq2d ( 𝑤 = 𝑧 → ( ‘ suc ( 𝑓𝑤 ) ) = ( ‘ suc ( 𝑓𝑧 ) ) )
128 fvex ( ‘ suc ( 𝑓𝑧 ) ) ∈ V
129 127 3 128 fvmpt ( 𝑧𝐴 → ( 𝐺𝑧 ) = ( ‘ suc ( 𝑓𝑧 ) ) )
130 123 129 syl ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝐺𝑧 ) = ( ‘ suc ( 𝑓𝑧 ) ) )
131 simp3 ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → 𝑧 = ( 𝑓𝑖 ) )
132 117 130 131 3eltr4d ( ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ∧ 𝑧 = ( 𝑓𝑖 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 )
133 132 3exp ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝑧 = ( 𝑓𝑖 ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
134 133 com3r ( 𝑧 = ( 𝑓𝑖 ) → ( ( : ω ⟶ 𝐴𝑓 : ω –1-1-onto𝐴𝑖 ∈ ω ) → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
135 134 3expd ( 𝑧 = ( 𝑓𝑖 ) → ( : ω ⟶ 𝐴 → ( 𝑓 : ω –1-1-onto𝐴 → ( 𝑖 ∈ ω → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) ) ) )
136 135 com4r ( 𝑖 ∈ ω → ( 𝑧 = ( 𝑓𝑖 ) → ( : ω ⟶ 𝐴 → ( 𝑓 : ω –1-1-onto𝐴 → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) ) ) )
137 136 rexlimiv ( ∃ 𝑖 ∈ ω 𝑧 = ( 𝑓𝑖 ) → ( : ω ⟶ 𝐴 → ( 𝑓 : ω –1-1-onto𝐴 → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) ) )
138 87 137 syl ( ( 𝑓 : ω –1-1-onto𝐴𝑧𝐴 ) → ( : ω ⟶ 𝐴 → ( 𝑓 : ω –1-1-onto𝐴 → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) ) )
139 84 138 mpid ( ( 𝑓 : ω –1-1-onto𝐴𝑧𝐴 ) → ( : ω ⟶ 𝐴 → ( ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
140 139 impd ( ( 𝑓 : ω –1-1-onto𝐴𝑧𝐴 ) → ( ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) → ( 𝐺𝑧 ) ∈ 𝑧 ) )
141 140 impancom ( ( 𝑓 : ω –1-1-onto𝐴 ∧ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) → ( 𝑧𝐴 → ( 𝐺𝑧 ) ∈ 𝑧 ) )
142 83 141 syl5 ( ( 𝑓 : ω –1-1-onto𝐴 ∧ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) → ( ( 𝑧𝑥𝑧 ≠ ∅ ) → ( 𝐺𝑧 ) ∈ 𝑧 ) )
143 142 expd ( ( 𝑓 : ω –1-1-onto𝐴 ∧ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) → ( 𝑧𝑥 → ( 𝑧 ≠ ∅ → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
144 143 ralrimiv ( ( 𝑓 : ω –1-1-onto𝐴 ∧ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) → ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝐺𝑧 ) ∈ 𝑧 ) )
145 fvrn0 ( ‘ suc ( 𝑓𝑤 ) ) ∈ ( ran ∪ { ∅ } )
146 145 rgenw 𝑤𝐴 ( ‘ suc ( 𝑓𝑤 ) ) ∈ ( ran ∪ { ∅ } )
147 eqid ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) = ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) )
148 147 fmpt ( ∀ 𝑤𝐴 ( ‘ suc ( 𝑓𝑤 ) ) ∈ ( ran ∪ { ∅ } ) ↔ ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) : 𝐴 ⟶ ( ran ∪ { ∅ } ) )
149 146 148 mpbi ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) : 𝐴 ⟶ ( ran ∪ { ∅ } )
150 vex ∈ V
151 150 rnex ran ∈ V
152 p0ex { ∅ } ∈ V
153 151 152 unex ( ran ∪ { ∅ } ) ∈ V
154 fex2 ( ( ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) : 𝐴 ⟶ ( ran ∪ { ∅ } ) ∧ 𝐴 ∈ V ∧ ( ran ∪ { ∅ } ) ∈ V ) → ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) ∈ V )
155 149 68 153 154 mp3an ( 𝑤𝐴 ↦ ( ‘ suc ( 𝑓𝑤 ) ) ) ∈ V
156 3 155 eqeltri 𝐺 ∈ V
157 fveq1 ( 𝑔 = 𝐺 → ( 𝑔𝑧 ) = ( 𝐺𝑧 ) )
158 157 eleq1d ( 𝑔 = 𝐺 → ( ( 𝑔𝑧 ) ∈ 𝑧 ↔ ( 𝐺𝑧 ) ∈ 𝑧 ) )
159 158 imbi2d ( 𝑔 = 𝐺 → ( ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) ↔ ( 𝑧 ≠ ∅ → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
160 159 ralbidv ( 𝑔 = 𝐺 → ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) ↔ ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝐺𝑧 ) ∈ 𝑧 ) ) )
161 156 160 spcev ( ∀ 𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝐺𝑧 ) ∈ 𝑧 ) → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )
162 144 161 syl ( ( 𝑓 : ω –1-1-onto𝐴 ∧ ( : ω ⟶ 𝐴 ∧ ∀ 𝑘 ∈ ω ( ‘ suc 𝑘 ) ∈ ( 𝑘 𝐹 ( 𝑘 ) ) ) ) → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )
163 77 162 exlimddv ( 𝑓 : ω –1-1-onto𝐴 → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )
164 163 exlimiv ( ∃ 𝑓 𝑓 : ω –1-1-onto𝐴 → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )
165 36 164 sylbi ( ω ≈ 𝐴 → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )
166 34 35 165 3syl ( 𝑥 ≈ ω → ∃ 𝑔𝑧𝑥 ( 𝑧 ≠ ∅ → ( 𝑔𝑧 ) ∈ 𝑧 ) )