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 ⊢ 𝑋 = ∪ 𝐽
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 0fin ⊢ ∅ ∈ 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 ‘ 𝐽 ) ‘ 𝐴 ) )