This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 } ) ) ) )