Database
BASIC TOPOLOGY
Topology
Closure and interior
sn0cld
Next ⟩
indiscld
Metamath Proof Explorer
Ascii
Unicode
Theorem
sn0cld
Description:
The closed sets of the topology
{ (/) }
.
(Contributed by
FL
, 5-Jan-2009)
Ref
Expression
Assertion
sn0cld
⊢
Clsd
⁡
∅
=
∅
Proof
Step
Hyp
Ref
Expression
1
0ex
⊢
∅
∈
V
2
discld
⊢
∅
∈
V
→
Clsd
⁡
𝒫
∅
=
𝒫
∅
3
1
2
ax-mp
⊢
Clsd
⁡
𝒫
∅
=
𝒫
∅
4
pw0
⊢
𝒫
∅
=
∅
5
4
fveq2i
⊢
Clsd
⁡
𝒫
∅
=
Clsd
⁡
∅
6
3
5
4
3eqtr3i
⊢
Clsd
⁡
∅
=
∅