Metamath Proof Explorer

Theorem 3on

Description: Ordinal 3 is an ordinal number. (Contributed by Mario Carneiro, 5-Jan-2016)

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

Proof

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