Metamath Proof Explorer

Theorem 4on

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

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

Proof

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