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		0fi	⊢ ∅ ∈ 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 ‘ 𝐽 ) ‘ 𝐴 ) )

Metamath Proof Explorer

Theorem bwth

Proof