Metamath Proof Explorer

Definition df-5o

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

Ref Expression
Assertion df-5o 
|- 5o = suc 4o

Detailed syntax breakdown

Step Hyp Ref Expression
0 c5o 
 |-  5o
1 c4o 
 |-  4o
2 1 csuc 
 |-  suc 4o
3 0 2 wceq 
 |-  5o = suc 4o