MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  peano2nn Structured version   Unicode version

Theorem peano2nn 10355
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
peano2nn  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  NN )

Proof of Theorem peano2nn
Dummy variables  x  y  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 frfnom 6911 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
2 fvelrnb 5760 . . . 4  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )  Fn  om  ->  ( A  e.  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  <->  E. y  e.  om  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A ) )
31, 2ax-mp 5 . . 3  |-  ( A  e.  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  <->  E. y  e.  om  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A )
4 ovex 6137 . . . . . . 7  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  +  1 )  e.  _V
5 eqid 2443 . . . . . . . 8  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
6 oveq1 6119 . . . . . . . 8  |-  ( z  =  x  ->  (
z  +  1 )  =  ( x  + 
1 ) )
7 oveq1 6119 . . . . . . . 8  |-  ( z  =  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  y )  ->  (
z  +  1 )  =  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y )  +  1 ) )
85, 6, 7frsucmpt2 6916 . . . . . . 7  |-  ( ( y  e.  om  /\  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  y )  +  1 )  e.  _V )  ->  ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  suc  y )  =  ( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  y )  +  1 ) )
94, 8mpan2 671 . . . . . 6  |-  ( y  e.  om  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  suc  y )  =  ( ( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  y )  +  1 ) )
10 peano2 6517 . . . . . . . 8  |-  ( y  e.  om  ->  suc  y  e.  om )
11 fnfvelrn 5861 . . . . . . . 8  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )  Fn  om  /\ 
suc  y  e.  om )  ->  ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  suc  y )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
)
121, 10, 11sylancr 663 . . . . . . 7  |-  ( y  e.  om  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  suc  y )  e.  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) )
13 df-nn 10344 . . . . . . . 8  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
14 df-ima 4874 . . . . . . . 8  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
1513, 14eqtri 2463 . . . . . . 7  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
1612, 15syl6eleqr 2534 . . . . . 6  |-  ( y  e.  om  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  suc  y )  e.  NN )
179, 16eqeltrrd 2518 . . . . 5  |-  ( y  e.  om  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  y )  +  1 )  e.  NN )
18 oveq1 6119 . . . . . 6  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A  -> 
( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  y )  +  1 )  =  ( A  +  1 ) )
1918eleq1d 2509 . . . . 5  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A  -> 
( ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y )  +  1 )  e.  NN  <->  ( A  + 
1 )  e.  NN ) )
2017, 19syl5ibcom 220 . . . 4  |-  ( y  e.  om  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  y )  =  A  ->  ( A  + 
1 )  e.  NN ) )
2120rexlimiv 2856 . . 3  |-  ( E. y  e.  om  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A  -> 
( A  +  1 )  e.  NN )
223, 21sylbi 195 . 2  |-  ( A  e.  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  ->  ( A  +  1 )  e.  NN )
2322, 15eleq2s 2535 1  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  NN )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    = wceq 1369    e. wcel 1756   E.wrex 2737   _Vcvv 2993    e. cmpt 4371   suc csuc 4742   ran crn 4862    |` cres 4863   "cima 4864    Fn wfn 5434   ` cfv 5439  (class class class)co 6112   omcom 6497   reccrdg 6886   1c1 9304    + caddc 9306   NNcn 10343
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-sep 4434  ax-nul 4442  ax-pow 4491  ax-pr 4552  ax-un 6393
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-ne 2622  df-ral 2741  df-rex 2742  df-reu 2743  df-rab 2745  df-v 2995  df-sbc 3208  df-csb 3310  df-dif 3352  df-un 3354  df-in 3356  df-ss 3363  df-pss 3365  df-nul 3659  df-if 3813  df-pw 3883  df-sn 3899  df-pr 3901  df-tp 3903  df-op 3905  df-uni 4113  df-iun 4194  df-br 4314  df-opab 4372  df-mpt 4373  df-tr 4407  df-eprel 4653  df-id 4657  df-po 4662  df-so 4663  df-fr 4700  df-we 4702  df-ord 4743  df-on 4744  df-lim 4745  df-suc 4746  df-xp 4867  df-rel 4868  df-cnv 4869  df-co 4870  df-dm 4871  df-rn 4872  df-res 4873  df-ima 4874  df-iota 5402  df-fun 5441  df-fn 5442  df-f 5443  df-f1 5444  df-fo 5445  df-f1o 5446  df-fv 5447  df-ov 6115  df-om 6498  df-recs 6853  df-rdg 6887  df-nn 10344
This theorem is referenced by:  dfnn2  10356  dfnn3  10357  peano2nnd  10360  nnind  10361  nnaddcl  10365  2nn  10500  3nn  10501  4nn  10502  5nn  10503  6nn  10504  7nn  10505  8nn  10506  9nn  10507  10nn  10508  nnunb  10596  nneo  10746  ser1const  11883  expp1  11893  facp1  12077  isercolllem1  13163  isercoll2  13167  climcndslem2  13334  climcnds  13335  harmonic  13342  trireciplem  13345  trirecip  13346  rpnnen2lem9  13526  sqr2irr  13552  rplpwr  13761  prmind2  13795  eulerthlem2  13878  pcmpt  13975  pockthi  13989  prmreclem6  14003  dec5nprm  14116  mulgnnp1  15656  1stcfb  19071  bcthlem3  20859  bcthlem4  20860  ovolunlem1a  21001  ovolicc2lem4  21025  voliunlem1  21053  volsup  21059  volsup2  21107  itg1climres  21214  mbfi1fseqlem5  21219  itg2monolem1  21250  itg2i1fseqle  21254  itg2i1fseq  21255  itg2i1fseq2  21256  itg2addlem  21258  itg2gt0  21260  itg2cnlem1  21261  aaliou3lem7  21837  emcllem1  22411  emcllem2  22412  emcllem3  22413  emcllem5  22415  emcllem6  22416  emcllem7  22417  bclbnd  22641  bposlem5  22649  2sqlem10  22735  dchrisumlem2  22761  logdivbnd  22827  pntrsumo1  22836  pntrsumbnd  22837  gxnn0suc  23773  opsqrlem5  25570  opsqrlem6  25571  nnindf  26111  esumpmono  26550  fibp1  26806  rrvsum  26859  zetacvg  27023  lgam1  27072  subfacp1lem6  27095  subfaclim  27098  iprodgam  27528  faclimlem1  27571  faclimlem2  27572  faclim2  27576  mblfinlem2  28455  volsupnfl  28462  nn0prpwlem  28543  seqpo  28669  incsequz  28670  incsequz2  28671  geomcau  28681  heiborlem6  28741  bfplem1  28747  jm2.27dlem4  29387  stoweidlem20  29841  wallispilem4  29889  wallispi2lem1  29892  wallispi2lem2  29893  stirlinglem4  29898  stirlinglem8  29902  stirlinglem11  29905  stirlinglem12  29906  stirlinglem13  29907  fzonn0p1p1  30242  wwlkext2clwwlk  30491  numclwwlk2lem1  30721  numclwlk2lem2f  30722
  Copyright terms: Public domain W3C validator