This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC TOPOLOGY Topology Closure and interior clstop
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 ⊢ 𝑋 = ∪ 𝐽
Assertion
clstop ⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
Proof
Step
Hyp
Ref
Expression
1
clscld.1 ⊢ 𝑋 = ∪ 𝐽
2
1
topcld ⊢ ( 𝐽 ∈ Top → 𝑋 ∈ ( Clsd ‘ 𝐽 ) )
3
cldcls ⊢ ( 𝑋 ∈ ( Clsd ‘ 𝐽 ) → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )
4
2 3
syl ⊢ ( 𝐽 ∈ Top → ( ( cls ‘ 𝐽 ) ‘ 𝑋 ) = 𝑋 )