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 = U. J
Assertion bwth 
|- ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> E. x e. X x e. ( ( limPt ` J ) ` A ) )

Proof

Step Hyp Ref Expression
1 bwt2.1 
 |-  X = U. J
2 pm3.24 
 |-  -. ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin )
3 2 a1i 
 |-  ( b e. z -> -. ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) )
4 3 nrex 
 |-  -. E. b e. z ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin )
5 r19.29 
 |-  ( ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) -> E. b e. z ( ( A i^i b ) e. Fin /\ -. ( A i^i b ) e. Fin ) )
6 4 5 mto 
 |-  -. ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin )
7 6 a1i 
 |-  ( z e. ( ~P J i^i Fin ) -> -. ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) )
8 7 nrex 
 |-  -. E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin )
9 ralnex 
 |-  ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> -. E. x e. X x e. ( ( limPt ` J ) ` A ) )
10 cmptop 
 |-  ( J e. Comp -> J e. Top )
11 1 islp3 
 |-  ( ( J e. Top /\ A C_ X /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` A ) <-> A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
12 11 3expa 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` A ) <-> A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
13 12 notbid 
 |-  ( ( ( J e. Top /\ A C_ X ) /\ x e. X ) -> ( -. x e. ( ( limPt ` J ) ` A ) <-> -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
14 13 ralbidva 
 |-  ( ( J e. Top /\ A C_ X ) -> ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
15 10 14 sylan 
 |-  ( ( J e. Comp /\ A C_ X ) -> ( A. x e. X -. x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
16 9 15 bitr3id 
 |-  ( ( J e. Comp /\ A C_ X ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) <-> A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) ) )
17 rexanali 
 |-  ( E. b e. J ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) <-> -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) )
18 nne 
 |-  ( -. ( b i^i ( A \ { x } ) ) =/= (/) <-> ( b i^i ( A \ { x } ) ) = (/) )
19 vex 
 |-  x e. _V
20 sneq 
 |-  ( o = x -> { o } = { x } )
21 20 difeq2d 
 |-  ( o = x -> ( A \ { o } ) = ( A \ { x } ) )
22 21 ineq2d 
 |-  ( o = x -> ( b i^i ( A \ { o } ) ) = ( b i^i ( A \ { x } ) ) )
23 22 eqeq1d 
 |-  ( o = x -> ( ( b i^i ( A \ { o } ) ) = (/) <-> ( b i^i ( A \ { x } ) ) = (/) ) )
24 19 23 spcev 
 |-  ( ( b i^i ( A \ { x } ) ) = (/) -> E. o ( b i^i ( A \ { o } ) ) = (/) )
25 18 24 sylbi 
 |-  ( -. ( b i^i ( A \ { x } ) ) =/= (/) -> E. o ( b i^i ( A \ { o } ) ) = (/) )
26 25 anim2i 
 |-  ( ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) -> ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) )
27 26 reximi 
 |-  ( E. b e. J ( x e. b /\ -. ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) )
28 17 27 sylbir 
 |-  ( -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) )
29 28 ralimi 
 |-  ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) )
30 1 cmpcov2 
 |-  ( ( J e. Comp /\ A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) )
31 30 ex 
 |-  ( J e. Comp -> ( A. x e. X E. b e. J ( x e. b /\ E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) )
32 29 31 syl5 
 |-  ( J e. Comp -> ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) )
33 32 adantr 
 |-  ( ( J e. Comp /\ A C_ X ) -> ( A. x e. X -. A. b e. J ( x e. b -> ( b i^i ( A \ { x } ) ) =/= (/) ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) )
34 16 33 sylbid 
 |-  ( ( J e. Comp /\ A C_ X ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) )
35 34 3adant3 
 |-  ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) ) )
36 elinel2 
 |-  ( z e. ( ~P J i^i Fin ) -> z e. Fin )
37 sseq2 
 |-  ( X = U. z -> ( A C_ X <-> A C_ U. z ) )
38 37 biimpac 
 |-  ( ( A C_ X /\ X = U. z ) -> A C_ U. z )
39 infssuni 
 |-  ( ( -. A e. Fin /\ z e. Fin /\ A C_ U. z ) -> E. b e. z -. ( A i^i b ) e. Fin )
40 39 3expa 
 |-  ( ( ( -. A e. Fin /\ z e. Fin ) /\ A C_ U. z ) -> E. b e. z -. ( A i^i b ) e. Fin )
41 40 ancoms 
 |-  ( ( A C_ U. z /\ ( -. A e. Fin /\ z e. Fin ) ) -> E. b e. z -. ( A i^i b ) e. Fin )
42 38 41 sylan 
 |-  ( ( ( A C_ X /\ X = U. z ) /\ ( -. A e. Fin /\ z e. Fin ) ) -> E. b e. z -. ( A i^i b ) e. Fin )
43 42 an42s 
 |-  ( ( ( A C_ X /\ -. A e. Fin ) /\ ( z e. Fin /\ X = U. z ) ) -> E. b e. z -. ( A i^i b ) e. Fin )
44 43 anassrs 
 |-  ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. Fin ) /\ X = U. z ) -> E. b e. z -. ( A i^i b ) e. Fin )
45 36 44 sylanl2 
 |-  ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) /\ X = U. z ) -> E. b e. z -. ( A i^i b ) e. Fin )
46 0fin 
 |-  (/) e. Fin
47 eleq1 
 |-  ( ( b i^i ( A \ { o } ) ) = (/) -> ( ( b i^i ( A \ { o } ) ) e. Fin <-> (/) e. Fin ) )
48 46 47 mpbiri 
 |-  ( ( b i^i ( A \ { o } ) ) = (/) -> ( b i^i ( A \ { o } ) ) e. Fin )
49 snfi 
 |-  { o } e. Fin
50 unfi 
 |-  ( ( ( b i^i ( A \ { o } ) ) e. Fin /\ { o } e. Fin ) -> ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin )
51 48 49 50 sylancl 
 |-  ( ( b i^i ( A \ { o } ) ) = (/) -> ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin )
52 ssun1 
 |-  b C_ ( b u. { o } )
53 ssun1 
 |-  A C_ ( A u. { o } )
54 undif1 
 |-  ( ( A \ { o } ) u. { o } ) = ( A u. { o } )
55 53 54 sseqtrri 
 |-  A C_ ( ( A \ { o } ) u. { o } )
56 ss2in 
 |-  ( ( b C_ ( b u. { o } ) /\ A C_ ( ( A \ { o } ) u. { o } ) ) -> ( b i^i A ) C_ ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) ) )
57 52 55 56 mp2an 
 |-  ( b i^i A ) C_ ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) )
58 incom 
 |-  ( A i^i b ) = ( b i^i A )
59 undir 
 |-  ( ( b i^i ( A \ { o } ) ) u. { o } ) = ( ( b u. { o } ) i^i ( ( A \ { o } ) u. { o } ) )
60 57 58 59 3sstr4i 
 |-  ( A i^i b ) C_ ( ( b i^i ( A \ { o } ) ) u. { o } )
61 ssfi 
 |-  ( ( ( ( b i^i ( A \ { o } ) ) u. { o } ) e. Fin /\ ( A i^i b ) C_ ( ( b i^i ( A \ { o } ) ) u. { o } ) ) -> ( A i^i b ) e. Fin )
62 51 60 61 sylancl 
 |-  ( ( b i^i ( A \ { o } ) ) = (/) -> ( A i^i b ) e. Fin )
63 62 exlimiv 
 |-  ( E. o ( b i^i ( A \ { o } ) ) = (/) -> ( A i^i b ) e. Fin )
64 63 ralimi 
 |-  ( A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) -> A. b e. z ( A i^i b ) e. Fin )
65 45 64 anim12ci 
 |-  ( ( ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) /\ X = U. z ) /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) )
66 65 expl 
 |-  ( ( ( A C_ X /\ -. A e. Fin ) /\ z e. ( ~P J i^i Fin ) ) -> ( ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) )
67 66 reximdva 
 |-  ( ( A C_ X /\ -. A e. Fin ) -> ( E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) )
68 67 3adant1 
 |-  ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( E. z e. ( ~P J i^i Fin ) ( X = U. z /\ A. b e. z E. o ( b i^i ( A \ { o } ) ) = (/) ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) )
69 35 68 syld 
 |-  ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> ( -. E. x e. X x e. ( ( limPt ` J ) ` A ) -> E. z e. ( ~P J i^i Fin ) ( A. b e. z ( A i^i b ) e. Fin /\ E. b e. z -. ( A i^i b ) e. Fin ) ) )
70 8 69 mt3i 
 |-  ( ( J e. Comp /\ A C_ X /\ -. A e. Fin ) -> E. x e. X x e. ( ( limPt ` J ) ` A ) )