Theorem cldss2

Description: The set of closed sets is contained in the powerset of the base. (Contributed by Mario Carneiro, 6-Jan-2014)

	Ref	Expression
Hypothesis	iscld.1	$$⊢X=\bigcup J$$
Assertion	cldss2	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$

Proof

Step	Hyp	Ref	Expression
1		iscld.1	$$⊢X=\bigcup J$$
2	1	cldss	$$⊢x\in \mathrm{Clsd}\left(J\right)\to x\subseteq X$$
3		velpw	$$⊢x\in 𝒫X\leftrightarrow x\subseteq X$$
4	2 3	sylibr	$$⊢x\in \mathrm{Clsd}\left(J\right)\to x\in 𝒫X$$
5	4	ssriv	$$⊢\mathrm{Clsd}\left(J\right)\subseteq 𝒫X$$