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