Metamath Proof Explorer

Theorem sn0topon

Description: The singleton of the empty set is a topology on the empty set. (Contributed by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion sn0topon ⊢ ∅ ∈ TopOn ⁡ ∅

Proof

Step Hyp Ref Expression
1 pw0 ⊢ 𝒫 ∅ = ∅
2 0ex ⊢ ∅ ∈ V
3 distopon ⊢ ∅ ∈ V → 𝒫 ∅ ∈ TopOn ⁡ ∅
4 2 3 ax-mp ⊢ 𝒫 ∅ ∈ TopOn ⁡ ∅
5 1 4 eqeltrri ⊢ ∅ ∈ TopOn ⁡ ∅