This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑵$

Step	Hyp	Ref	Expression
1		1onn	$⊢ 1_{𝑜} \in ω$
2		1n0	$⊢ 1_{𝑜} \neq \emptyset$
3		elni	$⊢ 1_{𝑜} \in 𝑵 \leftrightarrow (1_{𝑜} \in ω \land 1_{𝑜} \neq \emptyset)$
4	1 2 3	mpbir2an	$⊢ 1_{𝑜} \in 𝑵$