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 𝑋 = 𝐽
Assertion bwth ( ( 𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin ) → ∃ 𝑥𝑋 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝐴 ) )

Proof

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