# Metamath Proof Explorer

## Theorem clsss

Description: Subset relationship for closure. (Contributed by NM, 10-Feb-2007)

Ref Expression
Hypothesis clscld.1 ${⊢}{X}=\bigcup {J}$
Assertion clsss ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to \mathrm{cls}\left({J}\right)\left({T}\right)\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 clscld.1 ${⊢}{X}=\bigcup {J}$
2 sstr2 ${⊢}{T}\subseteq {S}\to \left({S}\subseteq {x}\to {T}\subseteq {x}\right)$
3 2 adantr ${⊢}\left({T}\subseteq {S}\wedge {x}\in \mathrm{Clsd}\left({J}\right)\right)\to \left({S}\subseteq {x}\to {T}\subseteq {x}\right)$
4 3 ss2rabdv ${⊢}{T}\subseteq {S}\to \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}\subseteq \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}$
5 intss ${⊢}\left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}\subseteq \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}\to \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}\subseteq \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
6 4 5 syl ${⊢}{T}\subseteq {S}\to \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}\subseteq \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
7 6 3ad2ant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}\subseteq \bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
8 simp1 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to {J}\in \mathrm{Top}$
9 sstr2 ${⊢}{T}\subseteq {S}\to \left({S}\subseteq {X}\to {T}\subseteq {X}\right)$
10 9 impcom ${⊢}\left({S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to {T}\subseteq {X}$
11 10 3adant1 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to {T}\subseteq {X}$
12 1 clsval ${⊢}\left({J}\in \mathrm{Top}\wedge {T}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({T}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}$
13 8 11 12 syl2anc ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to \mathrm{cls}\left({J}\right)\left({T}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{T}\subseteq {x}\right\}$
14 1 clsval ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
15 14 3adant3 ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to \mathrm{cls}\left({J}\right)\left({S}\right)=\bigcap \left\{{x}\in \mathrm{Clsd}\left({J}\right)|{S}\subseteq {x}\right\}$
16 7 13 15 3sstr4d ${⊢}\left({J}\in \mathrm{Top}\wedge {S}\subseteq {X}\wedge {T}\subseteq {S}\right)\to \mathrm{cls}\left({J}\right)\left({T}\right)\subseteq \mathrm{cls}\left({J}\right)\left({S}\right)$