Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  bwth Structured version   Visualization version   Unicode version

Theorem bwth 20418
 Description: The glorious Bolzano-Weierstrass theorem. The first general topology theorem ever proved. The first mention of this theorem can be found in a course by Weierstrass from 1865. In his course Weierstrass called it a lemma. He didn't know how famous this theorem would be. He used a Euclidean space instead of a general compact space. And he was not aware of the Heine-Borel property. But the concepts of neighborhood and limit point were already there although not precisely defined. Cantor was one of his students. He published and used the theorem in an article from 1872. The rest of the general topology followed from that. (Contributed by FL, 2-Aug-2009.) (Revised by Mario Carneiro, 15-Dec-2013.) Revised by BL to significantly shorten the proof and avoid infinity, regularity, and choice. (Revised by Brendan Leahy, 26-Dec-2018.)
Hypothesis
Ref Expression
bwt2.1
Assertion
Ref Expression
bwth
Distinct variable groups:   ,   ,   ,

Proof of Theorem bwth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pm3.24 892 . . . . . . 7
21a1i 11 . . . . . 6
32nrex 2841 . . . . 5
4 r19.29 2924 . . . . 5
53, 4mto 180 . . . 4
65a1i 11 . . 3
76nrex 2841 . 2
8 ralnex 2833 . . . . . 6
9 cmptop 20403 . . . . . . 7
10 bwt2.1 . . . . . . . . . . 11
1110islp3 20155 . . . . . . . . . 10
12113expa 1207 . . . . . . . . 9
1312notbid 296 . . . . . . . 8
1413ralbidva 2823 . . . . . . 7
159, 14sylan 474 . . . . . 6
168, 15syl5bbr 263 . . . . 5
17 rexanali 2839 . . . . . . . . 9
18 nne 2627 . . . . . . . . . . . 12
19 vex 3047 . . . . . . . . . . . . 13
20 sneq 3977 . . . . . . . . . . . . . . . 16
2120difeq2d 3550 . . . . . . . . . . . . . . 15
2221ineq2d 3633 . . . . . . . . . . . . . 14
2322eqeq1d 2452 . . . . . . . . . . . . 13
2419, 23spcev 3140 . . . . . . . . . . . 12
2518, 24sylbi 199 . . . . . . . . . . 11
2625anim2i 572 . . . . . . . . . 10
2726reximi 2854 . . . . . . . . 9
2817, 27sylbir 217 . . . . . . . 8
2928ralimi 2780 . . . . . . 7
3010cmpcov2 20398 . . . . . . . 8
3130ex 436 . . . . . . 7
3229, 31syl5 33 . . . . . 6
3332adantr 467 . . . . 5
3416, 33sylbid 219 . . . 4
36 inss2 3652 . . . . . . . . 9
3736sseli 3427 . . . . . . . 8
38 sseq2 3453 . . . . . . . . . . . 12
3938biimpac 489 . . . . . . . . . . 11
40 infssuni 7862 . . . . . . . . . . . . 13
41403expa 1207 . . . . . . . . . . . 12
4241ancoms 455 . . . . . . . . . . 11
4339, 42sylan 474 . . . . . . . . . 10
4443an42s 835 . . . . . . . . 9
4544anassrs 653 . . . . . . . 8
4637, 45sylanl2 656 . . . . . . 7
47 0fin 7796 . . . . . . . . . . . 12
48 eleq1 2516 . . . . . . . . . . . 12
4947, 48mpbiri 237 . . . . . . . . . . 11
50 snfi 7647 . . . . . . . . . . 11
51 unfi 7835 . . . . . . . . . . 11
5249, 50, 51sylancl 667 . . . . . . . . . 10
53 ssun1 3596 . . . . . . . . . . . 12
54 ssun1 3596 . . . . . . . . . . . . 13
55 undif1 3841 . . . . . . . . . . . . 13
5654, 55sseqtr4i 3464 . . . . . . . . . . . 12
57 ss2in 3658 . . . . . . . . . . . 12
5853, 56, 57mp2an 677 . . . . . . . . . . 11
59 incom 3624 . . . . . . . . . . 11
60 undir 3691 . . . . . . . . . . 11
6158, 59, 603sstr4i 3470 . . . . . . . . . 10
62 ssfi 7789 . . . . . . . . . 10
6352, 61, 62sylancl 667 . . . . . . . . 9
6463exlimiv 1775 . . . . . . . 8
6564ralimi 2780 . . . . . . 7
6646, 65anim12ci 570 . . . . . 6
6766expl 623 . . . . 5
6867reximdva 2861 . . . 4