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

Theorem 1nn 10016
Description: Peano postulate: 1 is a natural number. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
1nn  |-  1  e.  NN

Proof of Theorem 1nn
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 1ex 9091 . . . 4  |-  1  e.  _V
2 fr0g 6696 . . . 4  |-  ( 1  e.  _V  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1 )
31, 2ax-mp 5 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1
4 frfnom 6695 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 4867 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5870 . . . 4  |-  ( ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )  Fn  om  /\  (/)  e.  om )  -> 
( ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om ) `  (/) )  e.  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) )
74, 5, 6mp2an 655 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2509 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10006 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4894 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2458 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2511 1  |-  1  e.  NN
Colors of variables: wff set class
Syntax hints:    = wceq 1653    e. wcel 1726   _Vcvv 2958   (/)c0 3630    e. cmpt 4269   omcom 4848   ran crn 4882    |` cres 4883   "cima 4884    Fn wfn 5452   ` cfv 5457  (class class class)co 6084   reccrdg 6670   1c1 8996    + caddc 8998   NNcn 10005
This theorem is referenced by:  dfnn2  10018  dfnn3  10019  nnind  10023  nn1suc  10026  2nn  10138  nnunb  10222  1nn0  10242  nn0p1nn  10264  elz2  10303  1z  10316  nneo  10358  elnn1uz2  10557  zq  10585  rpnnen1lem4  10608  rpnnen1lem5  10609  ser1const  11384  exp1  11392  nnexpcl  11399  expnbnd  11513  fac1  11575  faccl  11581  faclbnd3  11588  faclbnd4lem1  11589  faclbnd4lem2  11590  faclbnd4lem3  11591  faclbnd4lem4  11592  cats1un  11795  revs1  11802  cats1fvn  11827  isercolllem2  12464  isercolllem3  12465  isercoll  12466  sumsn  12539  climcndslem1  12634  climcndslem2  12635  eftlub  12715  eirrlem  12808  xpnnenOLD  12814  rpnnen2lem5  12823  rpnnen2lem8  12826  rpnnen2  12830  nthruz  12856  dvdsle  12900  ndvdsp1  12934  bitsfzolem  12951  bitsfzo  12952  bitsinv1lem  12958  gcd1  13037  1nprm  13089  1idssfct  13090  qden1elz  13154  phi1  13167  phiprm  13171  pcpre1  13221  pczpre  13226  pcmptcl  13265  pcmpt  13266  infpnlem2  13284  prmreclem1  13289  prmreclem6  13294  mul4sq  13327  vdwmc2  13352  vdwlem8  13361  vdwlem13  13366  vdwnnlem3  13370  5prm  13436  7prm  13438  11prm  13442  13prm  13443  17prm  13444  19prm  13445  37prm  13448  43prm  13449  83prm  13450  139prm  13451  163prm  13452  317prm  13453  631prm  13454  1259lem4  13458  1259lem5  13459  1259prm  13460  2503lem3  13463  2503prm  13464  4001lem1  13465  4001lem2  13466  4001lem3  13467  4001lem4  13468  4001prm  13469  baseid  13516  basendx  13519  2strstr  13570  rngstr  13581  lmodstr  13598  topgrpstr  13621  otpsstr  13628  ocndx  13633  ocid  13634  ressds  13646  resshom  13651  ressco  13652  oppcbas  13949  rescbas  14034  rescabs  14038  catstr  14159  ipostr  14584  mulg1  14902  mulg2  14904  oppgbas  15152  od1  15200  gex1  15230  efgsval2  15370  efgsp1  15374  torsubg  15474  pgpfaclem1  15644  mgpbas  15659  mgpds  15663  opprbas  15739  srabase  16255  srads  16262  opsrbas  16544  zlmbas  16804  znbas2  16825  thlbas  16928  thlle  16929  hauspwdom  17569  ressunif  18297  tuslem  18302  imasdsf1olem  18408  setsmsds  18511  tmslem  18517  tnglem  18686  tngbas  18687  tngds  18694  bcthlem4  19285  bcth3  19289  ovolmge0  19378  ovollb2  19390  ovolctb  19391  ovolunlem1a  19397  ovolunlem1  19398  ovoliunlem1  19403  ovoliun  19406  ovoliun2  19407  ovolicc1  19417  voliunlem1  19449  volsup  19455  ioombl1lem2  19458  ioombl1lem4  19460  uniioombllem1  19478  uniioombllem2  19480  uniioombllem6  19485  itg1climres  19609  itg2seq  19637  itg2monolem1  19645  itg2monolem2  19646  itg2monolem3  19647  itg2mono  19648  itg2i1fseq2  19651  itg2cnlem1  19656  aalioulem5  20258  aaliou2b  20263  aaliou3lem4  20268  aaliou3lem7  20271  dcubic1lem  20688  dcubic2  20689  mcubic  20692  log2ub  20794  emcllem6  20844  emcllem7  20845  ftalem7  20866  efnnfsumcl  20890  vmaprm  20905  efvmacl  20908  efchtdvds  20947  vma1  20954  prmorcht  20966  sqff1o  20970  pclogsum  21004  perfectlem1  21018  perfectlem2  21019  bpos1  21072  bposlem5  21077  lgsdir  21119  1lgs  21126  lgs1  21127  lgsquad2lem2  21148  dchrmusumlema  21192  dchrisum0lema  21213  usgraexmpl  21425  konigsberg  21714  gx1  21855  ipval2  22208  opsqrlem2  23649  ssnnssfz  24153  rge0scvg  24340  zlmds  24353  qqh0  24373  qqh1  24374  esumfzf  24464  esumfsup  24465  esumpcvgval  24473  voliune  24590  rrvsum  24717  ballotlem4  24761  ballotlemi1  24765  ballotlemii  24766  ballotlemic  24769  ballotlem1c  24770  lgam1  24853  gam1  24854  fprodnncl  25286  prodsn  25291  nnrisefaccl  25340  faclimlem1  25367  ovoliunnfl  26260  voliunnfl  26262  volsupnfl  26263  nn0prpwlem  26339  nn0prpw  26340  incsequz  26466  bfplem1  26545  rrncmslem  26555  bezoutr1  27065  jm2.23  27081  rmydioph  27099  rmxdioph  27101  expdiophlem2  27107  expdioph  27108  sumsnd  27687  wallispilem4  27807  wallispi2lem1  27810  wallispi2lem2  27811  stirlinglem8  27820  stirlinglem11  27823  stirlinglem12  27824  stirlinglem13  27825  lswrd0  28295  hlhilsbase  32814
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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 4333  ax-nul 4341  ax-pow 4380  ax-pr 4406  ax-un 4704  ax-1cn 9053
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 4216  df-opab 4270  df-mpt 4271  df-tr 4306  df-eprel 4497  df-id 4501  df-po 4506  df-so 4507  df-fr 4544  df-we 4546  df-ord 4587  df-on 4588  df-lim 4589  df-suc 4590  df-om 4849  df-xp 4887  df-rel 4888  df-cnv 4889  df-co 4890  df-dm 4891  df-rn 4892  df-res 4893  df-ima 4894  df-iota 5421  df-fun 5459  df-fn 5460  df-f 5461  df-f1 5462  df-fo 5463  df-f1o 5464  df-fv 5465  df-recs 6636  df-rdg 6671  df-nn 10006
  Copyright terms: Public domain W3C validator