Metamath Proof Explorer

Theorem 1on

Description: Ordinal 1 is an ordinal number. (Contributed by NM, 29-Oct-1995) Avoid ax-un . (Revised by BTernaryTau, 30-Nov-2024)

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

Proof

Step Hyp Ref Expression
1 df-1o 
 |-  1o = suc (/)
2 0elon 
 |-  (/) e. On
3 1oex 
 |-  1o e. _V
4 1 3 eqeltrri 
 |-  suc (/) e. _V
5 sucexeloni 
 |-  ( ( (/) e. On /\ suc (/) e. _V ) -> suc (/) e. On )
6 2 4 5 mp2an 
 |-  suc (/) e. On
7 1 6 eqeltri 
 |-  1o e. On