Step |
Hyp |
Ref |
Expression |
1 |
|
lpfval.1 |
|- X = U. J |
2 |
1
|
isperf |
|- ( J e. Perf <-> ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) ) |
3 |
|
ssid |
|- X C_ X |
4 |
1
|
lpss |
|- ( ( J e. Top /\ X C_ X ) -> ( ( limPt ` J ) ` X ) C_ X ) |
5 |
3 4
|
mpan2 |
|- ( J e. Top -> ( ( limPt ` J ) ` X ) C_ X ) |
6 |
|
eqss |
|- ( ( ( limPt ` J ) ` X ) = X <-> ( ( ( limPt ` J ) ` X ) C_ X /\ X C_ ( ( limPt ` J ) ` X ) ) ) |
7 |
6
|
baib |
|- ( ( ( limPt ` J ) ` X ) C_ X -> ( ( ( limPt ` J ) ` X ) = X <-> X C_ ( ( limPt ` J ) ` X ) ) ) |
8 |
5 7
|
syl |
|- ( J e. Top -> ( ( ( limPt ` J ) ` X ) = X <-> X C_ ( ( limPt ` J ) ` X ) ) ) |
9 |
8
|
pm5.32i |
|- ( ( J e. Top /\ ( ( limPt ` J ) ` X ) = X ) <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) ) |
10 |
2 9
|
bitri |
|- ( J e. Perf <-> ( J e. Top /\ X C_ ( ( limPt ` J ) ` X ) ) ) |