Theorem 2onn

Description: The ordinal 2 is a natural number. For a shorter proof using Peano's postulates that depends on ax-un , see 2onnALT . (Contributed by NM, 28-Sep-2004) Avoid ax-un . (Revised by BTernaryTau, 1-Dec-2024)

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

Proof

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