Metamath Proof Explorer

Theorem 8on

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

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

Proof

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