Theorem 1onn

Description: The ordinal 1 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un , see 1onnALT . Lemma 2.2 of Schloeder p. 4. (Contributed by NM, 29-Oct-1995) Avoid ax-un . (Revised by BTernaryTau, 1-Dec-2024)

	Ref	Expression
Assertion	1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$

Proof

Step	Hyp	Ref	Expression
1		1on	$$⊢1_{𝑜}\in \mathrm{On}$$
2		1ellim	$$⊢\mathrm{Lim}x\to 1_{𝑜}\in x$$
3	2	ax-gen	$$⊢\forall x\left(\mathrm{Lim}x\to 1_{𝑜}\in x\right)$$
4		elom	$$⊢1_{𝑜}\in \mathrm{\omega }\leftrightarrow \left(1_{𝑜}\in \mathrm{On}\wedge \forall x\left(\mathrm{Lim}x\to 1_{𝑜}\in x\right)\right)$$
5	1 3 4	mpbir2an	$$⊢1_{𝑜}\in \mathrm{\omega }$$