Metamath Proof Explorer

Theorem clsss2

Description: If a subset is included in a closed set, so is the subset's closure. (Contributed by NM, 22-Feb-2007)

Ref Expression
Hypothesis clscld.1 ⊢ X = ⋃ J
Assertion clsss2 ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → cls ⁡ J ⁡ S ⊆ C

Proof

Step Hyp Ref Expression
1 clscld.1 ⊢ X = ⋃ J
2 cldrcl ⊢ C ∈ Clsd ⁡ J → J ∈ Top
3 2 adantr ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → J ∈ Top
4 1 cldss ⊢ C ∈ Clsd ⁡ J → C ⊆ X
5 4 adantr ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → C ⊆ X
6 simpr ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → S ⊆ C
7 1 clsss ⊢ J ∈ Top ∧ C ⊆ X ∧ S ⊆ C → cls ⁡ J ⁡ S ⊆ cls ⁡ J ⁡ C
8 3 5 6 7 syl3anc ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → cls ⁡ J ⁡ S ⊆ cls ⁡ J ⁡ C
9 cldcls ⊢ C ∈ Clsd ⁡ J → cls ⁡ J ⁡ C = C
10 9 adantr ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → cls ⁡ J ⁡ C = C
11 8 10 sseqtrd ⊢ C ∈ Clsd ⁡ J ∧ S ⊆ C → cls ⁡ J ⁡ S ⊆ C