Metamath Proof Explorer

Theorem clslp

Description: The closure of a subset of a topological space is the subset together with its limit points. Theorem 6.6 of Munkres p. 97. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis lpfval.1 
|- X = U. J
Assertion clslp 
|- ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( S u. ( ( limPt ` J ) ` S ) ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 
 |-  X = U. J
2 1 neindisj 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ ( x e. ( ( cls ` J ) ` S ) /\ n e. ( ( nei ` J ) ` { x } ) ) ) -> ( n i^i S ) =/= (/) )
3 2 expr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( n e. ( ( nei ` J ) ` { x } ) -> ( n i^i S ) =/= (/) ) )
4 3 adantr 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) /\ -. x e. S ) -> ( n e. ( ( nei ` J ) ` { x } ) -> ( n i^i S ) =/= (/) ) )
5 difsn 
 |-  ( -. x e. S -> ( S \ { x } ) = S )
6 5 ineq2d 
 |-  ( -. x e. S -> ( n i^i ( S \ { x } ) ) = ( n i^i S ) )
7 6 neeq1d 
 |-  ( -. x e. S -> ( ( n i^i ( S \ { x } ) ) =/= (/) <-> ( n i^i S ) =/= (/) ) )
8 7 adantl 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) /\ -. x e. S ) -> ( ( n i^i ( S \ { x } ) ) =/= (/) <-> ( n i^i S ) =/= (/) ) )
9 4 8 sylibrd 
 |-  ( ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) /\ -. x e. S ) -> ( n e. ( ( nei ` J ) ` { x } ) -> ( n i^i ( S \ { x } ) ) =/= (/) ) )
10 9 ex 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( -. x e. S -> ( n e. ( ( nei ` J ) ` { x } ) -> ( n i^i ( S \ { x } ) ) =/= (/) ) ) )
11 10 ralrimdv 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( -. x e. S -> A. n e. ( ( nei ` J ) ` { x } ) ( n i^i ( S \ { x } ) ) =/= (/) ) )
12 simpll 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> J e. Top )
13 simplr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> S C_ X )
14 1 clsss3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ X )
15 14 sselda 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> x e. X )
16 1 islp2 
 |-  ( ( J e. Top /\ S C_ X /\ x e. X ) -> ( x e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { x } ) ( n i^i ( S \ { x } ) ) =/= (/) ) )
17 12 13 15 16 syl3anc 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( x e. ( ( limPt ` J ) ` S ) <-> A. n e. ( ( nei ` J ) ` { x } ) ( n i^i ( S \ { x } ) ) =/= (/) ) )
18 11 17 sylibrd 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( -. x e. S -> x e. ( ( limPt ` J ) ` S ) ) )
19 18 orrd 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> ( x e. S \/ x e. ( ( limPt ` J ) ` S ) ) )
20 elun 
 |-  ( x e. ( S u. ( ( limPt ` J ) ` S ) ) <-> ( x e. S \/ x e. ( ( limPt ` J ) ` S ) ) )
21 19 20 sylibr 
 |-  ( ( ( J e. Top /\ S C_ X ) /\ x e. ( ( cls ` J ) ` S ) ) -> x e. ( S u. ( ( limPt ` J ) ` S ) ) )
22 21 ex 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` S ) -> x e. ( S u. ( ( limPt ` J ) ` S ) ) ) )
23 22 ssrdv 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) C_ ( S u. ( ( limPt ` J ) ` S ) ) )
24 1 sscls 
 |-  ( ( J e. Top /\ S C_ X ) -> S C_ ( ( cls ` J ) ` S ) )
25 1 lpsscls 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) C_ ( ( cls ` J ) ` S ) )
26 24 25 unssd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( S u. ( ( limPt ` J ) ` S ) ) C_ ( ( cls ` J ) ` S ) )
27 23 26 eqssd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( cls ` J ) ` S ) = ( S u. ( ( limPt ` J ) ` S ) ) )