Theorem 0npi

Description: The empty set is not a positive integer. (Contributed by NM, 26-Aug-1995) (New usage is discouraged.)

	Ref	Expression
Assertion	0npi	$$⊢\neg \varnothing \in 𝑵$$

Proof

Step	Hyp	Ref	Expression
1		eqid	$$⊢\varnothing =\varnothing$$
2		elni	$$⊢\varnothing \in 𝑵\leftrightarrow \left(\varnothing \in \mathrm{\omega }\wedge \varnothing \ne \varnothing \right)$$
3	2	simprbi	$$⊢\varnothing \in 𝑵\to \varnothing \ne \varnothing$$
4	3	necon2bi	$$⊢\varnothing =\varnothing \to \neg \varnothing \in 𝑵$$
5	1 4	ax-mp	$$⊢\neg \varnothing \in 𝑵$$