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 
|- -. (/) e. Top

Proof

Step Hyp Ref Expression
1 noel 
 |-  -. (/) e. (/)
2 0opn 
 |-  ( (/) e. Top -> (/) e. (/) )
3 1 2 mto 
 |-  -. (/) e. Top