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

Metamath Proof Explorer

Theorem nnn0

Description: The set of positive integers is nonempty. (Contributed by Glauco Siliprandi, 8-Apr-2021)

		Ref	Expression
	Assertion	nnn0	$⊢ ℕ \neq \emptyset$

Step	Hyp	Ref	Expression
1		1nn	$⊢ 1 \in ℕ$
2	1	ne0ii	$⊢ ℕ \neq \emptyset$