Theorem nnsuc

Description: A nonzero natural number is a successor. (Contributed by NM, 18-Feb-2004)

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

Proof

Step	Hyp	Ref	Expression
1		nnlim	|- ( A e. _om -> -. Lim A )
2	1	adantr	|- ( ( A e. _om /\ A =/= (/) ) -> -. Lim A )
3		nnord	|- ( A e. _om -> Ord A )
4		orduninsuc	|- ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )
5	4	adantr	|- ( ( Ord A /\ A =/= (/) ) -> ( A = U. A <-> -. E. x e. On A = suc x ) )
6		df-lim	|- ( Lim A <-> ( Ord A /\ A =/= (/) /\ A = U. A ) )
7	6	biimpri	|- ( ( Ord A /\ A =/= (/) /\ A = U. A ) -> Lim A )
8	7	3expia	|- ( ( Ord A /\ A =/= (/) ) -> ( A = U. A -> Lim A ) )
9	5 8	sylbird	|- ( ( Ord A /\ A =/= (/) ) -> ( -. E. x e. On A = suc x -> Lim A ) )
10	3 9	sylan	|- ( ( A e. _om /\ A =/= (/) ) -> ( -. E. x e. On A = suc x -> Lim A ) )
11	2 10	mt3d	|- ( ( A e. _om /\ A =/= (/) ) -> E. x e. On A = suc x )
12		eleq1	|- ( A = suc x -> ( A e. _om <-> suc x e. _om ) )
13	12	biimpcd	|- ( A e. _om -> ( A = suc x -> suc x e. _om ) )
14		peano2b	|- ( x e. _om <-> suc x e. _om )
15	13 14	imbitrrdi	|- ( A e. _om -> ( A = suc x -> x e. _om ) )
16	15	ancrd	|- ( A e. _om -> ( A = suc x -> ( x e. _om /\ A = suc x ) ) )
17	16	adantld	|- ( A e. _om -> ( ( x e. On /\ A = suc x ) -> ( x e. _om /\ A = suc x ) ) )
18	17	reximdv2	|- ( A e. _om -> ( E. x e. On A = suc x -> E. x e. _om A = suc x ) )
19	18	adantr	|- ( ( A e. _om /\ A =/= (/) ) -> ( E. x e. On A = suc x -> E. x e. _om A = suc x ) )
20	11 19	mpd	|- ( ( A e. _om /\ A =/= (/) ) -> E. x e. _om A = suc x )