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

Metamath Proof Explorer

Theorem 0ntop

Description: The empty set is not a topology. (Contributed by FL, 1-Jun-2008)

Ref Expression
Assertion 0ntop ⊢ ¬ ∅ ∈ Top

Proof

Step Hyp Ref Expression
1 noel ⊢ ¬ ∅ ∈ ∅
2 0opn ⊢ ∅ ∈ Top → ∅ ∈ ∅
3 1 2 mto ⊢ ¬ ∅ ∈ Top