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