Metamath Proof Explorer

Theorem 9on

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

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

Proof

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