Theorem 2olt9o

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

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

Proof

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