Theorem 4olt9o

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

	Ref	Expression
Assertion	4olt9o	Could not format assertion : No typesetting found for |- 4o e. 9o with typecode |-

Proof

Step	Hyp	Ref	Expression
1		4on	$$⊢4_{𝑜}\in \mathrm{On}$$
2		sucidg	$$⊢4_{𝑜}\in \mathrm{On}\to 4_{𝑜}\in \mathrm{suc}{4}_{𝑜}$$
3	1 2	ax-mp	$$⊢4_{𝑜}\in \mathrm{suc}{4}_{𝑜}$$
4		df-5o	Could not format 5o = suc 4o : No typesetting found for |- 5o = suc 4o with typecode |-
5	3 4	eleqtrri	Could not format 4o e. 5o : No typesetting found for |- 4o e. 5o with typecode |-
6		5olt9o	Could not format 5o e. 9o : No typesetting found for |- 5o e. 9o with typecode |-
7		9on	Could not format 9o e. On : No typesetting found for |- 9o e. On with typecode |-
8		ontr1	Could not format ( 9o e. On -> ( ( 4o e. 5o /\ 5o e. 9o ) -> 4o e. 9o ) ) : No typesetting found for |- ( 9o e. On -> ( ( 4o e. 5o /\ 5o e. 9o ) -> 4o e. 9o ) ) with typecode |-
9	7 8	ax-mp	Could not format ( ( 4o e. 5o /\ 5o e. 9o ) -> 4o e. 9o ) : No typesetting found for |- ( ( 4o e. 5o /\ 5o e. 9o ) -> 4o e. 9o ) with typecode |-
10	5 6 9	mp2an	Could not format 4o e. 9o : No typesetting found for |- 4o e. 9o with typecode |-