Metamath Proof Explorer

Theorem 2on

Description: Ordinal 2 is an ordinal number. (Contributed by NM, 18-Feb-2004) (Proof shortened by Andrew Salmon, 12-Aug-2011)

Ref Expression
Assertion 2on 
|- 2o e. On

Proof

Step Hyp Ref Expression
1 df-2o 
 |-  2o = suc 1o
2 1on 
 |-  1o e. On
3 2 onsuci 
 |-  suc 1o e. On
4 1 3 eqeltri 
 |-  2o e. On