Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  heibor1lem Unicode version

Theorem heibor1lem 26408
 Description: Lemma for heibor1 26409. A compact metric space is complete. This proof works by considering the collection for each , which has the finite intersection property because any finite intersection of upper integer sets is another upper integer set, so any finite intersection of the image closures will contain for some . Thus, by compactness, the intersection contains a point , which must then be the convergent point of . (Contributed by Jeff Madsen, 17-Jan-2014.) (Revised by Mario Carneiro, 5-Jun-2014.)
Hypotheses
Ref Expression
heibor.1
heibor1.3
heibor1.4
heibor1.5
heibor1.6
Assertion
Ref Expression
heibor1lem

Proof of Theorem heibor1lem
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 heibor1.4 . . 3
2 heibor1.3 . . . . . . . . . 10
3 metxmet 18317 . . . . . . . . . 10
42, 3syl 16 . . . . . . . . 9
5 heibor.1 . . . . . . . . . 10
65mopntop 18423 . . . . . . . . 9
74, 6syl 16 . . . . . . . 8
8 imassrn 5175 . . . . . . . . 9
9 heibor1.6 . . . . . . . . . . 11
10 frn 5556 . . . . . . . . . . 11
119, 10syl 16 . . . . . . . . . 10
125mopnuni 18424 . . . . . . . . . . 11
134, 12syl 16 . . . . . . . . . 10
1411, 13sseqtrd 3344 . . . . . . . . 9
158, 14syl5ss 3319 . . . . . . . 8
16 eqid 2404 . . . . . . . . 9
1716clscld 17066 . . . . . . . 8
187, 15, 17syl2anc 643 . . . . . . 7
19 eleq1a 2473 . . . . . . 7
2018, 19syl 16 . . . . . 6
2120rexlimdvw 2793 . . . . 5
2221abssdv 3377 . . . 4
23 fvex 5701 . . . . 5
2423elpw2 4324 . . . 4
2522, 24sylibr 204 . . 3
26 elin 3490 . . . . . . 7
27 vex 2919 . . . . . . . . . 10
2827elpw 3765 . . . . . . . . 9
29 ssabral 3374 . . . . . . . . 9
3028, 29bitri 241 . . . . . . . 8
3130anbi1i 677 . . . . . . 7
3226, 31bitri 241 . . . . . 6
33 raleq 2864 . . . . . . . . . . . . . 14
3433anbi2d 685 . . . . . . . . . . . . 13
35 inteq 4013 . . . . . . . . . . . . . . 15
3635sseq2d 3336 . . . . . . . . . . . . . 14
3736rexbidv 2687 . . . . . . . . . . . . 13
3834, 37imbi12d 312 . . . . . . . . . . . 12
39 raleq 2864 . . . . . . . . . . . . . 14
4039anbi2d 685 . . . . . . . . . . . . 13
41 inteq 4013 . . . . . . . . . . . . . . 15
4241sseq2d 3336 . . . . . . . . . . . . . 14
4342rexbidv 2687 . . . . . . . . . . . . 13
4440, 43imbi12d 312 . . . . . . . . . . . 12
45 raleq 2864 . . . . . . . . . . . . . 14
4645anbi2d 685 . . . . . . . . . . . . 13
47 inteq 4013 . . . . . . . . . . . . . . 15
4847sseq2d 3336 . . . . . . . . . . . . . 14
4948rexbidv 2687 . . . . . . . . . . . . 13
5046, 49imbi12d 312 . . . . . . . . . . . 12
51 raleq 2864 . . . . . . . . . . . . . 14
5251anbi2d 685 . . . . . . . . . . . . 13
53 inteq 4013 . . . . . . . . . . . . . . 15
5453sseq2d 3336 . . . . . . . . . . . . . 14
5554rexbidv 2687 . . . . . . . . . . . . 13
5652, 55imbi12d 312 . . . . . . . . . . . 12
57 uzf 10447 . . . . . . . . . . . . . . . 16
58 ffn 5550 . . . . . . . . . . . . . . . 16
5957, 58ax-mp 8 . . . . . . . . . . . . . . 15
60 0z 10249 . . . . . . . . . . . . . . 15
61 fnfvelrn 5826 . . . . . . . . . . . . . . 15
6259, 60, 61mp2an 654 . . . . . . . . . . . . . 14
63 ssv 3328 . . . . . . . . . . . . . . 15
64 int0 4024 . . . . . . . . . . . . . . 15
6563, 64sseqtr4i 3341 . . . . . . . . . . . . . 14
66 imaeq2 5158 . . . . . . . . . . . . . . . 16
6766sseq1d 3335 . . . . . . . . . . . . . . 15
6867rspcev 3012 . . . . . . . . . . . . . 14
6962, 65, 68mp2an 654 . . . . . . . . . . . . 13
7069a1i 11 . . . . . . . . . . . 12
71 ssun1 3470 . . . . . . . . . . . . . . . . 17
72 ssralv 3367 . . . . . . . . . . . . . . . . 17
7371, 72ax-mp 8 . . . . . . . . . . . . . . . 16
7473anim2i 553 . . . . . . . . . . . . . . 15
7574imim1i 56 . . . . . . . . . . . . . 14
76 ssun2 3471 . . . . . . . . . . . . . . . . . 18
77 ssralv 3367 . . . . . . . . . . . . . . . . . 18
7876, 77ax-mp 8 . . . . . . . . . . . . . . . . 17
79 vex 2919 . . . . . . . . . . . . . . . . . 18
80 eqeq1 2410 . . . . . . . . . . . . . . . . . . 19
8180rexbidv 2687 . . . . . . . . . . . . . . . . . 18
8279, 81ralsn 3809 . . . . . . . . . . . . . . . . 17
8378, 82sylib 189 . . . . . . . . . . . . . . . 16
84 uzin2 12103 . . . . . . . . . . . . . . . . . . . 20
858, 11syl5ss 3319 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
8685, 13sseqtrd 3344 . . . . . . . . . . . . . . . . . . . . . . . . . 26
8716sscls 17075 . . . . . . . . . . . . . . . . . . . . . . . . . 26
887, 86, 87syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
89 sseq2 3330 . . . . . . . . . . . . . . . . . . . . . . . . 25
9088, 89syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . . 24
91 inss2 3522 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
92 inss1 3521 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
93 imass2 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
94 imass2 5199 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
9593, 94anim12i 550 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
96 ssin 3523 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9795, 96sylib 189 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9891, 92, 97mp2an 654 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
99 ss2in 3528 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10098, 99syl5ss 3319 . . . . . . . . . . . . . . . . . . . . . . . . . 26
10179intunsn 4049 . . . . . . . . . . . . . . . . . . . . . . . . . 26
102100, 101syl6sseqr 3355 . . . . . . . . . . . . . . . . . . . . . . . . 25
103102expcom 425 . . . . . . . . . . . . . . . . . . . . . . . 24
10490, 103syl6 31 . . . . . . . . . . . . . . . . . . . . . . 23
105104imp3a 421 . . . . . . . . . . . . . . . . . . . . . 22
106 imaeq2 5158 . . . . . . . . . . . . . . . . . . . . . . . . 25
107106sseq1d 3335 . . . . . . . . . . . . . . . . . . . . . . . 24
108107rspcev 3012 . . . . . . . . . . . . . . . . . . . . . . 23
109108expcom 425 . . . . . . . . . . . . . . . . . . . . . 22
110105, 109syl6 31 . . . . . . . . . . . . . . . . . . . . 21
111110com23 74 . . . . . . . . . . . . . . . . . . . 20
11284, 111syl5 30 . . . . . . . . . . . . . . . . . . 19
113112rexlimdvv 2796 . . . . . . . . . . . . . . . . . 18
114 reeanv 2835 . . . . . . . . . . . . . . . . . 18
115 imaeq2 5158 . . . . . . . . . . . . . . . . . . . 20
116115sseq1d 3335 . . . . . . . . . . . . . . . . . . 19
117116cbvrexv 2893 . . . . . . . . . . . . . . . . . 18
118113, 114, 1173imtr3g 261 . . . . . . . . . . . . . . . . 17
119118exp3a 426 . . . . . . . . . . . . . . . 16
12083, 119syl5 30 . . . . . . . . . . . . . . 15
121120imp 419 . . . . . . . . . . . . . 14
12275, 121sylcom 27 . . . . . . . . . . . . 13
123122a1i 11 . . . . . . . . . . . 12
12438, 44, 50, 56, 70, 123findcard2 7307 . . . . . . . . . . 11
125124com12 29 . . . . . . . . . 10
126125impr 603 . . . . . . . . 9
127 ffn 5550 . . . . . . . . . . . 12
1289, 127syl 16 . . . . . . . . . . 11
129 inss1 3521 . . . . . . . . . . . . . . 15
130 imass2 5199 . . . . . . . . . . . . . . 15
131129, 130ax-mp 8 . . . . . . . . . . . . . 14
132 nnuz 10477 . . . . . . . . . . . . . . . . . . . 20
133 1z 10267 . . . . . . . . . . . . . . . . . . . . 21
134 fnfvelrn 5826 . . . . . . . . . . . . . . . . . . . . 21
13559, 133, 134mp2an 654 . . . . . . . . . . . . . . . . . . . 20
136132, 135eqeltri 2474 . . . . . . . . . . . . . . . . . . 19
137 uzin2 12103 . . . . . . . . . . . . . . . . . . 19
138136, 137mpan2 653 . . . . . . . . . . . . . . . . . 18
139 uzn0 10457 . . . . . . . . . . . . . . . . . 18
140138, 139syl 16 . . . . . . . . . . . . . . . . 17
141 n0 3597 . . . . . . . . . . . . . . . . 17
142140, 141sylib 189 . . . . . . . . . . . . . . . 16
143 fnfun 5501 . . . . . . . . . . . . . . . . . . 19
144 inss2 3522 . . . . . . . . . . . . . . . . . . . 20
145 fndm 5503 . . . . . . . . . . . . . . . . . . . 20
146144, 145syl5sseqr 3357 . . . . . . . . . . . . . . . . . . 19
147 funfvima2 5933 . . . . . . . . . . . . . . . . . . 19
148143, 146, 147syl2anc 643 . . . . . . . . . . . . . . . . . 18
149 ne0i 3594 . . . . . . . . . . . . . . . . . 18
150148, 149syl6 31 . . . . . . . . . . . . . . . . 17
151150exlimdv 1643 . . . . . . . . . . . . . . . 16
152142, 151syl5 30 . . . . . . . . . . . . . . 15
153152imp 419 . . . . . . . . . . . . . 14
154 ssn0 3620 . . . . . . . . . . . . . 14
155131, 153, 154sylancr 645 . . . . . . . . . . . . 13
156 ssn0 3620 . . . . . . . . . . . . . 14
157156expcom 425 . . . . . . . . . . . . 13
158155, 157syl 16 . . . . . . . . . . . 12
159158rexlimdva 2790 . . . . . . . . . . 11
160128, 159syl 16 . . . . . . . . . 10
161160adantr 452 . . . . . . . . 9
162126, 161mpd 15 . . . . . . . 8
163162necomd 2650 . . . . . . 7
164163neneqd 2583 . . . . . 6
16532, 164sylan2b 462 . . . . 5
166165nrexdv 2769 . . . 4
167 0ex 4299 . . . . 5
168 zex 10247 . . . . . . . 8
169168pwex 4342 . . . . . . 7
170 frn 5556 . . . . . . . 8
17157, 170ax-mp 8 . . . . . . 7
172169, 171ssexi 4308 . . . . . 6
173172abrexex 5942 . . . . 5
174 elfi 7376 . . . . 5
175167, 173, 174mp2an 654 . . . 4
176166, 175sylnibr 297 . . 3
177 cmptop 17412 . . . . . 6
178 cmpfi 17425 . . . . . 6
179177, 178syl 16 . . . . 5
180179ibi 233 . . . 4
181 fveq2 5687 . . . . . . . 8
182181eleq2d 2471 . . . . . . 7
183182notbid 286 . . . . . 6
184 inteq 4013 . . . . . . . 8
185184neeq1d 2580 . . . . . . 7
186 n0 3597 . . . . . . 7
187185, 186syl6bb 253 . . . . . 6
188183, 187imbi12d 312 . . . . 5
189188rspccv 3009 . . . 4
190180, 189syl 16 . . 3
1911, 25, 176, 190syl3c 59 . 2
192 lmrel 17248 . . 3
193 r19.23v 2782 . . . . . 6
194193albii 1572 . . . . 5
195 fvex 5701 . . . . . . . 8
196 eleq2 2465 . . . . . . . 8
197195, 196ceqsalv 2942 . . . . . . 7
198197ralbii 2690 . . . . . 6
199 ralcom4 2934 . . . . . 6
200198, 199bitr3i 243 . . . . 5
201 vex 2919 . . . . . 6
202201elintab 4021 . . . . 5
203194, 200, 2023bitr4i 269 . . . 4
204 eqid 2404 . . . . . . . . . . 11
205 imaeq2 5158 . . . . . . . . . . . . . 14
206205fveq2d 5691 . . . . . . . . . . . . 13
207206eqeq2d 2415 . . . . . . . . . . . 12
208207rspcev 3012 . . . . . . . . . . 11
209136, 204, 208mp2an 654 . . . . . . . . . 10
210 fvex 5701 . . . . . . . . . . 11
211 eqeq1 2410 . . . . . . . . . . . 12
212211rexbidv 2687 . . . . . . . . . . 11
213210, 212elab 3042 . . . . . . . . . 10
214209, 213mpbir 201 . . . . . . . . 9
215 intss1 4025 . . . . . . . . 9
216214, 215ax-mp 8 . . . . . . . 8
217 imassrn 5175 . . . . . . . . . . 11
218217, 14syl5ss 3319 . . . . . . . . . 10
21916clsss3 17078 . . . . . . . . . 10
2207, 218, 219syl2anc 643 . . . . . . . . 9
221220, 13sseqtr4d 3345 . . . . . . . 8
222216, 221syl5ss 3319 . . . . . . 7
223222sselda 3308 . . . . . 6
224203, 223sylan2b 462 . . . . 5
225 heibor1.5 . . . . . . . . . . . 12
226133a1i 11 . . . . . . . . . . . . 13
227132, 4, 226iscau3 19184 . . . . . . . . . . . 12
228225, 227mpbid 202 . . . . . . . . . . 11
229228simprd 450 . . . . . . . . . 10
230 simp3 959 . . . . . . . . . . . . 13
231230ralimi 2741 . . . . . . . . . . . 12
232231reximi 2773 . . . . . . . . . . 11
233232ralimi 2741 . . . . . . . . . 10
234229, 233syl 16 . . . . . . . . 9
235234adantr 452 . . . . . . . 8
236 rphalfcl 10592 . . . . . . . 8
237 breq2 4176 . . . . . . . . . . 11
2382372ralbidv 2708 . . . . . . . . . 10
239238rexbidv 2687 . . . . . . . . 9
240239rspccva 3011 . . . . . . . 8
241235, 236, 240syl2an 464 . . . . . . 7
242 ffun 5552 . . . . . . . . . . . . 13
2439, 242syl 16 . . . . . . . . . . . 12
244243ad2antrr 707 . . . . . . . . . . 11
2457ad2antrr 707 . . . . . . . . . . . 12
246 imassrn 5175 . . . . . . . . . . . . . 14
247246, 14syl5ss 3319 . . . . . . . . . . . . 13
248247ad2antrr 707 . . . . . . . . . . . 12
249 nnz 10259 . . . . . . . . . . . . . . 15
250 fnfvelrn 5826 . . . . . . . . . . . . . . 15
25159, 249, 250sylancr 645 . . . . . . . . . . . . . 14
252251ad2antll 710 . . . . . . . . . . . . 13
253 simplr 732 . . . . . . . . . . . . 13
254 imaeq2 5158 . . . . . . . . . . . . . . . 16
255254fveq2d 5691 . . . . . . . . . . . . . . 15
256255eleq2d 2471 . . . . . . . . . . . . . 14
257256rspcv 3008 . . . . . . . . . . . . 13
258252, 253, 257sylc 58 . . . . . . . . . . . 12
2594ad2antrr 707 . . . . . . . . . . . . 13
260224adantr 452 . . . . . . . . . . . . 13
261236ad2antrl 709 . . . . . . . . . . . . . 14
262261rpxrd 10605 . . . . . . . . . . . . 13
2635blopn 18483 . . . . . . . . . . . . 13
264259, 260, 262, 263syl3anc 1184 . . . . . . . . . . . 12
265 blcntr 18396 . . . . . . . . . . . . 13
266259, 260, 261, 265syl3anc 1184 . . . . . . . . . . . 12
26716clsndisj 17094 . . . . . . . . . . . 12
268245, 248, 258, 264, 266, 267syl32anc 1192 . . . . . . . . . . 11
269 n0 3597 . . . . . . . . . . . 12
270 inss2 3522 . . . . . . . . . . . . . . . . 17
271270sseli 3304 . . . . . . . . . . . . . . . 16
272 fvelima 5737 . . . . . . . . . . . . . . . 16
273271, 272sylan2 461 . . . . . . . . . . . . . . 15
274 inss1 3521 . . . . . . . . . . . . . . . . . . 19
275274sseli 3304 . . . . . . . . . . . . . . . . . 18
276275adantl 453 . . . . . . . . . . . . . . . . 17
277 eleq1a 2473 . . . . . . . . . . . . . . . . 17
278276, 277syl 16 . . . . . . . . . . . . . . . 16
279278reximdv 2777 . . . . . . . . . . . . . . 15
280273, 279mpd 15 . . . . . . . . . . . . . 14
281280ex 424 . . . . . . . . . . . . 13
282281exlimdv 1643 . . . . . . . . . . . 12
283269, 282syl5bi 209 . . . . . . . . . . 11
284244, 268, 283sylc 58 . . . . . . . . . 10
285 r19.29 2806 . . . . . . . . . . 11
286 uznnssnn 10480 . . . . . . . . . . . . . 14
287286ad2antll 710 . . . . . . . . . . . . 13
288 simprlr 740 . . . . . . . . . . . . . . . . . . . . . . 23
2894ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . 24
290 simplrl 737 . . . . . . . . . . . . . . . . . . . . . . . . . 26
291290, 236syl 16 . . . . . . . . . . . . . . . . . . . . . . . . 25
292291rpxrd 10605 . . . . . . . . . . . . . . . . . . . . . . . 24
293 simpllr 736 . . . . . . . . . . . . . . . . . . . . . . . 24
2949ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . 25
295132uztrn2 10459 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
296295ad2ant2lr 729 . . . . . . . . . . . . . . . . . . . . . . . . . 26
297296ad2ant2lr 729 . . . . . . . . . . . . . . . . . . . . . . . . 25
298294, 297ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . 24
299 elbl3 18375 . . . . . . . . . . . . . . . . . . . . . . . 24
300289, 292, 293, 298, 299syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . . 23
301288, 300mpbid 202 . . . . . . . . . . . . . . . . . . . . . 22
3022ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . 24
303 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . 26
304132uztrn2 10459 . . . . . . . . . . . . . . . . . . . . . . . . . 26
305297, 303, 304syl2anc 643 . . . . . . . . . . . . . . . . . . . . . . . . 25
306294, 305ffvelrnd 5830 . . . . . . . . . . . . . . . . . . . . . . . 24
307 metcl 18315 . . . . . . . . . . . . . . . . . . . . . . . 24
308302, 298, 306, 307syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23
309 metcl 18315 . . . . . . . . . . . . . . . . . . . . . . . 24
310302, 298, 293, 309syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . . 23
311291rpred 10604 . . . . . . . . . . . . . . . . . . . . . . 23
312 lt2add 9469 . . . . . . . . . . . . . . . . . . . . . . 23
313308, 310, 311, 311, 312syl22anc 1185 . . . . . . . . . . . . . . . . . . . . . 22
314301, 313mpan2d 656 . . . . . . . . . . . . . . . . . . . . 21
315290rpcnd 10606 . . . . . . . . . . . . . . . . . . . . . . 23
3163152halvesd 10169 . . . . . . . . . . . . . . . . . . . . . 22
317316breq2d 4184 . . . . . . . . . . . . . . . . . . . . 21
318314, 317sylibd 206 . . . . . . . . . . . . . . . . . . . 20
319 mettri2 18324 . . . . . . . . . . . . . . . . . . . . . 22
320302, 298, 306, 293, 319syl13anc 1186 . . . . . . . . . . . . . . . . . . . . 21
321 metcl 18315 . . . . . . . . . . . . . . . . . . . . . . 23
322302, 306, 293, 321syl3anc 1184 . . . . . . . . . . . . . . . . . . . . . 22
323308, 310readdcld 9071 . . . . . . . . . . . . . . . . . . . . . 22
324290rpred 10604 . . . . . . . . . . . . . . . . . . . . . 22
325 lelttr 9121 . . . . . . . . . . . . . . . . . . . . . 22
326322, 323, 324, 325syl3anc 1184 . . . . . . . . . . . . . . . . . . . . 21
327320, 326mpand 657 . . . . . . . . . . . . . . . . . . . 20
328318, 327syld 42 . . . . . . . . . . . . . . . . . . 19
329328anassrs 630 . . . . . . . . . . . . . . . . . 18
330329ralimdva 2744 . . . . . . . . . . . . . . . . 17
331330expr 599 . . . . . . . . . . . . . . . 16
332331com23 74 . . . . . . . . . . . . . . 15
333332imp3a 421 . . . . . . . . . . . . . 14
334333reximdva 2778 . . . . . . . . . . . . 13
335 ssrexv 3368 . . . . . . . . . . . . 13
336287, 334, 335sylsyld 54 . . . . . . . . . . . 12
337224, 336syldanl 26303 . . . . . . . . . . 11