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 𝑋 = 𝐽
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 ‘ 𝐽 ) ⊆ 𝒫 𝑋