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

Theorem 1nn 10338
Description: Peano postulate: 1 is a positive integer. (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 9386 . . . 4  |-  1  e.  _V
2 fr0g 6896 . . . 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 6895 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6500 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5845 . . . 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 672 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2514 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10328 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4858 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2463 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2516 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1369    e. wcel 1756   _Vcvv 2977   (/)c0 3642    e. cmpt 4355   ran crn 4846    |` cres 4847   "cima 4848    Fn wfn 5418   ` cfv 5423  (class class class)co 6096   omcom 6481   reccrdg 6870   1c1 9288    + caddc 9290   NNcn 10327
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 4418  ax-nul 4426  ax-pow 4475  ax-pr 4536  ax-un 6377  ax-1cn 9345
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 2573  df-ne 2613  df-ral 2725  df-rex 2726  df-reu 2727  df-rab 2729  df-v 2979  df-sbc 3192  df-csb 3294  df-dif 3336  df-un 3338  df-in 3340  df-ss 3347  df-pss 3349  df-nul 3643  df-if 3797  df-pw 3867  df-sn 3883  df-pr 3885  df-tp 3887  df-op 3889  df-uni 4097  df-iun 4178  df-br 4298  df-opab 4356  df-mpt 4357  df-tr 4391  df-eprel 4637  df-id 4641  df-po 4646  df-so 4647  df-fr 4684  df-we 4686  df-ord 4727  df-on 4728  df-lim 4729  df-suc 4730  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5386  df-fun 5425  df-fn 5426  df-f 5427  df-f1 5428  df-fo 5429  df-f1o 5430  df-fv 5431  df-om 6482  df-recs 6837  df-rdg 6871  df-nn 10328
This theorem is referenced by:  dfnn2  10340  dfnn3  10341  nnind  10345  nn1suc  10348  2nn  10484  nnunb  10580  1nn0  10600  nn0p1nn  10624  elz2  10668  1z  10681  neg1z  10686  nneo  10730  elnn1uz2  10936  zq  10964  rpnnen1lem4  10987  rpnnen1lem5  10988  ser1const  11867  exp1  11876  nnexpcl  11883  expnbnd  11998  fac1  12060  faccl  12066  faclbnd3  12073  faclbnd4lem1  12074  faclbnd4lem2  12075  faclbnd4lem3  12076  faclbnd4lem4  12077  lsw0  12272  cats1un  12375  revs1  12410  cats1fvn  12490  isercolllem2  13148  isercolllem3  13149  isercoll  13150  sumsn  13222  climcndslem1  13317  climcndslem2  13318  eftlub  13398  eirrlem  13491  xpnnenOLD  13497  rpnnen2lem5  13506  rpnnen2lem8  13509  rpnnen2  13513  dvdsle  13583  n2dvds1  13587  ndvdsp1  13618  gcd1  13721  1nprm  13773  1idssfct  13774  qden1elz  13840  phi1  13853  phiprm  13857  pcpre1  13914  pczpre  13919  pcmptcl  13958  pcmpt  13959  infpnlem2  13977  prmreclem1  13982  prmreclem6  13987  mul4sq  14020  vdwmc2  14045  vdwlem8  14054  vdwlem13  14059  vdwnnlem3  14063  5prm  14141  7prm  14143  11prm  14147  13prm  14148  17prm  14149  19prm  14150  37prm  14153  43prm  14154  83prm  14155  139prm  14156  163prm  14157  317prm  14158  631prm  14159  1259lem4  14163  1259lem5  14164  1259prm  14165  2503lem3  14168  2503prm  14169  4001lem1  14170  4001lem2  14171  4001lem3  14172  4001lem4  14173  4001prm  14174  baseid  14225  basendx  14228  2strstr  14279  rngstr  14290  lmodstr  14307  topgrpstr  14332  otpsstr  14339  ocndx  14344  ocid  14345  ressds  14357  resshom  14362  ressco  14363  oppcbas  14662  rescbas  14747  rescabs  14751  catstr  14872  ipostr  15328  mulg1  15639  mulg2  15641  oppgbas  15871  od1  16065  gex1  16095  efgsval2  16235  efgsp1  16239  torsubg  16341  pgpfaclem1  16587  mgpbas  16602  mgpds  16606  opprbas  16726  srabase  17264  srads  17272  opsrbas  17565  zlmbas  17954  znbas2  17977  thlbas  18126  thlle  18127  m2detleiblem1  18435  hauspwdom  19110  ressunif  19842  tuslem  19847  imasdsf1olem  19953  setsmsds  20056  tmslem  20062  tnglem  20231  tngbas  20232  tngds  20239  bcthlem4  20843  bcth3  20847  ovolmge0  20965  ovollb2  20977  ovolctb  20978  ovolunlem1a  20984  ovolunlem1  20985  ovoliunlem1  20990  ovoliun  20993  ovoliun2  20994  ovolicc1  21004  voliunlem1  21036  volsup  21042  ioombl1lem2  21045  ioombl1lem4  21047  uniioombllem1  21066  uniioombllem2  21068  uniioombllem6  21073  itg1climres  21197  itg2seq  21225  itg2monolem1  21233  itg2monolem2  21234  itg2monolem3  21235  itg2mono  21236  itg2i1fseq2  21239  itg2cnlem1  21244  aalioulem5  21807  aaliou2b  21812  aaliou3lem4  21817  aaliou3lem7  21820  dcubic1lem  22243  dcubic2  22244  mcubic  22247  log2ub  22349  emcllem6  22399  emcllem7  22400  ftalem7  22421  efnnfsumcl  22445  vmaprm  22460  efvmacl  22463  efchtdvds  22502  vma1  22509  prmorcht  22521  sqff1o  22525  pclogsum  22559  perfectlem1  22573  perfectlem2  22574  bpos1  22627  bposlem5  22632  lgsdir  22674  1lgs  22681  lgs1  22682  lgsquad2lem2  22703  dchrmusumlema  22747  dchrisum0lema  22768  trkgstr  22910  ttgbas  23128  ttgplusg  23129  ttgvsca  23131  eengstr  23231  usgraexmpl  23324  konigsberg  23613  gx1  23754  ipval2  24107  opsqrlem2  25550  ssnnssfz  26081  nnindf  26094  nn0min  26095  isarchi3  26209  resvbas  26305  rge0scvg  26384  zlmds  26398  qqh0  26418  qqh1  26419  esumfzf  26523  esumfsup  26524  esumpcvgval  26532  voliune  26650  eulerpartgbij  26760  eulerpartlemgs2  26768  fib2  26790  rrvsum  26842  ballotlem4  26886  ballotlemi1  26890  ballotlemii  26891  ballotlemic  26894  ballotlem1c  26895  signswbase  26960  signswplusg  26961  lgam1  27055  gam1  27056  fprodnncl  27473  prodsn  27478  nnrisefaccl  27527  faclimlem1  27554  ovoliunnfl  28438  voliunnfl  28440  volsupnfl  28441  nn0prpwlem  28522  nn0prpw  28523  incsequz  28649  bfplem1  28726  rrncmslem  28736  bezoutr1  29334  jm2.23  29350  rmydioph  29368  rmxdioph  29370  expdiophlem2  29376  expdioph  29377  sumsnd  29753  wallispilem4  29868  wallispi2lem1  29871  wallispi2lem2  29872  stirlinglem8  29881  stirlinglem11  29884  stirlinglem12  29885  stirlinglem13  29886  ccat2s1p1  30270  hlhilsbase  35592
  Copyright terms: Public domain W3C validator