Metamath Proof Explorer

Definition df-9o

Description: Define the ordinal number 9. (Contributed by BTernaryTau, 2-Sep-2026)

Ref Expression
Assertion df-9o 
|- 9o = suc 8o

Detailed syntax breakdown

Step Hyp Ref Expression
0 c9o 
 |-  9o
1 c8o 
 |-  8o
2 1 csuc 
 |-  suc 8o
3 0 2 wceq 
 |-  9o = suc 8o