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 ( 𝐽 ∈ Top → ∅ ∈ ( Clsd ‘ 𝐽 ) )

Proof

Step Hyp Ref Expression
1 dif0 ( 𝐽 ∖ ∅ ) = 𝐽
2 1 topopn ( 𝐽 ∈ Top → ( 𝐽 ∖ ∅ ) ∈ 𝐽 )
3 0ss ∅ ⊆ 𝐽
4 eqid 𝐽 = 𝐽
5 4 iscld2 ( ( 𝐽 ∈ Top ∧ ∅ ⊆ 𝐽 ) → ( ∅ ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐽 ∖ ∅ ) ∈ 𝐽 ) )
6 3 5 mpan2 ( 𝐽 ∈ Top → ( ∅ ∈ ( Clsd ‘ 𝐽 ) ↔ ( 𝐽 ∖ ∅ ) ∈ 𝐽 ) )
7 2 6 mpbird ( 𝐽 ∈ Top → ∅ ∈ ( Clsd ‘ 𝐽 ) )