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.

Step	Hyp	Ref	Expression
1		pm3.24 402	. . . . . . 7 ⊢ ¬ ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin)
2	1	a1i 11	. . . . . 6 ⊢ (𝑏 ∈ 𝑧 → ¬ ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin))
3	2	nrex 3065	. . . . 5 ⊢ ¬ ∃𝑏 ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin)
4		r19.29 3100	. . . . 5 ⊢ ((∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin) → ∃𝑏 ∈ 𝑧 ((𝐴 ∩ 𝑏) ∈ Fin ∧ ¬ (𝐴 ∩ 𝑏) ∈ Fin))
5	3, 4	mto 197	. . . 4 ⊢ ¬ (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
6	5	a1i 11	. . 3 ⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → ¬ (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))
7	6	nrex 3065	. 2 ⊢ ¬ ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
8		ralnex 3063	. . . . . 6 ⊢ (∀𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))
9		cmptop 23343	. . . . . . 7 ⊢ (𝐽 ∈ Comp → 𝐽 ∈ Top)
10		bwt2.1	. . . . . . . . . . 11 ⊢ 𝑋 = ∪ 𝐽
11	10	islp3 23094	. . . . . . . . . 10 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋 ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
12	11	3expa 1119	. . . . . . . . 9 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → (𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
13	12	notbid 318	. . . . . . . 8 ⊢ (((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) ∧ 𝑥 ∈ 𝑋) → (¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
14	13	ralbidva 3158	. . . . . . 7 ⊢ ((𝐽 ∈ Top ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
15	9, 14	sylan 581	. . . . . 6 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
16	8, 15	bitr3id 285	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) ↔ ∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅)))
17		rexanali 3091	. . . . . . . . 9 ⊢ (∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) ↔ ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅))
18		nne 2937	. . . . . . . . . . . 12 ⊢ (¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅)
19		vex 3445	. . . . . . . . . . . . 13 ⊢ 𝑥 ∈ V
20		sneq 4591	. . . . . . . . . . . . . . . 16 ⊢ (𝑜 = 𝑥 → {𝑜} = {𝑥})
21	20	difeq2d 4079	. . . . . . . . . . . . . . 15 ⊢ (𝑜 = 𝑥 → (𝐴 ∖ {𝑜}) = (𝐴 ∖ {𝑥}))
22	21	ineq2d 4173	. . . . . . . . . . . . . 14 ⊢ (𝑜 = 𝑥 → (𝑏 ∩ (𝐴 ∖ {𝑜})) = (𝑏 ∩ (𝐴 ∖ {𝑥})))
23	22	eqeq1d 2739	. . . . . . . . . . . . 13 ⊢ (𝑜 = 𝑥 → ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ ↔ (𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅))
24	19, 23	spcev 3561	. . . . . . . . . . . 12 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑥})) = ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)
25	18, 24	sylbi 217	. . . . . . . . . . 11 ⊢ (¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅ → ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)
26	25	anim2i 618	. . . . . . . . . 10 ⊢ ((𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
27	26	reximi 3075	. . . . . . . . 9 ⊢ (∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ¬ (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
28	17, 27	sylbir 235	. . . . . . . 8 ⊢ (¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
29	28	ralimi 3074	. . . . . . 7 ⊢ (∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
30	10	cmpcov2 23338	. . . . . . . 8 ⊢ ((𝐽 ∈ Comp ∧ ∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅))
31	30	ex 412	. . . . . . 7 ⊢ (𝐽 ∈ Comp → (∀𝑥 ∈ 𝑋 ∃𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 ∧ ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
32	29, 31	syl5 34	. . . . . 6 ⊢ (𝐽 ∈ Comp → (∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
33	32	adantr 480	. . . . 5 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (∀𝑥 ∈ 𝑋 ¬ ∀𝑏 ∈ 𝐽 (𝑥 ∈ 𝑏 → (𝑏 ∩ (𝐴 ∖ {𝑥})) ≠ ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
34	16, 33	sylbid 240	. . . 4 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
35	34	3adant3 1133	. . 3 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅)))
36		elinel2 4155	. . . . . . . 8 ⊢ (𝑧 ∈ (𝒫 𝐽 ∩ Fin) → 𝑧 ∈ Fin)
37		sseq2 3961	. . . . . . . . . . . 12 ⊢ (𝑋 = ∪ 𝑧 → (𝐴 ⊆ 𝑋 ↔ 𝐴 ⊆ ∪ 𝑧))
38	37	biimpac 478	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧) → 𝐴 ⊆ ∪ 𝑧)
39		infssuni 9250	. . . . . . . . . . . . 13 ⊢ ((¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin ∧ 𝐴 ⊆ ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
40	39	3expa 1119	. . . . . . . . . . . 12 ⊢ (((¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin) ∧ 𝐴 ⊆ ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
41	40	ancoms 458	. . . . . . . . . . 11 ⊢ ((𝐴 ⊆ ∪ 𝑧 ∧ (¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
42	38, 41	sylan 581	. . . . . . . . . 10 ⊢ (((𝐴 ⊆ 𝑋 ∧ 𝑋 = ∪ 𝑧) ∧ (¬ 𝐴 ∈ Fin ∧ 𝑧 ∈ Fin)) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
43	42	an42s 662	. . . . . . . . 9 ⊢ (((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ (𝑧 ∈ Fin ∧ 𝑋 = ∪ 𝑧)) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
44	43	anassrs 467	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ Fin) ∧ 𝑋 = ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
45	36, 44	sylanl2 682	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = ∪ 𝑧) → ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)
46		0fi 8983	. . . . . . . . . . . 12 ⊢ ∅ ∈ Fin
47		eleq1 2825	. . . . . . . . . . . 12 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ↔ ∅ ∈ Fin))
48	46, 47	mpbiri 258	. . . . . . . . . . 11 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin)
49		snfi 8984	. . . . . . . . . . 11 ⊢ {𝑜} ∈ Fin
50		unfi 9099	. . . . . . . . . . 11 ⊢ (((𝑏 ∩ (𝐴 ∖ {𝑜})) ∈ Fin ∧ {𝑜} ∈ Fin) → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin)
51	48, 49, 50	sylancl 587	. . . . . . . . . 10 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin)
52		ssun1 4131	. . . . . . . . . . . 12 ⊢ 𝑏 ⊆ (𝑏 ∪ {𝑜})
53		ssun1 4131	. . . . . . . . . . . . 13 ⊢ 𝐴 ⊆ (𝐴 ∪ {𝑜})
54		undif1 4429	. . . . . . . . . . . . 13 ⊢ ((𝐴 ∖ {𝑜}) ∪ {𝑜}) = (𝐴 ∪ {𝑜})
55	53, 54	sseqtrri 3984	. . . . . . . . . . . 12 ⊢ 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜})
56		ss2in 4198	. . . . . . . . . . . 12 ⊢ ((𝑏 ⊆ (𝑏 ∪ {𝑜}) ∧ 𝐴 ⊆ ((𝐴 ∖ {𝑜}) ∪ {𝑜})) → (𝑏 ∩ 𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜})))
57	52, 55, 56	mp2an 693	. . . . . . . . . . 11 ⊢ (𝑏 ∩ 𝐴) ⊆ ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜}))
58		incom 4162	. . . . . . . . . . 11 ⊢ (𝐴 ∩ 𝑏) = (𝑏 ∩ 𝐴)
59		undir 4240	. . . . . . . . . . 11 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) = ((𝑏 ∪ {𝑜}) ∩ ((𝐴 ∖ {𝑜}) ∪ {𝑜}))
60	57, 58, 59	3sstr4i 3986	. . . . . . . . . 10 ⊢ (𝐴 ∩ 𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜})
61		ssfi 9101	. . . . . . . . . 10 ⊢ ((((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜}) ∈ Fin ∧ (𝐴 ∩ 𝑏) ⊆ ((𝑏 ∩ (𝐴 ∖ {𝑜})) ∪ {𝑜})) → (𝐴 ∩ 𝑏) ∈ Fin)
62	51, 60, 61	sylancl 587	. . . . . . . . 9 ⊢ ((𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴 ∩ 𝑏) ∈ Fin)
63	62	exlimiv 1932	. . . . . . . 8 ⊢ (∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → (𝐴 ∩ 𝑏) ∈ Fin)
64	63	ralimi 3074	. . . . . . 7 ⊢ (∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅ → ∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin)
65	45, 64	anim12ci 615	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) ∧ 𝑋 = ∪ 𝑧) ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin))
66	65	expl 457	. . . . 5 ⊢ (((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) ∧ 𝑧 ∈ (𝒫 𝐽 ∩ Fin)) → ((𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → (∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)))
67	66	reximdva 3150	. . . 4 ⊢ ((𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)))
68	67	3adant1 1131	. . 3 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(𝑋 = ∪ 𝑧 ∧ ∀𝑏 ∈ 𝑧 ∃𝑜(𝑏 ∩ (𝐴 ∖ {𝑜})) = ∅) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)))
69	35, 68	syld 47	. 2 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → (¬ ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴) → ∃𝑧 ∈ (𝒫 𝐽 ∩ Fin)(∀𝑏 ∈ 𝑧 (𝐴 ∩ 𝑏) ∈ Fin ∧ ∃𝑏 ∈ 𝑧 ¬ (𝐴 ∩ 𝑏) ∈ Fin)))
70	7, 69	mt3i 149	1 ⊢ ((𝐽 ∈ Comp ∧ 𝐴 ⊆ 𝑋 ∧ ¬ 𝐴 ∈ Fin) → ∃𝑥 ∈ 𝑋 𝑥 ∈ ((limPt‘𝐽)‘𝐴))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 206   ∧ wa 395   ∧ w3a 1087   = wceq 1542  ∃wex 1781   ∈ wcel 2114   ≠ wne 2933  ∀wral 3052  ∃wrex 3061   ∖ cdif 3899   ∪ cun 3900   ∩ cin 3901   ⊆ wss 3902  ∅c0 4286  𝒫 cpw 4555  {csn 4581  ∪ cuni 4864  ‘cfv 6493  Fincfn 8887  Topctop 22841  limPtclp 23082  Compccmp 23334

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-rep 5225  ax-sep 5242  ax-nul 5252  ax-pow 5311  ax-pr 5378  ax-un 7682

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-reu 3352  df-rab 3401  df-v 3443  df-sbc 3742  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-pss 3922  df-nul 4287  df-if 4481  df-pw 4557  df-sn 4582  df-pr 4584  df-op 4588  df-uni 4865  df-int 4904  df-iun 4949  df-iin 4950  df-br 5100  df-opab 5162  df-mpt 5181  df-tr 5207  df-id 5520  df-eprel 5525  df-po 5533  df-so 5534  df-fr 5578  df-we 5580  df-xp 5631  df-rel 5632  df-cnv 5633  df-co 5634  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ord 6321  df-on 6322  df-lim 6323  df-suc 6324  df-iota 6449  df-fun 6495  df-fn 6496  df-f 6497  df-f1 6498  df-fo 6499  df-f1o 6500  df-fv 6501  df-om 7811  df-1o 8399  df-en 8888  df-fin 8891  df-top 22842  df-cld 22967  df-ntr 22968  df-cls 22969  df-lp 23084  df-cmp 23335

This theorem is referenced by:  poimirlem30  37853  fourierdlem42  46460