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

Metamath Proof Explorer

Theorem 0cld

Description: The empty set is closed. Part of Theorem 6.1(1) of Munkres p. 93. (Contributed by NM, 4-Oct-2006)

Ref Expression
Assertion 0cld ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J

Proof

Step Hyp Ref Expression
1 dif0 ⊢ ⋃ J ∖ ∅ = ⋃ J
2 1 topopn ⊢ J ∈ Top → ⋃ J ∖ ∅ ∈ J
3 0ss ⊢ ∅ ⊆ ⋃ J
4 eqid ⊢ ⋃ J = ⋃ J
5 4 iscld2 ⊢ J ∈ Top ∧ ∅ ⊆ ⋃ J → ∅ ∈ Clsd ⁡ J ↔ ⋃ J ∖ ∅ ∈ J
6 3 5 mpan2 ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J ↔ ⋃ J ∖ ∅ ∈ J
7 2 6 mpbird ⊢ J ∈ Top → ∅ ∈ Clsd ⁡ J