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		0fi	\|- (/) 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 ) )

Metamath Proof Explorer

Theorem bwth

Proof