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 = J
restcls.2 K = J 𝑡 Y
Assertion restlp J Top Y X S Y limPt K S = limPt J S Y

Proof

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