This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ffvelcdm ⊢ ( ( 𝑓 : ω ⟶ 𝐴 ∧ ∅ ∈ ω ) → ( 𝑓 ‘ ∅ ) ∈ 𝐴 )
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 ffvelcdmda ⊢ ( ( 𝑓 : ω –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 biimtrid ⊢ ( ( 𝑓 : ω –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 ffvelcdm ⊢ ( ( ℎ : ω ⟶ ∪ 𝐴 ∧ 𝑖 ∈ ω ) → ( ℎ ‘ 𝑖 ) ∈ ∪ 𝐴 )
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 ffvelcdmda ⊢ ( ( 𝑓 : ω –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 ⊢ ( 𝑥 ≈ ω → ∃ 𝑔 ∀ 𝑧 ∈ 𝑥 ( 𝑧 ≠ ∅ → ( 𝑔 ‘ 𝑧 ) ∈ 𝑧 ) )