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 ⊢ 𝑋 = ∪ 𝐽
restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
Assertion restlp ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 restcls.1 ⊢ 𝑋 = ∪ 𝐽
2 restcls.2 ⊢ 𝐾 = ( 𝐽 ↾t 𝑌 )
3 simp3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ 𝑌 )
4 3 ssdifssd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑌 )
5 1 2 restcls ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∩ 𝑌 ) )
6 4 5 syld3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) = ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∩ 𝑌 ) )
7 6 eleq2d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ 𝑥 ∈ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∩ 𝑌 ) ) )
8 elin ⊢ ( 𝑥 ∈ ( ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝑥 ∈ 𝑌 ) )
9 7 8 bitrdi ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝑥 ∈ 𝑌 ) ) )
10 simp1 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐽 ∈ Top )
11 1 toptopon ⊢ ( 𝐽 ∈ Top ↔ 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
12 10 11 sylib ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐽 ∈ ( TopOn ‘ 𝑋 ) )
13 simp2 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑌 ⊆ 𝑋 )
14 resttopon ⊢ ( ( 𝐽 ∈ ( TopOn ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
15 12 13 14 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝐽 ↾t 𝑌 ) ∈ ( TopOn ‘ 𝑌 ) )
16 2 15 eqeltrid ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐾 ∈ ( TopOn ‘ 𝑌 ) )
17 topontop ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝐾 ∈ Top )
18 16 17 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝐾 ∈ Top )
19 toponuni ⊢ ( 𝐾 ∈ ( TopOn ‘ 𝑌 ) → 𝑌 = ∪ 𝐾 )
20 16 19 syl ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑌 = ∪ 𝐾 )
21 3 20 sseqtrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ ∪ 𝐾 )
22 eqid ⊢ ∪ 𝐾 = ∪ 𝐾
23 22 islp ⊢ ( ( 𝐾 ∈ Top ∧ 𝑆 ⊆ ∪ 𝐾 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
24 18 21 23 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐾 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
25 elin ⊢ ( 𝑥 ∈ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) )
26 3 13 sstrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → 𝑆 ⊆ 𝑋 )
27 1 islp ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
28 10 26 27 syl2anc ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
29 28 anbi1d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∧ 𝑥 ∈ 𝑌 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝑥 ∈ 𝑌 ) ) )
30 25 29 syl5bb ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝑥 ∈ 𝑌 ) ) )
31 9 24 30 3bitr4d ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ) )
32 31 eqrdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )