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