Step |
Hyp |
Ref |
Expression |
1 |
|
restcls.1 |
|- X = U. J |
2 |
|
restcls.2 |
|- K = ( J |`t Y ) |
3 |
1
|
toptopon |
|- ( J e. Top <-> J e. ( TopOn ` X ) ) |
4 |
|
resttopon |
|- ( ( J e. ( TopOn ` X ) /\ Y C_ X ) -> ( J |`t Y ) e. ( TopOn ` Y ) ) |
5 |
3 4
|
sylanb |
|- ( ( J e. Top /\ Y C_ X ) -> ( J |`t Y ) e. ( TopOn ` Y ) ) |
6 |
2 5
|
eqeltrid |
|- ( ( J e. Top /\ Y C_ X ) -> K e. ( TopOn ` Y ) ) |
7 |
|
topontop |
|- ( K e. ( TopOn ` Y ) -> K e. Top ) |
8 |
6 7
|
syl |
|- ( ( J e. Top /\ Y C_ X ) -> K e. Top ) |
9 |
|
eqid |
|- U. K = U. K |
10 |
9
|
isperf |
|- ( K e. Perf <-> ( K e. Top /\ ( ( limPt ` K ) ` U. K ) = U. K ) ) |
11 |
10
|
baib |
|- ( K e. Top -> ( K e. Perf <-> ( ( limPt ` K ) ` U. K ) = U. K ) ) |
12 |
8 11
|
syl |
|- ( ( J e. Top /\ Y C_ X ) -> ( K e. Perf <-> ( ( limPt ` K ) ` U. K ) = U. K ) ) |
13 |
|
sseqin2 |
|- ( Y C_ ( ( limPt ` J ) ` Y ) <-> ( ( ( limPt ` J ) ` Y ) i^i Y ) = Y ) |
14 |
|
ssid |
|- Y C_ Y |
15 |
1 2
|
restlp |
|- ( ( J e. Top /\ Y C_ X /\ Y C_ Y ) -> ( ( limPt ` K ) ` Y ) = ( ( ( limPt ` J ) ` Y ) i^i Y ) ) |
16 |
14 15
|
mp3an3 |
|- ( ( J e. Top /\ Y C_ X ) -> ( ( limPt ` K ) ` Y ) = ( ( ( limPt ` J ) ` Y ) i^i Y ) ) |
17 |
|
toponuni |
|- ( K e. ( TopOn ` Y ) -> Y = U. K ) |
18 |
6 17
|
syl |
|- ( ( J e. Top /\ Y C_ X ) -> Y = U. K ) |
19 |
18
|
fveq2d |
|- ( ( J e. Top /\ Y C_ X ) -> ( ( limPt ` K ) ` Y ) = ( ( limPt ` K ) ` U. K ) ) |
20 |
16 19
|
eqtr3d |
|- ( ( J e. Top /\ Y C_ X ) -> ( ( ( limPt ` J ) ` Y ) i^i Y ) = ( ( limPt ` K ) ` U. K ) ) |
21 |
20 18
|
eqeq12d |
|- ( ( J e. Top /\ Y C_ X ) -> ( ( ( ( limPt ` J ) ` Y ) i^i Y ) = Y <-> ( ( limPt ` K ) ` U. K ) = U. K ) ) |
22 |
13 21
|
syl5bb |
|- ( ( J e. Top /\ Y C_ X ) -> ( Y C_ ( ( limPt ` J ) ` Y ) <-> ( ( limPt ` K ) ` U. K ) = U. K ) ) |
23 |
12 22
|
bitr4d |
|- ( ( J e. Top /\ Y C_ X ) -> ( K e. Perf <-> Y C_ ( ( limPt ` J ) ` Y ) ) ) |