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 = U. J
Assertion cldss2 
|- ( Clsd ` J ) C_ ~P X

Proof

Step Hyp Ref Expression
1 iscld.1 
 |-  X = U. J
2 1 cldss 
 |-  ( x e. ( Clsd ` J ) -> x C_ X )
3 velpw 
 |-  ( x e. ~P X <-> x C_ X )
4 2 3 sylibr 
 |-  ( x e. ( Clsd ` J ) -> x e. ~P X )
5 4 ssriv 
 |-  ( Clsd ` J ) C_ ~P X