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