Metamath Proof Explorer


Theorem islp

Description: The predicate "the class P is a limit point of S ". (Contributed by NM, 10-Feb-2007)

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

Proof

Step Hyp Ref Expression
1 lpfval.1
 |-  X = U. J
2 1 lpval
 |-  ( ( J e. Top /\ S C_ X ) -> ( ( limPt ` J ) ` S ) = { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } )
3 2 eleq2d
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } ) )
4 id
 |-  ( P e. ( ( cls ` J ) ` ( S \ { P } ) ) -> P e. ( ( cls ` J ) ` ( S \ { P } ) ) )
5 id
 |-  ( x = P -> x = P )
6 sneq
 |-  ( x = P -> { x } = { P } )
7 6 difeq2d
 |-  ( x = P -> ( S \ { x } ) = ( S \ { P } ) )
8 7 fveq2d
 |-  ( x = P -> ( ( cls ` J ) ` ( S \ { x } ) ) = ( ( cls ` J ) ` ( S \ { P } ) ) )
9 5 8 eleq12d
 |-  ( x = P -> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
10 4 9 elab3
 |-  ( P e. { x | x e. ( ( cls ` J ) ` ( S \ { x } ) ) } <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) )
11 3 10 bitrdi
 |-  ( ( J e. Top /\ S C_ X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )