Metamath Proof Explorer

Theorem axdc4lem

Description: Lemma for axdc4 . (Contributed by Mario Carneiro, 31-Jan-2013) (Revised by Mario Carneiro, 16-Nov-2013)

Ref Expression
Hypotheses axdc4lem.1 ⊢A∈V
axdc4lem.2 ⊢G=n∈ω,x∈A⟼suc⁡n×nFx
Assertion axdc4lem ⊢C∈A∧F:ω×A⟶𝒫A∖∅→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k

Proof

Step Hyp Ref Expression
1 axdc4lem.1 ⊢A∈V
2 axdc4lem.2 ⊢G=n∈ω,x∈A⟼suc⁡n×nFx
3 peano1 ⊢∅∈ω
4 opelxpi ⊢∅∈ω∧C∈A→∅C∈ω×A
5 3 4 mpan ⊢C∈A→∅C∈ω×A
6 simp2 ⊢F:ω×A⟶𝒫A∖∅∧n∈ω∧x∈A→n∈ω
7 fovcdm ⊢F:ω×A⟶𝒫A∖∅∧n∈ω∧x∈A→nFx∈𝒫A∖∅
8 peano2 ⊢n∈ω→suc⁡n∈ω
9 8 snssd ⊢n∈ω→suc⁡n⊆ω
10 eldifi ⊢nFx∈𝒫A∖∅→nFx∈𝒫A
11 1 elpw2 ⊢nFx∈𝒫A↔nFx⊆A
12 xpss12 ⊢suc⁡n⊆ω∧nFx⊆A→suc⁡n×nFx⊆ω×A
13 11 12 sylan2b ⊢suc⁡n⊆ω∧nFx∈𝒫A→suc⁡n×nFx⊆ω×A
14 9 10 13 syl2an ⊢n∈ω∧nFx∈𝒫A∖∅→suc⁡n×nFx⊆ω×A
15 snex ⊢suc⁡n∈V
16 ovex ⊢nFx∈V
17 15 16 xpex ⊢suc⁡n×nFx∈V
18 17 elpw ⊢suc⁡n×nFx∈𝒫ω×A↔suc⁡n×nFx⊆ω×A
19 14 18 sylibr ⊢n∈ω∧nFx∈𝒫A∖∅→suc⁡n×nFx∈𝒫ω×A
20 6 7 19 syl2anc ⊢F:ω×A⟶𝒫A∖∅∧n∈ω∧x∈A→suc⁡n×nFx∈𝒫ω×A
21 eldifn ⊢nFx∈𝒫A∖∅→¬nFx∈∅
22 16 elsn ⊢nFx∈∅↔nFx=∅
23 22 necon3bbii ⊢¬nFx∈∅↔nFx≠∅
24 vex ⊢n∈V
25 24 sucex ⊢suc⁡n∈V
26 25 snnz ⊢suc⁡n≠∅
27 xpnz ⊢suc⁡n≠∅∧nFx≠∅↔suc⁡n×nFx≠∅
28 27 biimpi ⊢suc⁡n≠∅∧nFx≠∅→suc⁡n×nFx≠∅
29 26 28 mpan ⊢nFx≠∅→suc⁡n×nFx≠∅
30 23 29 sylbi ⊢¬nFx∈∅→suc⁡n×nFx≠∅
31 17 elsn ⊢suc⁡n×nFx∈∅↔suc⁡n×nFx=∅
32 31 necon3bbii ⊢¬suc⁡n×nFx∈∅↔suc⁡n×nFx≠∅
33 30 32 sylibr ⊢¬nFx∈∅→¬suc⁡n×nFx∈∅
34 7 21 33 3syl ⊢F:ω×A⟶𝒫A∖∅∧n∈ω∧x∈A→¬suc⁡n×nFx∈∅
35 20 34 eldifd ⊢F:ω×A⟶𝒫A∖∅∧n∈ω∧x∈A→suc⁡n×nFx∈𝒫ω×A∖∅
36 35 3expib ⊢F:ω×A⟶𝒫A∖∅→n∈ω∧x∈A→suc⁡n×nFx∈𝒫ω×A∖∅
37 36 ralrimivv ⊢F:ω×A⟶𝒫A∖∅→∀n∈ω∀x∈Asuc⁡n×nFx∈𝒫ω×A∖∅
38 2 fmpo ⊢∀n∈ω∀x∈Asuc⁡n×nFx∈𝒫ω×A∖∅↔G:ω×A⟶𝒫ω×A∖∅
39 37 38 sylib ⊢F:ω×A⟶𝒫A∖∅→G:ω×A⟶𝒫ω×A∖∅
40 dcomex ⊢ω∈V
41 40 1 xpex ⊢ω×A∈V
42 41 axdc3 ⊢∅C∈ω×A∧G:ω×A⟶𝒫ω×A∖∅→∃hh:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k
43 5 39 42 syl2an ⊢C∈A∧F:ω×A⟶𝒫A∖∅→∃hh:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k
44 2ndcof ⊢h:ω⟶ω×A→2nd∘h:ω⟶A
45 44 3ad2ant1 ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h:ω⟶A
46 45 adantl ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h:ω⟶A
47 fex2 ⊢2nd∘h:ω⟶A∧ω∈V∧A∈V→2nd∘h∈V
48 40 1 47 mp3an23 ⊢2nd∘h:ω⟶A→2nd∘h∈V
49 46 48 syl ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h∈V
50 fvco3 ⊢h:ω⟶ω×A∧∅∈ω→2nd∘h⁡∅=2nd⁡h⁡∅
51 3 50 mpan2 ⊢h:ω⟶ω×A→2nd∘h⁡∅=2nd⁡h⁡∅
52 51 3ad2ant1 ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡∅=2nd⁡h⁡∅
53 fveq2 ⊢h⁡∅=∅C→2nd⁡h⁡∅=2nd⁡∅C
54 53 3ad2ant2 ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd⁡h⁡∅=2nd⁡∅C
55 52 54 eqtrd ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡∅=2nd⁡∅C
56 op2ndg ⊢∅∈ω∧C∈A→2nd⁡∅C=C
57 3 56 mpan ⊢C∈A→2nd⁡∅C=C
58 55 57 sylan9eqr ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡∅=C
59 nfv ⊢ℲkC∈A
60 nfv ⊢Ⅎkh:ω⟶ω×A
61 nfv ⊢Ⅎkh⁡∅=∅C
62 nfra1 ⊢Ⅎk∀k∈ωh⁡suc⁡k∈G⁡h⁡k
63 60 61 62 nf3an ⊢Ⅎkh:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k
64 59 63 nfan ⊢ℲkC∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k
65 fveq2 ⊢m=∅→h⁡m=h⁡∅
66 opeq1 ⊢m=∅→mz=∅z
67 65 66 eqeq12d ⊢m=∅→h⁡m=mz↔h⁡∅=∅z
68 67 exbidv ⊢m=∅→∃zh⁡m=mz↔∃zh⁡∅=∅z
69 fveq2 ⊢m=i→h⁡m=h⁡i
70 opeq1 ⊢m=i→mz=iz
71 69 70 eqeq12d ⊢m=i→h⁡m=mz↔h⁡i=iz
72 71 exbidv ⊢m=i→∃zh⁡m=mz↔∃zh⁡i=iz
73 fveq2 ⊢m=suc⁡i→h⁡m=h⁡suc⁡i
74 opeq1 ⊢m=suc⁡i→mz=suc⁡iz
75 73 74 eqeq12d ⊢m=suc⁡i→h⁡m=mz↔h⁡suc⁡i=suc⁡iz
76 75 exbidv ⊢m=suc⁡i→∃zh⁡m=mz↔∃zh⁡suc⁡i=suc⁡iz
77 opeq2 ⊢z=C→∅z=∅C
78 77 eqeq2d ⊢z=C→h⁡∅=∅z↔h⁡∅=∅C
79 78 spcegv ⊢C∈A→h⁡∅=∅C→∃zh⁡∅=∅z
80 79 imp ⊢C∈A∧h⁡∅=∅C→∃zh⁡∅=∅z
81 80 3ad2antr2 ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃zh⁡∅=∅z
82 fveq2 ⊢h⁡i=iz→G⁡h⁡i=G⁡iz
83 df-ov ⊢iGz=G⁡iz
84 82 83 eqtr4di ⊢h⁡i=iz→G⁡h⁡i=iGz
85 84 adantl ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→G⁡h⁡i=iGz
86 simplr ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→i∈ω
87 ffvelcdm ⊢h:ω⟶ω×A∧i∈ω→h⁡i∈ω×A
88 eleq1 ⊢h⁡i=iz→h⁡i∈ω×A↔iz∈ω×A
89 opelxp2 ⊢iz∈ω×A→z∈A
90 88 89 syl6bi ⊢h⁡i=iz→h⁡i∈ω×A→z∈A
91 87 90 mpan9 ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→z∈A
92 suceq ⊢n=i→suc⁡n=suc⁡i
93 92 sneqd ⊢n=i→suc⁡n=suc⁡i
94 oveq1 ⊢n=i→nFx=iFx
95 93 94 xpeq12d ⊢n=i→suc⁡n×nFx=suc⁡i×iFx
96 oveq2 ⊢x=z→iFx=iFz
97 96 xpeq2d ⊢x=z→suc⁡i×iFx=suc⁡i×iFz
98 snex ⊢suc⁡i∈V
99 ovex ⊢iFz∈V
100 98 99 xpex ⊢suc⁡i×iFz∈V
101 95 97 2 100 ovmpo ⊢i∈ω∧z∈A→iGz=suc⁡i×iFz
102 86 91 101 syl2anc ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→iGz=suc⁡i×iFz
103 85 102 eqtrd ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→G⁡h⁡i=suc⁡i×iFz
104 suceq ⊢k=i→suc⁡k=suc⁡i
105 104 fveq2d ⊢k=i→h⁡suc⁡k=h⁡suc⁡i
106 2fveq3 ⊢k=i→G⁡h⁡k=G⁡h⁡i
107 105 106 eleq12d ⊢k=i→h⁡suc⁡k∈G⁡h⁡k↔h⁡suc⁡i∈G⁡h⁡i
108 107 rspcv ⊢i∈ω→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→h⁡suc⁡i∈G⁡h⁡i
109 108 ad2antlr ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→h⁡suc⁡i∈G⁡h⁡i
110 eleq2 ⊢G⁡h⁡i=suc⁡i×iFz→h⁡suc⁡i∈G⁡h⁡i↔h⁡suc⁡i∈suc⁡i×iFz
111 elxp ⊢h⁡suc⁡i∈suc⁡i×iFz↔∃s∃th⁡suc⁡i=st∧s∈suc⁡i∧t∈iFz
112 velsn ⊢s∈suc⁡i↔s=suc⁡i
113 opeq1 ⊢s=suc⁡i→st=suc⁡it
114 112 113 sylbi ⊢s∈suc⁡i→st=suc⁡it
115 114 eqeq2d ⊢s∈suc⁡i→h⁡suc⁡i=st↔h⁡suc⁡i=suc⁡it
116 115 biimpac ⊢h⁡suc⁡i=st∧s∈suc⁡i→h⁡suc⁡i=suc⁡it
117 116 adantrr ⊢h⁡suc⁡i=st∧s∈suc⁡i∧t∈iFz→h⁡suc⁡i=suc⁡it
118 117 eximi ⊢∃th⁡suc⁡i=st∧s∈suc⁡i∧t∈iFz→∃th⁡suc⁡i=suc⁡it
119 118 exlimiv ⊢∃s∃th⁡suc⁡i=st∧s∈suc⁡i∧t∈iFz→∃th⁡suc⁡i=suc⁡it
120 111 119 sylbi ⊢h⁡suc⁡i∈suc⁡i×iFz→∃th⁡suc⁡i=suc⁡it
121 110 120 syl6bi ⊢G⁡h⁡i=suc⁡i×iFz→h⁡suc⁡i∈G⁡h⁡i→∃th⁡suc⁡i=suc⁡it
122 103 109 121 sylsyld ⊢h:ω⟶ω×A∧i∈ω∧h⁡i=iz→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃th⁡suc⁡i=suc⁡it
123 122 expcom ⊢h⁡i=iz→h:ω⟶ω×A∧i∈ω→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃th⁡suc⁡i=suc⁡it
124 123 exlimiv ⊢∃zh⁡i=iz→h:ω⟶ω×A∧i∈ω→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃th⁡suc⁡i=suc⁡it
125 124 com3l ⊢h:ω⟶ω×A∧i∈ω→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃zh⁡i=iz→∃th⁡suc⁡i=suc⁡it
126 opeq2 ⊢t=z→suc⁡it=suc⁡iz
127 126 eqeq2d ⊢t=z→h⁡suc⁡i=suc⁡it↔h⁡suc⁡i=suc⁡iz
128 127 cbvexvw ⊢∃th⁡suc⁡i=suc⁡it↔∃zh⁡suc⁡i=suc⁡iz
129 125 128 syl8ib ⊢h:ω⟶ω×A∧i∈ω→∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃zh⁡i=iz→∃zh⁡suc⁡i=suc⁡iz
130 129 impancom ⊢h:ω⟶ω×A∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→i∈ω→∃zh⁡i=iz→∃zh⁡suc⁡i=suc⁡iz
131 130 3adant2 ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→i∈ω→∃zh⁡i=iz→∃zh⁡suc⁡i=suc⁡iz
132 131 adantl ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→i∈ω→∃zh⁡i=iz→∃zh⁡suc⁡i=suc⁡iz
133 132 com12 ⊢i∈ω→C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃zh⁡i=iz→∃zh⁡suc⁡i=suc⁡iz
134 68 72 76 81 133 finds2 ⊢m∈ω→C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃zh⁡m=mz
135 134 com12 ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→m∈ω→∃zh⁡m=mz
136 135 ralrimiv ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∀m∈ω∃zh⁡m=mz
137 fveq2 ⊢m=k→h⁡m=h⁡k
138 opeq1 ⊢m=k→mz=kz
139 137 138 eqeq12d ⊢m=k→h⁡m=mz↔h⁡k=kz
140 139 exbidv ⊢m=k→∃zh⁡m=mz↔∃zh⁡k=kz
141 140 rspccv ⊢∀m∈ω∃zh⁡m=mz→k∈ω→∃zh⁡k=kz
142 136 141 syl ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→k∈ω→∃zh⁡k=kz
143 142 3impia ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→∃zh⁡k=kz
144 simp21 ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→h:ω⟶ω×A
145 simp3 ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→k∈ω
146 rspa ⊢∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→h⁡suc⁡k∈G⁡h⁡k
147 146 3ad2antl3 ⊢h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→h⁡suc⁡k∈G⁡h⁡k
148 147 3adant1 ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→h⁡suc⁡k∈G⁡h⁡k
149 simpl ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡k=kz
150 149 fveq2d ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→G⁡h⁡k=G⁡kz
151 simprr ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→k∈ω
152 eleq1 ⊢h⁡k=kz→h⁡k∈ω×A↔kz∈ω×A
153 opelxp2 ⊢kz∈ω×A→z∈A
154 152 153 syl6bi ⊢h⁡k=kz→h⁡k∈ω×A→z∈A
155 ffvelcdm ⊢h:ω⟶ω×A∧k∈ω→h⁡k∈ω×A
156 154 155 impel ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→z∈A
157 df-ov ⊢kGz=G⁡kz
158 suceq ⊢n=k→suc⁡n=suc⁡k
159 158 sneqd ⊢n=k→suc⁡n=suc⁡k
160 oveq1 ⊢n=k→nFx=kFx
161 159 160 xpeq12d ⊢n=k→suc⁡n×nFx=suc⁡k×kFx
162 oveq2 ⊢x=z→kFx=kFz
163 162 xpeq2d ⊢x=z→suc⁡k×kFx=suc⁡k×kFz
164 snex ⊢suc⁡k∈V
165 ovex ⊢kFz∈V
166 164 165 xpex ⊢suc⁡k×kFz∈V
167 161 163 2 166 ovmpo ⊢k∈ω∧z∈A→kGz=suc⁡k×kFz
168 157 167 eqtr3id ⊢k∈ω∧z∈A→G⁡kz=suc⁡k×kFz
169 151 156 168 syl2anc ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→G⁡kz=suc⁡k×kFz
170 150 169 eqtrd ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→G⁡h⁡k=suc⁡k×kFz
171 170 eleq2d ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈G⁡h⁡k↔h⁡suc⁡k∈suc⁡k×kFz
172 elxp ⊢h⁡suc⁡k∈suc⁡k×kFz↔∃s∃th⁡suc⁡k=st∧s∈suc⁡k∧t∈kFz
173 peano2 ⊢k∈ω→suc⁡k∈ω
174 fvco3 ⊢h:ω⟶ω×A∧suc⁡k∈ω→2nd∘h⁡suc⁡k=2nd⁡h⁡suc⁡k
175 173 174 sylan2 ⊢h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k=2nd⁡h⁡suc⁡k
176 175 adantl ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k=2nd⁡h⁡suc⁡k
177 simpll ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡suc⁡k=st
178 177 fveq2d ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd⁡h⁡suc⁡k=2nd⁡st
179 176 178 eqtrd ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k=2nd⁡st
180 vex ⊢s∈V
181 vex ⊢t∈V
182 180 181 op2nd ⊢2nd⁡st=t
183 179 182 eqtrdi ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k=t
184 fvco3 ⊢h:ω⟶ω×A∧k∈ω→2nd∘h⁡k=2nd⁡h⁡k
185 184 adantl ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡k=2nd⁡h⁡k
186 simplr ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡k=kz
187 186 fveq2d ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd⁡h⁡k=2nd⁡kz
188 185 187 eqtrd ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡k=2nd⁡kz
189 vex ⊢k∈V
190 vex ⊢z∈V
191 189 190 op2nd ⊢2nd⁡kz=z
192 188 191 eqtrdi ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡k=z
193 192 oveq2d ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→kF2nd∘h⁡k=kFz
194 183 193 eleq12d ⊢h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k↔t∈kFz
195 194 biimprcd ⊢t∈kFz→h⁡suc⁡k=st∧h⁡k=kz∧h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
196 195 exp4c ⊢t∈kFz→h⁡suc⁡k=st→h⁡k=kz→h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
197 196 adantl ⊢s∈suc⁡k∧t∈kFz→h⁡suc⁡k=st→h⁡k=kz→h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
198 197 impcom ⊢h⁡suc⁡k=st∧s∈suc⁡k∧t∈kFz→h⁡k=kz→h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
199 198 exlimivv ⊢∃s∃th⁡suc⁡k=st∧s∈suc⁡k∧t∈kFz→h⁡k=kz→h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
200 172 199 sylbi ⊢h⁡suc⁡k∈suc⁡k×kFz→h⁡k=kz→h:ω⟶ω×A∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
201 200 com3l ⊢h⁡k=kz→h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈suc⁡k×kFz→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
202 201 imp ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈suc⁡k×kFz→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
203 171 202 sylbid ⊢h⁡k=kz∧h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
204 203 ex ⊢h⁡k=kz→h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
205 204 exlimiv ⊢∃zh⁡k=kz→h:ω⟶ω×A∧k∈ω→h⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
206 205 3imp ⊢∃zh⁡k=kz∧h:ω⟶ω×A∧k∈ω∧h⁡suc⁡k∈G⁡h⁡k→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
207 143 144 145 148 206 syl121anc ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k∧k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
208 207 3expia ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→k∈ω→2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
209 64 208 ralrimi ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∀k∈ω2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
210 46 58 209 3jca ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→2nd∘h:ω⟶A∧2nd∘h⁡∅=C∧∀k∈ω2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
211 feq1 ⊢g=2nd∘h→g:ω⟶A↔2nd∘h:ω⟶A
212 fveq1 ⊢g=2nd∘h→g⁡∅=2nd∘h⁡∅
213 212 eqeq1d ⊢g=2nd∘h→g⁡∅=C↔2nd∘h⁡∅=C
214 fveq1 ⊢g=2nd∘h→g⁡suc⁡k=2nd∘h⁡suc⁡k
215 fveq1 ⊢g=2nd∘h→g⁡k=2nd∘h⁡k
216 215 oveq2d ⊢g=2nd∘h→kFg⁡k=kF2nd∘h⁡k
217 214 216 eleq12d ⊢g=2nd∘h→g⁡suc⁡k∈kFg⁡k↔2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
218 217 ralbidv ⊢g=2nd∘h→∀k∈ωg⁡suc⁡k∈kFg⁡k↔∀k∈ω2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
219 211 213 218 3anbi123d ⊢g=2nd∘h→g:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k↔2nd∘h:ω⟶A∧2nd∘h⁡∅=C∧∀k∈ω2nd∘h⁡suc⁡k∈kF2nd∘h⁡k
220 49 210 219 spcedv ⊢C∈A∧h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k
221 220 ex ⊢C∈A→h:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k
222 221 exlimdv ⊢C∈A→∃hh:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k
223 222 adantr ⊢C∈A∧F:ω×A⟶𝒫A∖∅→∃hh:ω⟶ω×A∧h⁡∅=∅C∧∀k∈ωh⁡suc⁡k∈G⁡h⁡k→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k
224 43 223 mpd ⊢C∈A∧F:ω×A⟶𝒫A∖∅→∃gg:ω⟶A∧g⁡∅=C∧∀k∈ωg⁡suc⁡k∈kFg⁡k