Theorem nn0suc

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

	Ref	Expression
Assertion	nn0suc	⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	⊢ ( 𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅ )
2		nnsuc	⊢ ( ( 𝐴 ∈ ω ∧ 𝐴 ≠ ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
3	1 2	sylan2br	⊢ ( ( 𝐴 ∈ ω ∧ ¬ 𝐴 = ∅ ) → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 )
4	3	ex	⊢ ( 𝐴 ∈ ω → ( ¬ 𝐴 = ∅ → ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )
5	4	orrd	⊢ ( 𝐴 ∈ ω → ( 𝐴 = ∅ ∨ ∃ 𝑥 ∈ ω 𝐴 = suc 𝑥 ) )