Metamath Proof Explorer

Theorem 5on

Description: Ordinal 5 is an ordinal number. (Contributed by BTernaryTau, 4-Sep-2026)

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

Proof

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