Database
BASIC TOPOLOGY
Topology
Closure and interior
clstop
Metamath Proof Explorer
Description: The closure of a topology's underlying set is the entire set.
(Contributed by NM , 5-Oct-2007) (Proof shortened by Jim Kingdon , 11-Mar-2023)
Ref
Expression
Hypothesis
clscld.1
⊢ X = ⋃ J
Assertion
clstop
⊢ J ∈ Top → cls ⁡ J ⁡ X = X
Proof
Step
Hyp
Ref
Expression
1
clscld.1
⊢ X = ⋃ J
2
1
topcld
⊢ J ∈ Top → X ∈ Clsd ⁡ J
3
cldcls
⊢ X ∈ Clsd ⁡ J → cls ⁡ J ⁡ X = X
4
2 3
syl
⊢ J ∈ Top → cls ⁡ J ⁡ X = X