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

Theorem peano2nn 10014
Description: Peano postulate: a successor of a natural number is a natural number. (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 6694 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
2 fvelrnb 5776 . . . 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 8 . . 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 6108 . . . . . . 7  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  +  1 )  e.  _V
5 eqid 2438 . . . . . . . 8  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  =  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
6 oveq1 6090 . . . . . . . 8  |-  ( z  =  x  ->  (
z  +  1 )  =  ( x  + 
1 ) )
7 oveq1 6090 . . . . . . . 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 6699 . . . . . . 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 654 . . . . . 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 4867 . . . . . . . 8  |-  ( y  e.  om  ->  suc  y  e.  om )
11 fnfvelrn 5869 . . . . . . . 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 646 . . . . . . 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 10003 . . . . . . . 8  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
14 df-ima 4893 . . . . . . . 8  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
1513, 14eqtri 2458 . . . . . . 7  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
1612, 15syl6eleqr 2529 . . . . . 6  |-  ( y  e.  om  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  suc  y )  e.  NN )
179, 16eqeltrrd 2513 . . . . 5  |-  ( y  e.  om  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  y )  +  1 )  e.  NN )
18 oveq1 6090 . . . . . 6  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A  -> 
( ( ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om ) `  y )  +  1 )  =  ( A  +  1 ) )
1918eleq1d 2504 . . . . 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 213 . . . 4  |-  ( y  e.  om  ->  (
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  y )  =  A  ->  ( A  + 
1 )  e.  NN ) )
2120rexlimiv 2826 . . 3  |-  ( E. y  e.  om  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  y
)  =  A  -> 
( A  +  1 )  e.  NN )
223, 21sylbi 189 . 2  |-  ( A  e.  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  ->  ( A  +  1 )  e.  NN )
2322, 15eleq2s 2530 1  |-  ( A  e.  NN  ->  ( A  +  1 )  e.  NN )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 178    = wceq 1653    e. wcel 1726   E.wrex 2708   _Vcvv 2958    e. cmpt 4268   suc csuc 4585   omcom 4847   ran crn 4881    |` cres 4882   "cima 4883    Fn wfn 5451   ` cfv 5456  (class class class)co 6083   reccrdg 6669   1c1 8993    + caddc 8995   NNcn 10002
This theorem is referenced by:  dfnn2  10015  dfnn3  10016  peano2nnd  10019  nnind  10020  nnaddcl  10024  2nn  10135  3nn  10136  4nn  10137  5nn  10138  6nn  10139  7nn  10140  8nn  10141  9nn  10142  10nn  10143  nnunb  10219  nneo  10355  ser1const  11381  expp1  11390  facp1  11573  isercolllem1  12460  isercoll2  12464  climcndslem2  12632  climcnds  12633  harmonic  12640  trireciplem  12643  trirecip  12644  rpnnen2lem9  12824  sqr2irr  12850  rplpwr  13058  prmind2  13092  eulerthlem2  13173  pcmpt  13263  pockthi  13277  prmreclem6  13291  dec5nprm  13404  mulgnnp1  14900  1stcfb  17510  bcthlem3  19281  bcthlem4  19282  ovolunlem1a  19394  ovolicc2lem4  19418  voliunlem1  19446  volsup  19452  volsup2  19499  itg1climres  19608  mbfi1fseqlem5  19613  itg2monolem1  19644  itg2i1fseqle  19648  itg2i1fseq  19649  itg2i1fseq2  19650  itg2addlem  19652  itg2gt0  19654  itg2cnlem1  19655  aaliou3lem7  20268  emcllem1  20836  emcllem2  20837  emcllem3  20838  emcllem5  20840  emcllem6  20841  emcllem7  20842  bclbnd  21066  bposlem5  21074  2sqlem10  21160  dchrisumlem2  21186  logdivbnd  21252  pntrsumo1  21261  pntrsumbnd  21262  gxnn0suc  21854  opsqrlem5  23649  opsqrlem6  23650  esumpmono  24471  rrvsum  24714  zetacvg  24801  lgam1  24850  subfacp1lem6  24873  subfaclim  24876  iprodgam  25321  faclimlem1  25364  faclimlem2  25365  faclim2  25369  mblfinlem2  26246  volsupnfl  26253  nn0prpwlem  26327  seqpo  26453  incsequz  26454  incsequz2  26455  geomcau  26467  heiborlem6  26527  bfplem1  26533  jm2.27dlem4  27085  stoweidlem20  27747  wallispilem4  27795  wallispi2lem1  27798  wallispi2lem2  27799  stirlinglem4  27804  stirlinglem8  27808  stirlinglem11  27811  stirlinglem12  27812  stirlinglem13  27813
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-13 1728  ax-14 1730  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419  ax-sep 4332  ax-nul 4340  ax-pow 4379  ax-pr 4405  ax-un 4703
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-3or 938  df-3an 939  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-eu 2287  df-mo 2288  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ne 2603  df-ral 2712  df-rex 2713  df-reu 2714  df-rab 2716  df-v 2960  df-sbc 3164  df-csb 3254  df-dif 3325  df-un 3327  df-in 3329  df-ss 3336  df-pss 3338  df-nul 3631  df-if 3742  df-pw 3803  df-sn 3822  df-pr 3823  df-tp 3824  df-op 3825  df-uni 4018  df-iun 4097  df-br 4215  df-opab 4269  df-mpt 4270  df-tr 4305  df-eprel 4496  df-id 4500  df-po 4505  df-so 4506  df-fr 4543  df-we 4545  df-ord 4586  df-on 4587  df-lim 4588  df-suc 4589  df-om 4848  df-xp 4886  df-rel 4887  df-cnv 4888  df-co 4889  df-dm 4890  df-rn 4891  df-res 4892  df-ima 4893  df-iota 5420  df-fun 5458  df-fn 5459  df-f 5460  df-f1 5461  df-fo 5462  df-f1o 5463  df-fv 5464  df-ov 6086  df-recs 6635  df-rdg 6670  df-nn 10003
  Copyright terms: Public domain W3C validator