Theorem 8olt9o

Description: Ordinal 8 is less than ordinal 9. (Contributed by BTernaryTau, 17-Oct-2026)

	Ref	Expression
Assertion	8olt9o	⊢ 8o ∈ 9o

Proof

Step	Hyp	Ref	Expression
1		8on	⊢ 8o ∈ On
2		sucidg	⊢ ( 8o ∈ On → 8o ∈ suc 8o )
3	1 2	ax-mp	⊢ 8o ∈ suc 8o
4		df-9o	⊢ 9o = suc 8o
5	3 4	eleqtrri	⊢ 8o ∈ 9o