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 ≠ ∅