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

Theorem bwth 23358
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 ((𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
Distinct variable groups:   𝑥,𝐴   𝑥,𝐽   𝑥,𝑋

Proof of Theorem bwth
Dummy variables 𝑜 𝑏 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 pm3.24 401 . . . . . . 7 ¬ ((𝐴𝑏) ∈ Fin ∧ ¬ (𝐴𝑏) ∈ Fin)
21a1i 11 . . . . . 6 (𝑏𝑧 → ¬ ((𝐴𝑏) ∈ Fin ∧ ¬ (𝐴𝑏) ∈ Fin))
32nrex 3063 . . . . 5 ¬ ∃𝑏𝑧 ((𝐴𝑏) ∈ Fin ∧ ¬ (𝐴𝑏) ∈ Fin)
4 r19.29 3103 . . . . 5 ((∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin) → ∃𝑏𝑧 ((𝐴𝑏) ∈ Fin ∧ ¬ (𝐴𝑏) ∈ Fin))
53, 4mto 196 . . . 4 ¬ (∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
65a1i 11 . . 3 (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → ¬ (∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin))
76nrex 3063 . 2 ¬ ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
8 ralnex 3061 . . . . . 6 (∀𝑥𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
9 cmptop 23343 . . . . . . 7 (𝐽 ∈ Comp → 𝐽 ∈ Top)
10 bwt2.1 . . . . . . . . . . 11 𝑋 = 𝐽
1110islp3 23094 . . . . . . . . . 10 ((𝐽 ∈ Top ∧ 𝐴𝑋𝑥𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
12113expa 1115 . . . . . . . . 9 (((𝐽 ∈ Top ∧ 𝐴𝑋) ∧ 𝑥𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
1312notbid 317 . . . . . . . 8 (((𝐽 ∈ Top ∧ 𝐴𝑋) ∧ 𝑥𝑋) → (¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
1413ralbidva 3165 . . . . . . 7 ((𝐽 ∈ Top ∧ 𝐴𝑋) → (∀𝑥𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
159, 14sylan 578 . . . . . 6 ((𝐽 ∈ Comp ∧ 𝐴𝑋) → (∀𝑥𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
168, 15bitr3id 284 . . . . 5 ((𝐽 ∈ Comp ∧ 𝐴𝑋) → (¬ ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
17 rexanali 3091 . . . . . . . . 9 (∃𝑏𝐽 (𝑥𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) ↔ ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))
18 nne 2933 . . . . . . . . . . . 12 (¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅)
19 vex 3465 . . . . . . . . . . . . 13 𝑥 ∈ V
20 sneq 4640 . . . . . . . . . . . . . . . 16 (𝑜 = 𝑥 → {𝑜} = {𝑥})
2120difeq2d 4118 . . . . . . . . . . . . . . 15 (𝑜 = 𝑥 → (𝐴 ∖ {𝑜}) = (𝐴 ∖ {𝑥}))
2221ineq2d 4210 . . . . . . . . . . . . . 14 (𝑜 = 𝑥 → (𝑏 ∩ (𝐴 ∖ {𝑜})) = (𝑏 ∩ (𝐴 ∖ {𝑥})))
2322eqeq1d 2727 . . . . . . . . . . . . 13 (𝑜 = 𝑥 → ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅))
2419, 23spcev 3590 . . . . . . . . . . . 12 ((𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)
2518, 24sylbi 216 . . . . . . . . . . 11 (¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)
2625anim2i 615 . . . . . . . . . 10 ((𝑥𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
2726reximi 3073 . . . . . . . . 9 (∃𝑏𝐽 (𝑥𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏𝐽 (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
2817, 27sylbir 234 . . . . . . . 8 (¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏𝐽 (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
2928ralimi 3072 . . . . . . 7 (∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∀𝑥𝑋𝑏𝐽 (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
3010cmpcov2 23338 . . . . . . . 8 ((𝐽 ∈ Comp ∧ ∀𝑥𝑋𝑏𝐽 (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
3130ex 411 . . . . . . 7 (𝐽 ∈ Comp → (∀𝑥𝑋𝑏𝐽 (𝑥𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
3229, 31syl5 34 . . . . . 6 (𝐽 ∈ Comp → (∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
3332adantr 479 . . . . 5 ((𝐽 ∈ Comp ∧ 𝐴𝑋) → (∀𝑥𝑋 ¬ ∀𝑏𝐽 (𝑥𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
3416, 33sylbid 239 . . . 4 ((𝐽 ∈ Comp ∧ 𝐴𝑋) → (¬ ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
35343adant3 1129 . . 3 ((𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
36 elinel2 4194 . . . . . . . 8 (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → 𝑧 ∈ Fin)
37 sseq2 4003 . . . . . . . . . . . 12 (𝑋 = 𝑧 → (𝐴𝑋𝐴 𝑧))
3837biimpac 477 . . . . . . . . . . 11 ((𝐴𝑋𝑋 = 𝑧) → 𝐴 𝑧)
39 infssuni 9369 . . . . . . . . . . . . 13 ((¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ∧ 𝐴 𝑧) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
40393expa 1115 . . . . . . . . . . . 12 (((¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin) ∧ 𝐴 𝑧) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
4140ancoms 457 . . . . . . . . . . 11 ((𝐴 𝑧 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
4238, 41sylan 578 . . . . . . . . . 10 (((𝐴𝑋𝑋 = 𝑧) ∧ (¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
4342an42s 659 . . . . . . . . 9 (((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ (𝑧 ∈ Fin ∧ 𝑋 = 𝑧)) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
4443anassrs 466 . . . . . . . 8 ((((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ Fin) ∧ 𝑋 = 𝑧) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
4536, 44sylanl2 679 . . . . . . 7 ((((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = 𝑧) → ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)
46 0fin 9196 . . . . . . . . . . . 12 ∅ ∈ Fin
47 eleq1 2813 . . . . . . . . . . . 12 ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ↔ ∅ ∈ Fin))
4846, 47mpbiri 257 . . . . . . . . . . 11 ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin)
49 snfi 9069 . . . . . . . . . . 11 {𝑜} ∈ Fin
50 unfi 9197 . . . . . . . . . . 11 (((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ∧ {𝑜} ∈ Fin) → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin)
5148, 49, 50sylancl 584 . . . . . . . . . 10 ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin)
52 ssun1 4170 . . . . . . . . . . . 12 𝑏 ⊆ (𝑏 ∪ {𝑜})
53 ssun1 4170 . . . . . . . . . . . . 13 𝐴 ⊆ (𝐴 ∪ {𝑜})
54 undif1 4477 . . . . . . . . . . . . 13 ((𝐴 ∖ {𝑜}) ∪ {𝑜}) = (𝐴 ∪ {𝑜})
5553, 54sseqtrri 4014 . . . . . . . . . . . 12 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜})
56 ss2in 4235 . . . . . . . . . . . 12 ((𝑏 ⊆ (𝑏 ∪ {𝑜}) ∧ 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜})) → (𝑏𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜})))
5752, 55, 56mp2an 690 . . . . . . . . . . 11 (𝑏𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜}))
58 incom 4199 . . . . . . . . . . 11 (𝐴𝑏) = (𝑏𝐴)
59 undir 4275 . . . . . . . . . . 11 ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) = ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜}))
6057, 58, 593sstr4i 4020 . . . . . . . . . 10 (𝐴𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜})
61 ssfi 9198 . . . . . . . . . 10 ((((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin ∧ (𝐴𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜})) → (𝐴𝑏) ∈ Fin)
6251, 60, 61sylancl 584 . . . . . . . . 9 ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴𝑏) ∈ Fin)
6362exlimiv 1925 . . . . . . . 8 (∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴𝑏) ∈ Fin)
6463ralimi 3072 . . . . . . 7 (∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ∀𝑏𝑧 (𝐴𝑏) ∈ Fin)
6545, 64anim12ci 612 . . . . . 6 (((((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = 𝑧) ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin))
6665expl 456 . . . . 5 (((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) → ((𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)))
6766reximdva 3157 . . . 4 ((𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)))
68673adant1 1127 . . 3 ((𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = 𝑧 ∧ ∀𝑏𝑧𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)))
6935, 68syld 47 . 2 ((𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏𝑧 (𝐴𝑏) ∈ Fin ∧ ∃𝑏𝑧 ¬ (𝐴𝑏) ∈ Fin)))
707, 69mt3i 149 1 ((𝐽 ∈ Comp ∧ 𝐴𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 394  w3a 1084   = wceq 1533  wex 1773  wcel 2098  wne 2929  wral 3050  wrex 3059  cdif 3941  cun 3942  cin 3943  wss 3944  c0 4322  𝒫 cpw 4604  {csn 4630   cuni 4909  cfv 6549  Fincfn 8964  Topctop 22839  limPtclp 23082  Compccmp 23334
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2166  ax-ext 2696  ax-rep 5286  ax-sep 5300  ax-nul 5307  ax-pow 5365  ax-pr 5429  ax-un 7741
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3or 1085  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-mo 2528  df-eu 2557  df-clab 2703  df-cleq 2717  df-clel 2802  df-nfc 2877  df-ne 2930  df-ral 3051  df-rex 3060  df-reu 3364  df-rab 3419  df-v 3463  df-sbc 3774  df-csb 3890  df-dif 3947  df-un 3949  df-in 3951  df-ss 3961  df-pss 3964  df-nul 4323  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-op 4637  df-uni 4910  df-int 4951  df-iun 4999  df-iin 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-tr 5267  df-id 5576  df-eprel 5582  df-po 5590  df-so 5591  df-fr 5633  df-we 5635  df-xp 5684  df-rel 5685  df-cnv 5686  df-co 5687  df-dm 5688  df-rn 5689  df-res 5690  df-ima 5691  df-ord 6374  df-on 6375  df-lim 6376  df-suc 6377  df-iota 6501  df-fun 6551  df-fn 6552  df-f 6553  df-f1 6554  df-fo 6555  df-f1o 6556  df-fv 6557  df-om 7872  df-1o 8487  df-en 8965  df-fin 8968  df-top 22840  df-cld 22967  df-ntr 22968  df-cls 22969  df-lp 23084  df-cmp 23335
This theorem is referenced by:  poimirlem30  37251  fourierdlem42  45672
  Copyright terms: Public domain W3C validator