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 𝒫 X

Proof

Step Hyp Ref Expression
1 iscld.1 X = J
2 1 cldss x Clsd J x X
3 velpw x 𝒫 X x X
4 2 3 sylibr x Clsd J x 𝒫 X
5 4 ssriv Clsd J 𝒫 X