Theorem cldcls

Description: A closed subset equals its own closure. (Contributed by NM, 15-Mar-2007)

	Ref	Expression
Assertion	cldcls	$$⊢S\in \mathrm{Clsd}\left(J\right)\to \mathrm{cls}\left(J\right)\left(S\right)=S$$

Proof

Step	Hyp	Ref	Expression
1		cldrcl	$$⊢S\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
2		eqid	$$⊢\bigcup J=\bigcup J$$
3	2	cldss	$$⊢S\in \mathrm{Clsd}\left(J\right)\to S\subseteq \bigcup J$$
4	2	clsval	$$⊢\left(J\in \mathrm{Top}\wedge S\subseteq \bigcup J\right)\to \mathrm{cls}\left(J\right)\left(S\right)=\bigcap \left\{x\in \mathrm{Clsd}\left(J\right)|S\subseteq x\right\}$$
5	1 3 4	syl2anc	$$⊢S\in \mathrm{Clsd}\left(J\right)\to \mathrm{cls}\left(J\right)\left(S\right)=\bigcap \left\{x\in \mathrm{Clsd}\left(J\right)|S\subseteq x\right\}$$
6		intmin	$$⊢S\in \mathrm{Clsd}\left(J\right)\to \bigcap \left\{x\in \mathrm{Clsd}\left(J\right)|S\subseteq x\right\}=S$$
7	5 6	eqtrd	$$⊢S\in \mathrm{Clsd}\left(J\right)\to \mathrm{cls}\left(J\right)\left(S\right)=S$$