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=J
Assertion islp3 JTopSXPXPlimPtJSxJPxxSP

Proof

Step Hyp Ref Expression
1 lpfval.1 X=J
2 1 islp JTopSXPlimPtJSPclsJSP
3 2 3adant3 JTopSXPXPlimPtJSPclsJSP
4 simp2 JTopSXPXSX
5 4 ssdifssd JTopSXPXSPX
6 1 elcls JTopSPXPXPclsJSPxJPxxSP
7 5 6 syld3an2 JTopSXPXPclsJSPxJPxxSP
8 3 7 bitrd JTopSXPXPlimPtJSxJPxxSP