Metamath Proof Explorer

Theorem lpss3

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

Ref Expression
Hypothesis lpfval.1 ⊢ X = ⋃ J
Assertion lpss3 ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → limPt ⁡ J ⁡ T ⊆ limPt ⁡ J ⁡ S

Proof

Step Hyp Ref Expression
1 lpfval.1 ⊢ X = ⋃ J
2 simp1 ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → J ∈ Top
3 simp2 ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → S ⊆ X
4 3 ssdifssd ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → S ∖ x ⊆ X
5 simp3 ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → T ⊆ S
6 5 ssdifd ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → T ∖ x ⊆ S ∖ x
7 1 clsss ⊢ J ∈ Top ∧ S ∖ x ⊆ X ∧ T ∖ x ⊆ S ∖ x → cls ⁡ J ⁡ T ∖ x ⊆ cls ⁡ J ⁡ S ∖ x
8 2 4 6 7 syl3anc ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → cls ⁡ J ⁡ T ∖ x ⊆ cls ⁡ J ⁡ S ∖ x
9 8 sseld ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → x ∈ cls ⁡ J ⁡ T ∖ x → x ∈ cls ⁡ J ⁡ S ∖ x
10 5 3 sstrd ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → T ⊆ X
11 1 islp ⊢ J ∈ Top ∧ T ⊆ X → x ∈ limPt ⁡ J ⁡ T ↔ x ∈ cls ⁡ J ⁡ T ∖ x
12 2 10 11 syl2anc ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → x ∈ limPt ⁡ J ⁡ T ↔ x ∈ cls ⁡ J ⁡ T ∖ x
13 1 islp ⊢ J ∈ Top ∧ S ⊆ X → x ∈ limPt ⁡ J ⁡ S ↔ x ∈ cls ⁡ J ⁡ S ∖ x
14 2 3 13 syl2anc ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → x ∈ limPt ⁡ J ⁡ S ↔ x ∈ cls ⁡ J ⁡ S ∖ x
15 9 12 14 3imtr4d ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → x ∈ limPt ⁡ J ⁡ T → x ∈ limPt ⁡ J ⁡ S
16 15 ssrdv ⊢ J ∈ Top ∧ S ⊆ X ∧ T ⊆ S → limPt ⁡ J ⁡ T ⊆ limPt ⁡ J ⁡ S