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