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	bitrid	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ∧ 𝑥 ∈ 𝑌 ) ) )
31	9 24 30	3bitr4d	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) ) )
32	31	eqrdv	⊢ ( ( 𝐽 ∈ Top ∧ 𝑌 ⊆ 𝑋 ∧ 𝑆 ⊆ 𝑌 ) → ( ( limPt ‘ 𝐾 ) ‘ 𝑆 ) = ( ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ∩ 𝑌 ) )