Metamath Proof Explorer

Theorem lpdifsn

Description: P is a limit point of S iff it is a limit point of S \ { P } . (Contributed by Mario Carneiro, 25-Dec-2016)

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

Proof

Step Hyp Ref Expression
1 lpfval.1 
 |-  X = U. J
2 1 islp 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
3 ssdifss 
 |-  ( S C_ X -> ( S \ { P } ) C_ X )
4 1 islp 
 |-  ( ( J e. Top /\ ( S \ { P } ) C_ X ) -> ( P e. ( ( limPt ` J ) ` ( S \ { P } ) ) <-> P e. ( ( cls ` J ) ` ( ( S \ { P } ) \ { P } ) ) ) )
5 3 4 sylan2 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` ( S \ { P } ) ) <-> P e. ( ( cls ` J ) ` ( ( S \ { P } ) \ { P } ) ) ) )
6 difabs 
 |-  ( ( S \ { P } ) \ { P } ) = ( S \ { P } )
7 6 fveq2i 
 |-  ( ( cls ` J ) ` ( ( S \ { P } ) \ { P } ) ) = ( ( cls ` J ) ` ( S \ { P } ) )
8 7 eleq2i 
 |-  ( P e. ( ( cls ` J ) ` ( ( S \ { P } ) \ { P } ) ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) )
9 5 8 bitrdi 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` ( S \ { P } ) ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
10 2 9 bitr4d 
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( limPt ` J ) ` ( S \ { P } ) ) ) )