This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = ⋃ J$
	Assertion	cldss2	$⊢ Clsd (J) \subseteq 𝒫 X$

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