Metamath Proof Explorer

Theorem 1on

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995)

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

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 0elon 
 |-  (/) e. On
3 2 onsuci 
 |-  suc (/) e. On
4 1 3 eqeltri 
 |-  1o e. On