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 ‘ 𝐽 ) ⊆ 𝒫 𝑋 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iscld.1 | ⊢ 𝑋 = ∪ 𝐽 | |
2 | 1 | cldss | ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ⊆ 𝑋 ) |
3 | velpw | ⊢ ( 𝑥 ∈ 𝒫 𝑋 ↔ 𝑥 ⊆ 𝑋 ) | |
4 | 2 3 | sylibr | ⊢ ( 𝑥 ∈ ( Clsd ‘ 𝐽 ) → 𝑥 ∈ 𝒫 𝑋 ) |
5 | 4 | ssriv | ⊢ ( Clsd ‘ 𝐽 ) ⊆ 𝒫 𝑋 |