Metamath Proof Explorer

Theorem sn0top

Description: The singleton of the empty set is a topology. (Contributed by Stefan Allan, 3-Mar-2006) (Proof shortened by Mario Carneiro, 13-Aug-2015)

Ref Expression
Assertion sn0top ⊢ ∅ ∈ Top

Proof

Step Hyp Ref Expression
1 sn0topon ⊢ ∅ ∈ TopOn ⁡ ∅
2 1 topontopi ⊢ ∅ ∈ Top