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