Metamath Proof Explorer

Theorem 2onn

Description: The ordinal 2 is a natural number. (Contributed by NM, 28-Sep-2004)

Ref Expression
Assertion 2onn 
|- 2o e. _om

Proof

Step Hyp Ref Expression
1 df-2o 
 |-  2o = suc 1o
2 1onn 
 |-  1o e. _om
3 peano2 
 |-  ( 1o e. _om -> suc 1o e. _om )
4 2 3 ax-mp 
 |-  suc 1o e. _om
5 1 4 eqeltri 
 |-  2o e. _om