Definition df-7o

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

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		c7o	Could not format 7o : No typesetting found for class 7o with typecode class
1		c6o	Could not format 6o : No typesetting found for class 6o with typecode class
2	1	csuc	Could not format suc 6o : No typesetting found for class suc 6o with typecode class
3	0 2	wceq	Could not format 7o = suc 6o : No typesetting found for wff 7o = suc 6o with typecode wff