# 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}=\bigcup {J}$
Assertion clsss2 ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {C}$

### Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 cldrcl ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to {J}\in \mathrm{Top}$
3 2 adantr ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to {J}\in \mathrm{Top}$
4 1 cldss ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to {C}\subseteq {X}$
5 4 adantr ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to {C}\subseteq {X}$
6 simpr ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to {S}\subseteq {C}$
7 1 clsss ${⊢}\left({J}\in \mathrm{Top}\wedge {C}\subseteq {X}\wedge {S}\subseteq {C}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq \mathrm{cls}\left({J}\right)\left({C}\right)$
8 3 5 6 7 syl3anc ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq \mathrm{cls}\left({J}\right)\left({C}\right)$
9 cldcls ${⊢}{C}\in \mathrm{Clsd}\left({J}\right)\to \mathrm{cls}\left({J}\right)\left({C}\right)={C}$
10 9 adantr ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to \mathrm{cls}\left({J}\right)\left({C}\right)={C}$
11 8 10 sseqtrd ${⊢}\left({C}\in \mathrm{Clsd}\left({J}\right)\wedge {S}\subseteq {C}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)\subseteq {C}$