Theorem 1pi

Description: Ordinal 'one' is a positive integer. (Contributed by NM, 29-Oct-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	1pi	$$⊢1_{𝑜}\in 𝑵$$

Proof

Step	Hyp	Ref	Expression
1		1onn	$$⊢1_{𝑜}\in \mathrm{\omega }$$
2		1n0	$$⊢1_{𝑜}\ne \varnothing$$
3		elni	$$⊢1_{𝑜}\in 𝑵\leftrightarrow \left(1_{𝑜}\in \mathrm{\omega }\wedge 1_{𝑜}\ne \varnothing \right)$$
4	1 2 3	mpbir2an	$$⊢1_{𝑜}\in 𝑵$$