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