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

Metamath Proof Explorer

Theorem nn0suc

Description: A natural number is either 0 or a successor. (Contributed by NM, 27-May-1998)

		Ref	Expression
	Assertion	nn0suc	$⊢ A \in ω \to (A = \emptyset \lor \exists x \in ω A = suc x)$

Step	Hyp	Ref	Expression
1		df-ne	$⊢ A \neq \emptyset \leftrightarrow \neg A = \emptyset$
2		nnsuc	$⊢ (A \in ω \land A \neq \emptyset) \to \exists x \in ω A = suc x$
3	1 2	sylan2br	$⊢ (A \in ω \land \neg A = \emptyset) \to \exists x \in ω A = suc x$
4	3	ex	$⊢ A \in ω \to (\neg A = \emptyset \to \exists x \in ω A = suc x)$
5	4	orrd	$⊢ A \in ω \to (A = \emptyset \lor \exists x \in ω A = suc x)$