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	⊢ 𝑋 = ∪ 𝐽
Assertion	cldss2	⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋

Proof

Step	Hyp	Ref	Expression
1		iscld.1	⊢ 𝑋 = ∪ 𝐽
2	1	cldss	⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ 𝑋 )
3		velpw	⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 )
4	2 3	sylibr	⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ 𝒫 𝑋 )
5	4	ssriv	⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋