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

Metamath Proof Explorer

Theorem lpsscls

Description: The limit points of a subset are included in the subset's closure. (Contributed by NM, 26-Feb-2007)

Ref Expression
Hypothesis lpfval.1 ⊢ 𝑋 = ∪ 𝐽
Assertion lpsscls ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ 𝑋 = ∪ 𝐽
2 1 lpval ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) = { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } )
3 difss ⊢ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑆
4 1 clsss ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ∧ ( 𝑆 ∖ { 𝑥 } ) ⊆ 𝑆 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
5 3 4 mp3an3 ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
6 5 sseld ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) → 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) ) )
7 6 abssdv ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → { 𝑥 ∣ 𝑥 ∈ ( ( cls ‘ 𝐽 ) ‘ ( 𝑆 ∖ { 𝑥 } ) ) } ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )
8 2 7 eqsstrd ⊢ ( ( 𝐽 ∈ Top ∧ 𝑆 ⊆ 𝑋 ) → ( ( limPt ‘ 𝐽 ) ‘ 𝑆 ) ⊆ ( ( cls ‘ 𝐽 ) ‘ 𝑆 ) )