Metamath Proof Explorer

Theorem restperf

Description: Perfection of a subspace. Note that the term "perfect set" is reserved forclosed sets which are perfect in the subspace topology. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses restcls.1 
|- X = U. J
restcls.2 
|- K = ( J |`t Y )
Assertion restperf 
|- ( ( J e. Top /\ Y C_ X ) -> ( K e. Perf <-> Y C_ ( ( limPt ` J ) ` Y ) ) )

Proof

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