Theorem 1olt9o

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

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

Proof

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