Metamath Proof Explorer

Theorem lpval

Description: The set of limit points of a subset of the base set of a topology. Alternate definition of limit point in Munkres p. 97. (Contributed by NM, 10-Feb-2007) (Revised by Mario Carneiro, 11-Nov-2013)

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

Proof

Step Hyp Ref Expression
1 lpfval.1 
 |-  X = U. J
2 1 lpfval 
 |-  ( J e. Top -> ( limPt ` J ) = ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } ) )
3 2 fveq1d 
 |-  ( J e. Top -> ( ( limPt ` J ) ` S ) = ( ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } ) ` S ) )
4 3 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) = ( ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } ) ` S ) )
5 eqid 
 |-  ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } ) = ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } )
6 difeq1 
 |-  ( y = S -> ( y \ { x } ) = ( S \ { x } ) )
7 6 fveq2d 
 |-  ( y = S -> ( ( cls ` J ) ` ( y \ { x } ) ) = ( ( cls ` J ) ` ( S \ { x } ) ) )
8 7 eleq2d 
 |-  ( y = S -> ( x e. ( ( cls ` J ) ` ( y \ { x } ) ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
9 8 abbidv 
 |-  ( y = S -> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )
10 1 topopn 
 |-  ( J e. Top -> X e. J )
11 elpw2g 
 |-  ( X e. J -> ( S e. ~P X <-> S C_ X ) )
12 10 11 syl 
 |-  ( J e. Top -> ( S e. ~P X <-> S C_ X ) )
13 12 biimpar 
 |-  ( ( J e. Top /\ S C_ X ) -> S e. ~P X )
14 10 adantr 
 |-  ( ( J e. Top /\ S C_ X ) -> X e. J )
15 ssdifss 
 |-  ( S C_ X -> ( S \ { x } ) C_ X )
16 1 clsss3 
 |-  ( ( J e. Top /\ ( S \ { x } ) C_ X ) -> ( ( cls ` J ) ` ( S \ { x } ) ) C_ X )
17 16 sseld 
 |-  ( ( J e. Top /\ ( S \ { x } ) C_ X ) -> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) -> x e. X ) )
18 15 17 sylan2 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) -> x e. X ) )
19 18 abssdv 
 |-  ( ( J e. Top /\ S C_ X ) -> { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } C_ X )
20 14 19 ssexd 
 |-  ( ( J e. Top /\ S C_ X ) -> { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } e. _V )
21 5 9 13 20 fvmptd3 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( y e. ~P X |-> { x | x e. ( ( cls ` J ) ` ( y \ { x } ) ) } ) ` S ) = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )
22 4 21 eqtrd 
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )