Theorem 3olt9o

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

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

Proof

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