Theorem nn0suc

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

	Ref	Expression
Assertion	nn0suc	|- ( A e. _om -> ( A = (/) \/ E. x e. _om A = suc x ) )

Proof

Step	Hyp	Ref	Expression
1		df-ne	|- ( A =/= (/) <-> -. A = (/) )
2		nnsuc	|- ( ( A e. _om /\ A =/= (/) ) -> E. x e. _om A = suc x )
3	1 2	sylan2br	|- ( ( A e. _om /\ -. A = (/) ) -> E. x e. _om A = suc x )
4	3	ex	|- ( A e. _om -> ( -. A = (/) -> E. x e. _om A = suc x ) )
5	4	orrd	|- ( A e. _om -> ( A = (/) \/ E. x e. _om A = suc x ) )