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

Metamath Proof Explorer

Theorem 2on0

Description: Ordinal two is not zero. (Contributed by Scott Fenton, 17-Jun-2011)

Ref Expression
Assertion 2on0 
|- 2o =/= (/)

Proof

Step Hyp Ref Expression
1 df-2o 
 |-  2o = suc 1o
2 nsuceq0 
 |-  suc 1o =/= (/)
3 1 2 eqnetri 
 |-  2o =/= (/)