This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cls0

Description: The closure of the empty set. (Contributed by NM, 2-Oct-2007) (Proof shortened by Jim Kingdon, 12-Mar-2023)

Ref Expression
Assertion cls0 ⊢ J ∈ Top → cls ⁡ J ⁡ ∅ = ∅

Proof

Step Hyp Ref Expression
1 0cld ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J
2 cldcls ⊢ ∅ ∈ Clsd ⁡ J → cls ⁡ J ⁡ ∅ = ∅
3 1 2 syl ⊢ J ∈ Top → cls ⁡ J ⁡ ∅ = ∅