Metamath Proof Explorer

Theorem restlp

Description: The limit points of a subset restrict naturally in a subspace. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypotheses restcls.1 
|- X = U. J
restcls.2 
|- K = ( J |`t Y )
Assertion restlp 
|- ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( limPt ` K ) ` S ) = ( ( ( limPt ` J ) ` S ) i^i Y ) )

Proof

Step Hyp Ref Expression
1 restcls.1 
 |-  X = U. J
2 restcls.2 
 |-  K = ( J |`t Y )
3 simp3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ Y )
4 3 ssdifssd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( S \ { x } ) C_ Y )
5 1 2 restcls 
 |-  ( ( J e. Top /\ Y C_ X /\ ( S \ { x } ) C_ Y ) -> ( ( cls ` K ) ` ( S \ { x } ) ) = ( ( ( cls ` J ) ` ( S \ { x } ) ) i^i Y ) )
6 4 5 syld3an3 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( cls ` K ) ` ( S \ { x } ) ) = ( ( ( cls ` J ) ` ( S \ { x } ) ) i^i Y ) )
7 6 eleq2d 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( cls ` K ) ` ( S \ { x } ) ) <-> x e. ( ( ( cls ` J ) ` ( S \ { x } ) ) i^i Y ) ) )
8 elin 
 |-  ( x e. ( ( ( cls ` J ) ` ( S \ { x } ) ) i^i Y ) <-> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) /\ x e. Y ) )
9 7 8 bitrdi 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( cls ` K ) ` ( S \ { x } ) ) <-> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) /\ x e. Y ) ) )
10 simp1 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> J e. Top )
11 1 toptopon 
 |-  ( J e. Top <-> J e. ( TopOn ` X ) )
12 10 11 sylib 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> J e. ( TopOn ` X ) )
13 simp2 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> Y C_ X )
14 resttopon 
 |-  ( ( J e. ( TopOn ` X ) /\ Y C_ X ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
15 12 13 14 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( J |`t Y ) e. ( TopOn ` Y ) )
16 2 15 eqeltrid 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> K e. ( TopOn ` Y ) )
17 topontop 
 |-  ( K e. ( TopOn ` Y ) -> K e. Top )
18 16 17 syl 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> K e. Top )
19 toponuni 
 |-  ( K e. ( TopOn ` Y ) -> Y = U. K )
20 16 19 syl 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> Y = U. K )
21 3 20 sseqtrd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ U. K )
22 eqid 
 |-  U. K = U. K
23 22 islp 
 |-  ( ( K e. Top /\ S C_ U. K ) -> ( x e. ( ( limPt ` K ) ` S ) <-> x e. ( ( cls ` K ) ` ( S \ { x } ) ) ) )
24 18 21 23 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( limPt ` K ) ` S ) <-> x e. ( ( cls ` K ) ` ( S \ { x } ) ) ) )
25 elin 
 |-  ( x e. ( ( ( limPt ` J ) ` S ) i^i Y ) <-> ( x e. ( ( limPt ` J ) ` S ) /\ x e. Y ) )
26 3 13 sstrd 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> S C_ X )
27 1 islp 
 |-  ( ( J e. Top /\ S C_ X ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
28 10 26 27 syl2anc 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( limPt ` J ) ` S ) <-> x e. ( ( cls ` J ) ` ( S \ { x } ) ) ) )
29 28 anbi1d 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( x e. ( ( limPt ` J ) ` S ) /\ x e. Y ) <-> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) /\ x e. Y ) ) )
30 25 29 syl5bb 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( ( limPt ` J ) ` S ) i^i Y ) <-> ( x e. ( ( cls ` J ) ` ( S \ { x } ) ) /\ x e. Y ) ) )
31 9 24 30 3bitr4d 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( x e. ( ( limPt ` K ) ` S ) <-> x e. ( ( ( limPt ` J ) ` S ) i^i Y ) ) )
32 31 eqrdv 
 |-  ( ( J e. Top /\ Y C_ X /\ S C_ Y ) -> ( ( limPt ` K ) ` S ) = ( ( ( limPt ` J ) ` S ) i^i Y ) )