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 ‘ 𝐽 ) ) |
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 ‘ 𝐽 ) ) |