Definition df-5o

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

	Ref	Expression
Assertion	df-5o	Could not format assertion : No typesetting found for |- 5o = suc 4o with typecode |-

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c5o	Could not format 5o : No typesetting found for class 5o with typecode class
1		c4o	$$class{4}_{𝑜}$$
2	1	csuc	$$class\mathrm{suc}{4}_{𝑜}$$
3	0 2	wceq	Could not format 5o = suc 4o : No typesetting found for wff 5o = suc 4o with typecode wff