Metamath Proof Explorer

Theorem bwth

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)

Ref Expression
Hypothesis bwt2.1 ⊢ X = ⋃ J
Assertion bwth ⊢ J ∈ Comp ∧ A ⊆ X ∧ ¬ A ∈ Fin → ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A

Proof

Step Hyp Ref Expression
1 bwt2.1 ⊢ X = ⋃ J
2 pm3.24 ⊢ ¬ A ∩ b ∈ Fin ∧ ¬ A ∩ b ∈ Fin
3 2 a1i ⊢ b ∈ z → ¬ A ∩ b ∈ Fin ∧ ¬ A ∩ b ∈ Fin
4 3 nrex ⊢ ¬ ∃ b ∈ z A ∩ b ∈ Fin ∧ ¬ A ∩ b ∈ Fin
5 r19.29 ⊢ ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin → ∃ b ∈ z A ∩ b ∈ Fin ∧ ¬ A ∩ b ∈ Fin
6 4 5 mto ⊢ ¬ ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
7 6 a1i ⊢ z ∈ 𝒫 J ∩ Fin → ¬ ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
8 7 nrex ⊢ ¬ ∃ z ∈ 𝒫 J ∩ Fin ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
9 ralnex ⊢ ∀ x ∈ X ¬ x ∈ limPt ⁡ J ⁡ A ↔ ¬ ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A
10 cmptop ⊢ J ∈ Comp → J ∈ Top
11 1 islp3 ⊢ J ∈ Top ∧ A ⊆ X ∧ x ∈ X → x ∈ limPt ⁡ J ⁡ A ↔ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
12 11 3expa ⊢ J ∈ Top ∧ A ⊆ X ∧ x ∈ X → x ∈ limPt ⁡ J ⁡ A ↔ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
13 12 notbid ⊢ J ∈ Top ∧ A ⊆ X ∧ x ∈ X → ¬ x ∈ limPt ⁡ J ⁡ A ↔ ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
14 13 ralbidva ⊢ J ∈ Top ∧ A ⊆ X → ∀ x ∈ X ¬ x ∈ limPt ⁡ J ⁡ A ↔ ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
15 10 14 sylan ⊢ J ∈ Comp ∧ A ⊆ X → ∀ x ∈ X ¬ x ∈ limPt ⁡ J ⁡ A ↔ ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
16 9 15 bitr3id ⊢ J ∈ Comp ∧ A ⊆ X → ¬ ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A ↔ ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
17 rexanali ⊢ ∃ b ∈ J x ∈ b ∧ ¬ b ∩ A ∖ x ≠ ∅ ↔ ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅
18 nne ⊢ ¬ b ∩ A ∖ x ≠ ∅ ↔ b ∩ A ∖ x = ∅
19 vex ⊢ x ∈ V
20 sneq ⊢ o = x → o = x
21 20 difeq2d ⊢ o = x → A ∖ o = A ∖ x
22 21 ineq2d ⊢ o = x → b ∩ A ∖ o = b ∩ A ∖ x
23 22 eqeq1d ⊢ o = x → b ∩ A ∖ o = ∅ ↔ b ∩ A ∖ x = ∅
24 19 23 spcev ⊢ b ∩ A ∖ x = ∅ → ∃ o b ∩ A ∖ o = ∅
25 18 24 sylbi ⊢ ¬ b ∩ A ∖ x ≠ ∅ → ∃ o b ∩ A ∖ o = ∅
26 25 anim2i ⊢ x ∈ b ∧ ¬ b ∩ A ∖ x ≠ ∅ → x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅
27 26 reximi ⊢ ∃ b ∈ J x ∈ b ∧ ¬ b ∩ A ∖ x ≠ ∅ → ∃ b ∈ J x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅
28 17 27 sylbir ⊢ ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅ → ∃ b ∈ J x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅
29 28 ralimi ⊢ ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅ → ∀ x ∈ X ∃ b ∈ J x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅
30 1 cmpcov2 ⊢ J ∈ Comp ∧ ∀ x ∈ X ∃ b ∈ J x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅ → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
31 30 ex ⊢ J ∈ Comp → ∀ x ∈ X ∃ b ∈ J x ∈ b ∧ ∃ o b ∩ A ∖ o = ∅ → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
32 29 31 syl5 ⊢ J ∈ Comp → ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅ → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
33 32 adantr ⊢ J ∈ Comp ∧ A ⊆ X → ∀ x ∈ X ¬ ∀ b ∈ J x ∈ b → b ∩ A ∖ x ≠ ∅ → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
34 16 33 sylbid ⊢ J ∈ Comp ∧ A ⊆ X → ¬ ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
35 34 3adant3 ⊢ J ∈ Comp ∧ A ⊆ X ∧ ¬ A ∈ Fin → ¬ ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅
36 elinel2 ⊢ z ∈ 𝒫 J ∩ Fin → z ∈ Fin
37 sseq2 ⊢ X = ⋃ z → A ⊆ X ↔ A ⊆ ⋃ z
38 37 biimpac ⊢ A ⊆ X ∧ X = ⋃ z → A ⊆ ⋃ z
39 infssuni ⊢ ¬ A ∈ Fin ∧ z ∈ Fin ∧ A ⊆ ⋃ z → ∃ b ∈ z ¬ A ∩ b ∈ Fin
40 39 3expa ⊢ ¬ A ∈ Fin ∧ z ∈ Fin ∧ A ⊆ ⋃ z → ∃ b ∈ z ¬ A ∩ b ∈ Fin
41 40 ancoms ⊢ A ⊆ ⋃ z ∧ ¬ A ∈ Fin ∧ z ∈ Fin → ∃ b ∈ z ¬ A ∩ b ∈ Fin
42 38 41 sylan ⊢ A ⊆ X ∧ X = ⋃ z ∧ ¬ A ∈ Fin ∧ z ∈ Fin → ∃ b ∈ z ¬ A ∩ b ∈ Fin
43 42 an42s ⊢ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ∈ Fin ∧ X = ⋃ z → ∃ b ∈ z ¬ A ∩ b ∈ Fin
44 43 anassrs ⊢ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ∈ Fin ∧ X = ⋃ z → ∃ b ∈ z ¬ A ∩ b ∈ Fin
45 36 44 sylanl2 ⊢ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ∈ 𝒫 J ∩ Fin ∧ X = ⋃ z → ∃ b ∈ z ¬ A ∩ b ∈ Fin
46 0fi ⊢ ∅ ∈ Fin
47 eleq1 ⊢ b ∩ A ∖ o = ∅ → b ∩ A ∖ o ∈ Fin ↔ ∅ ∈ Fin
48 46 47 mpbiri ⊢ b ∩ A ∖ o = ∅ → b ∩ A ∖ o ∈ Fin
49 snfi ⊢ o ∈ Fin
50 unfi ⊢ b ∩ A ∖ o ∈ Fin ∧ o ∈ Fin → b ∩ A ∖ o ∪ o ∈ Fin
51 48 49 50 sylancl ⊢ b ∩ A ∖ o = ∅ → b ∩ A ∖ o ∪ o ∈ Fin
52 ssun1 ⊢ b ⊆ b ∪ o
53 ssun1 ⊢ A ⊆ A ∪ o
54 undif1 ⊢ A ∖ o ∪ o = A ∪ o
55 53 54 sseqtrri ⊢ A ⊆ A ∖ o ∪ o
56 ss2in ⊢ b ⊆ b ∪ o ∧ A ⊆ A ∖ o ∪ o → b ∩ A ⊆ b ∪ o ∩ A ∖ o ∪ o
57 52 55 56 mp2an ⊢ b ∩ A ⊆ b ∪ o ∩ A ∖ o ∪ o
58 incom ⊢ A ∩ b = b ∩ A
59 undir ⊢ b ∩ A ∖ o ∪ o = b ∪ o ∩ A ∖ o ∪ o
60 57 58 59 3sstr4i ⊢ A ∩ b ⊆ b ∩ A ∖ o ∪ o
61 ssfi ⊢ b ∩ A ∖ o ∪ o ∈ Fin ∧ A ∩ b ⊆ b ∩ A ∖ o ∪ o → A ∩ b ∈ Fin
62 51 60 61 sylancl ⊢ b ∩ A ∖ o = ∅ → A ∩ b ∈ Fin
63 62 exlimiv ⊢ ∃ o b ∩ A ∖ o = ∅ → A ∩ b ∈ Fin
64 63 ralimi ⊢ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅ → ∀ b ∈ z A ∩ b ∈ Fin
65 45 64 anim12ci ⊢ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ∈ 𝒫 J ∩ Fin ∧ X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅ → ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
66 65 expl ⊢ A ⊆ X ∧ ¬ A ∈ Fin ∧ z ∈ 𝒫 J ∩ Fin → X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅ → ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
67 66 reximdva ⊢ A ⊆ X ∧ ¬ A ∈ Fin → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅ → ∃ z ∈ 𝒫 J ∩ Fin ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
68 67 3adant1 ⊢ J ∈ Comp ∧ A ⊆ X ∧ ¬ A ∈ Fin → ∃ z ∈ 𝒫 J ∩ Fin X = ⋃ z ∧ ∀ b ∈ z ∃ o b ∩ A ∖ o = ∅ → ∃ z ∈ 𝒫 J ∩ Fin ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
69 35 68 syld ⊢ J ∈ Comp ∧ A ⊆ X ∧ ¬ A ∈ Fin → ¬ ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A → ∃ z ∈ 𝒫 J ∩ Fin ∀ b ∈ z A ∩ b ∈ Fin ∧ ∃ b ∈ z ¬ A ∩ b ∈ Fin
70 8 69 mt3i ⊢ J ∈ Comp ∧ A ⊆ X ∧ ¬ A ∈ Fin → ∃ x ∈ X x ∈ limPt ⁡ J ⁡ A