Metamath Proof Explorer


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 syl6ibr
 |-  ( 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 )