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