This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝐽 ) ‘ 𝑆 ) )