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 ⊢A=x∖∅
axcclem.2 ⊢F=n∈ω,y∈⋃A⟼f⁡n
axcclem.3 ⊢G=w∈A⟼h⁡suc⁡f-1⁡w
Assertion axcclem ⊢x≈ω→∃g∀z∈xz≠∅→g⁡z∈z

Proof

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