Theorem cldss

Description: A closed set is a subset of the underlying set of a topology. (Contributed by NM, 5-Oct-2006) (Revised by Stefan O'Rear, 22-Feb-2015)

	Ref	Expression
Hypothesis	iscld.1	$$⊢X=\bigcup J$$
Assertion	cldss	$$⊢S\in \mathrm{Clsd}\left(J\right)\to S\subseteq X$$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2		cldrcl	$$⊢S\in \mathrm{Clsd}\left(J\right)\to J\in \mathrm{Top}$$
3	1	iscld	$$⊢J\in \mathrm{Top}\to \left(S\in \mathrm{Clsd}\left(J\right)\leftrightarrow \left(S\subseteq X\wedge X\setminus S\in J\right)\right)$$
4	3	simprbda	$$⊢\left(J\in \mathrm{Top}\wedge S\in \mathrm{Clsd}\left(J\right)\right)\to S\subseteq X$$
5	2 4	mpancom	$$⊢S\in \mathrm{Clsd}\left(J\right)\to S\subseteq X$$