Definition df-6o

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

	Ref	Expression
Assertion	df-6o	⊢ 6o = suc 5o

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c6o	⊢ 6o
1		c5o	⊢ 5o
2	1	csuc	⊢ suc 5o
3	0 2	wceq	⊢ 6o = suc 5o