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

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