Metamath Proof Explorer

Theorem lpcls

Description: The limit points of the closure of a subset are the same as the limit points of the set in a T_1 space. (Contributed by Mario Carneiro, 26-Dec-2016)

Ref Expression
Hypothesis lpcls.1 ⊢ 𝑋 = ∪ 𝐽
Assertion lpcls ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 lpcls.1 ⊢ 𝑋 = ∪ 𝐽
2 t1top ⊢ ( 𝐽 ∈ Fre → 𝐽 ∈ Top )
3 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
4 3 ssdifssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ 𝑋 )
5 1 clsss3 ⊢ ( ( 𝐽 ∈ Top ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ⊆ 𝑋 )
6 4 5 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ⊆ 𝑋 )
7 2 6 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ⊆ 𝑋 )
8 7 sseld ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → 𝑥 ∈ 𝑋 ) )
9 ssdifss ⊢ ( 𝑆 ⊆ 𝑋 → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
10 1 clscld ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Clsd ‘ 𝐽 ) )
11 2 9 10 syl2an ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Clsd ‘ 𝐽 ) )
12 11 adantr ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Clsd ‘ 𝐽 ) )
13 1 t1sncld ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
14 13 adantlr ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) )
15 uncld ⊢ ( ( { 𝑥 } ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Clsd ‘ 𝐽 ) ) → ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
16 14 12 15 syl2anc ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( Clsd ‘ 𝐽 ) )
17 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
18 2 9 17 syl2an ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
19 ssundif ⊢ ( 𝑆 ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
20 18 19 sylibr ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
21 20 adantr ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → 𝑆 ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
22 1 clsss2 ⊢ ( ( ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ 𝑆 ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
23 16 21 22 syl2anc ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
24 ssundif ⊢ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( { 𝑥 } ∪ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ↔ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
25 23 24 sylib ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
26 1 clsss2 ⊢ ( ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∈ ( Clsd ‘ 𝐽 ) ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
27 12 25 26 syl2anc ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
28 27 sseld ⊢ ( ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
29 28 ex ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ 𝑋 → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
30 29 com23 ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → ( 𝑥 ∈ 𝑋 → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) ) )
31 8 30 mpdd ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
32 2 adantr ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → 𝐽 ∈ Top )
33 2 3 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 )
34 33 ssdifssd ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ 𝑋 )
35 1 sscls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
36 2 35 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → 𝑆 ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
37 36 ssdifd ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) )
38 1 clsss ⊢ ( ( 𝐽 ∈ Top ∧ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ⊆ 𝑋 ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) )
39 32 34 37 38 syl3anc ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) )
40 39 sseld ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ) )
41 31 40 impbid ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
42 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ) )
43 3 42 syldan ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ) )
44 2 43 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ∖ { 𝑥 } ) ) ) )
45 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
46 2 45 sylan ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
47 41 44 46 3bitr4d ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) ↔ 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
48 47 eqrdv ⊢ ( ( 𝐽 ∈ Fre ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) = ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )