Metamath Proof Explorer


Theorem lpss3

Description: Subset relationship for limit points. (Contributed by Mario Carneiro, 25-Dec-2016)

Ref Expression
Hypothesis lpfval.1 𝑋 = 𝐽
Assertion lpss3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 𝑋 = 𝐽
2 simp1 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → 𝐽 ∈ Top )
3 simp2 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → 𝑆𝑋 )
4 3 ssdifssd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 )
5 simp3 ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → 𝑇𝑆 )
6 5 ssdifd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑇 ∖ { 𝑥 } ) ⊆ ( 𝑆 ∖ { 𝑥 } ) )
7 1 clsss ( ( 𝐽 ∈ Top ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑋 ∧ ( 𝑇 ∖ { 𝑥 } ) ⊆ ( 𝑆 ∖ { 𝑥 } ) ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑇 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
8 2 4 6 7 syl3anc ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑇 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) )
9 8 sseld ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑇 ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
10 5 3 sstrd ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → 𝑇𝑋 )
11 1 islp ( ( 𝐽 ∈ Top ∧ 𝑇𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑇 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑇 ∖ { 𝑥 } ) ) ) )
12 2 10 11 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑇 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑇 ∖ { 𝑥 } ) ) ) )
13 1 islp ( ( 𝐽 ∈ Top ∧ 𝑆𝑋 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
14 2 3 13 syl2anc ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ↔ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ) )
15 9 12 14 3imtr4d ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑇 ) → 𝑥 ∈ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ) )
16 15 ssrdv ( ( 𝐽 ∈ Top ∧ 𝑆𝑋𝑇𝑆 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑇 ) ⊆ ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) )