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

Metamath Proof Explorer

Theorem islp3

Description: The predicate " P is a limit point of S " in terms of open sets. see islp2 , elcls , islp . (Contributed by FL, 31-Jul-2009)

Ref Expression
Hypothesis lpfval.1 
|- X = U. J
Assertion islp3 
|- ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i ( 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 2 3adant3 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> P e. ( ( cls ` J ) ` ( S \ { P } ) ) ) )
4 simp2 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> S C_ X )
5 4 ssdifssd 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( S \ { P } ) C_ X )
6 1 elcls 
 |-  ( ( J e. Top /\ ( S \ { P } ) C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` ( S \ { P } ) ) <-> A. x e. J ( P e. x -> ( x i^i ( S \ { P } ) ) =/= (/) ) ) )
7 5 6 syld3an2 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( cls ` J ) ` ( S \ { P } ) ) <-> A. x e. J ( P e. x -> ( x i^i ( S \ { P } ) ) =/= (/) ) ) )
8 3 7 bitrd 
 |-  ( ( J e. Top /\ S C_ X /\ P e. X ) -> ( P e. ( ( limPt ` J ) ` S ) <-> A. x e. J ( P e. x -> ( x i^i ( S \ { P } ) ) =/= (/) ) ) )