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 
|- X = U. J
Assertion lpcls 
|- ( ( J e. Fre /\ S C_ X ) -> ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) = ( ( limPt ` J ) ` S ) )

Proof

Step Hyp Ref Expression
1 lpcls.1 
 |-  X = U. J
2 t1top 
 |-  ( J e. Fre -> J e. Top )
3 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
4 3 ssdifssd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( ( cls ` J ) ` S ) \ { x } ) C_ X )
5 1 clsss3 
 |-  ( ( J e. Top /\ ( ( ( cls ` J ) ` S ) \ { x } ) C_ X ) -> ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) C_ X )
6 4 5 syldan 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) C_ X )
7 2 6 sylan 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) C_ X )
8 7 sseld 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) -> x e. X ) )
9 ssdifss 
 |-  ( S C_ X -> ( S \ { x } ) C_ X )
10 1 clscld 
 |-  ( ( J e. Top /\ ( S \ { x } ) C_ X ) -> ( ( cls ` J ) ` ( S \ { x } ) ) e. ( Clsd ` J ) )
11 2 9 10 syl2an 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( cls ` J ) ` ( S \ { x } ) ) e. ( Clsd ` J ) )
12 11 adantr 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( ( cls ` J ) ` ( S \ { x } ) ) e. ( Clsd ` J ) )
13 1 t1sncld 
 |-  ( ( J e. Fre /\ x e. X ) -> { x } e. ( Clsd ` J ) )
14 13 adantlr 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> { x } e. ( Clsd ` J ) )
15 uncld 
 |-  ( ( { x } e. ( Clsd ` J ) /\ ( ( cls ` J ) ` ( S \ { x } ) ) e. ( Clsd ` J ) ) -> ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) e. ( Clsd ` J ) )
16 14 12 15 syl2anc 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) e. ( Clsd ` J ) )
17 1 sscls 
 |-  ( ( J e. Top /\ ( S \ { x } ) C_ X ) -> ( S \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
18 2 9 17 syl2an 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( S \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
19 ssundif 
 |-  ( S C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) <-> ( S \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
20 18 19 sylibr 
 |-  ( ( J e. Fre /\ S C_ X ) -> S C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
21 20 adantr 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> S C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
22 1 clsss2 
 |-  ( ( ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) e. ( Clsd ` J ) /\ S C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) ) -> ( ( cls ` J ) ` S ) C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
23 16 21 22 syl2anc 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( ( cls ` J ) ` S ) C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
24 ssundif 
 |-  ( ( ( cls ` J ) ` S ) C_ ( { x } u. ( ( cls ` J ) ` ( S \ { x } ) ) ) <-> ( ( ( cls ` J ) ` S ) \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
25 23 24 sylib 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( ( ( cls ` J ) ` S ) \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
26 1 clsss2 
 |-  ( ( ( ( cls ` J ) ` ( S \ { x } ) ) e. ( Clsd ` J ) /\ ( ( ( cls ` J ) ` S ) \ { x } ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) ) -> ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
27 12 25 26 syl2anc 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) C_ ( ( cls ` J ) ` ( S \ { x } ) ) )
28 27 sseld 
 |-  ( ( ( J e. Fre /\ S C_ X ) /\ x e. X ) -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) -> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
29 28 ex 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. X -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) -> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) ) )
30 29 com23 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) -> ( x e. X -> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) ) )
31 8 30 mpdd 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) -> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
32 2 adantr 
 |-  ( ( J e. Fre /\ S C_ X ) -> J e. Top )
33 2 3 sylan 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
34 33 ssdifssd 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( ( cls ` J ) ` S ) \ { x } ) C_ X )
35 1 sscls 
 |-  ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
36 2 35 sylan 
 |-  ( ( J e. Fre /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
37 36 ssdifd 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( S \ { x } ) C_ ( ( ( cls ` J ) ` S ) \ { x } ) )
38 1 clsss 
 |-  ( ( J e. Top /\ ( ( ( cls ` J ) ` S ) \ { x } ) C_ X /\ ( S \ { x } ) C_ ( ( ( cls ` J ) ` S ) \ { x } ) ) -> ( ( cls ` J ) ` ( S \ { x } ) ) C_ ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) )
39 32 34 37 38 syl3anc 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( cls ` J ) ` ( S \ { x } ) ) C_ ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) )
40 39 sseld 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) -> x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) ) )
41 31 40 impbid 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
42 1 islp 
 |-  ( ( J e. Top /\ ( ( cls ` J ) ` S ) C_ X ) -> ( x e. ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) <-> x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) ) )
43 3 42 syldan 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) <-> x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) ) )
44 2 43 sylan 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) <-> x e. ( ( cls ` J ) ` ( ( ( cls ` J ) ` S ) \ { x } ) ) ) )
45 1 islp 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
46 2 45 sylan 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
47 41 44 46 3bitr4d 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) <-> x e. ( ( limPt ` J ) ` S ) ) )
48 47 eqrdv 
 |-  ( ( J e. Fre /\ S C_ X ) -> ( ( limPt ` J ) ` ( ( cls ` J ) ` S ) ) = ( ( limPt ` J ) ` S ) )