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

Theorem 1nn 10653
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 9669 . . . 4  |-  1  e.  _V
2 fr0g 7184 . . . 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 7183 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6744 . . . 4  |-  (/)  e.  om
6 fnfvelrn 6047 . . . 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 683 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2537 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10643 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4869 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2484 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2539 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1455    e. wcel 1898   _Vcvv 3057   (/)c0 3743    |-> cmpt 4477   ran crn 4857    |` cres 4858   "cima 4859    Fn wfn 5600   ` cfv 5605  (class class class)co 6320   omcom 6724   reccrdg 7158   1c1 9571    + caddc 9573   NNcn 10642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-8 1900  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4541  ax-nul 4550  ax-pow 4598  ax-pr 4656  ax-un 6615  ax-1cn 9628
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3or 992  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-ral 2754  df-rex 2755  df-reu 2756  df-rab 2758  df-v 3059  df-sbc 3280  df-csb 3376  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-pss 3432  df-nul 3744  df-if 3894  df-pw 3965  df-sn 3981  df-pr 3983  df-tp 3985  df-op 3987  df-uni 4213  df-iun 4294  df-br 4419  df-opab 4478  df-mpt 4479  df-tr 4514  df-eprel 4767  df-id 4771  df-po 4777  df-so 4778  df-fr 4815  df-we 4817  df-xp 4862  df-rel 4863  df-cnv 4864  df-co 4865  df-dm 4866  df-rn 4867  df-res 4868  df-ima 4869  df-pred 5403  df-ord 5449  df-on 5450  df-lim 5451  df-suc 5452  df-iota 5569  df-fun 5607  df-fn 5608  df-f 5609  df-f1 5610  df-fo 5611  df-f1o 5612  df-fv 5613  df-om 6725  df-wrecs 7059  df-recs 7121  df-rdg 7159  df-nn 10643
This theorem is referenced by:  dfnn2  10655  dfnn3  10656  nnind  10660  nn1suc  10663  2nn  10801  nnunb  10899  1nn0  10919  nn0p1nn  10943  elz2  10988  1z  11001  neg1z  11007  nneo  11053  elnn1uz2  11269  zq  11304  rpnnen1lem4  11327  rpnnen1lem5  11328  ser1const  12307  exp1  12316  nnexpcl  12323  expnbnd  12439  fac1  12501  faccl  12507  faclbnd3  12515  faclbnd4lem1  12516  faclbnd4lem2  12517  faclbnd4lem3  12518  faclbnd4lem4  12519  lsw0  12754  eqs1  12792  ccat2s1p1  12804  cats1un  12875  revs1  12913  cats1fvn  12997  relexpsucnnl  13150  relexpaddg  13171  isercolllem2  13784  isercolllem3  13785  isercoll  13786  sumsn  13862  climcndslem1  13962  climcndslem2  13963  fprodnncl  14064  prodsn  14071  prodsnf  14073  nnrisefaccl  14127  eftlub  14218  eirrlem  14311  rpnnen2lem5  14326  rpnnen2lem8  14329  rpnnen2  14333  dvdsle  14405  n2dvds1  14409  ndvdsp1  14445  gcd1  14551  lcmslefacOLD  14641  1nprm  14684  1idssfct  14685  qden1elz  14761  phi1  14776  phiprm  14780  pcpre1  14847  pczpre  14852  pcmptcl  14891  pcmpt  14892  infpnlem2  14910  prmreclem1  14915  prmreclem6  14920  mul4sq  14953  vdwmc2  14984  vdwlem8  14993  vdwlem13  14998  vdwnnlem3  15002  prmocl  15047  prmop1  15051  fvprmselelfz  15057  fvprmselgcd1  15058  prmolefac  15059  prmodvdslcmf  15060  prmormapnnOLD  15069  prmorlefacOLD  15073  prmordvdslcmfOLD  15074  prmordvdslcmsOLDOLD  15076  prmgapprmo  15088  5prm  15135  7prm  15137  11prm  15141  13prm  15142  17prm  15143  19prm  15144  37prm  15147  43prm  15148  83prm  15149  139prm  15150  163prm  15151  317prm  15152  631prm  15153  1259lem4  15160  1259lem5  15161  1259prm  15162  2503lem3  15165  2503prm  15166  4001lem1  15167  4001lem2  15168  4001lem3  15169  4001lem4  15170  4001prm  15171  baseid  15224  basendx  15228  basendxnn  15229  ressval3d  15241  1strstr  15281  2strstr  15285  rngstr  15299  lmodstr  15316  topgrpstr  15341  otpsstr  15348  ocndx  15353  ocid  15354  ressds  15366  resshom  15371  ressco  15372  slotsbhcdif  15373  oppcbas  15678  rescbas  15789  rescabs  15793  catstr  15917  estrreslem1  16077  ipostr  16454  mulg1  16820  mulg2  16822  oppgbas  17057  od1  17265  gex1  17298  efgsval2  17438  efgsp1  17442  torsubg  17547  pgpfaclem1  17769  mgpbas  17784  mgpds  17788  opprbas  17912  srabase  18456  srads  18464  opsrbas  18757  zlmbas  19144  znbas2  19165  thlbas  19314  thlle  19315  pmatcollpw3fi1lem2  19866  hauspwdom  20571  ressunif  21332  tuslem  21337  imasdsf1olem  21443  setsmsds  21546  tmslem  21552  tnglem  21703  tngbas  21704  tngds  21711  bcthlem4  22350  bcth3  22354  ovolmge0  22485  ovollb2  22497  ovolctb  22498  ovolunlem1a  22504  ovolunlem1  22505  ovoliunlem1  22510  ovoliun  22513  ovoliun2  22514  ovolicc1  22524  voliunlem1  22559  volsup  22565  ioombl1lem2  22568  ioombl1lem4  22570  uniioombllem1  22594  uniioombllem2  22596  uniioombllem2OLD  22597  uniioombllem6  22602  itg1climres  22728  itg2seq  22756  itg2monolem1  22764  itg2monolem2  22765  itg2monolem3  22766  itg2mono  22767  itg2i1fseq2  22770  itg2cnlem1  22775  aalioulem5  23348  aaliou2b  23353  aaliou3lem4  23358  aaliou3lem7  23361  dcubic1lem  23825  dcubic2  23826  mcubic  23829  log2ub  23931  emcllem6  23982  emcllem7  23983  lgam1  24045  gam1  24046  ftalem7  24061  efnnfsumcl  24085  vmaprm  24100  efvmacl  24103  efchtdvds  24142  vma1  24149  prmorcht  24161  sqff1o  24165  pclogsum  24199  perfectlem1  24213  perfectlem2  24214  bpos1  24267  bposlem5  24272  lgsdir  24314  1lgs  24321  lgs1  24322  lgsquad2lem2  24343  dchrmusumlema  24387  dchrisum0lema  24408  trkgstr  24548  ttgbas  24963  ttgplusg  24964  ttgvsca  24966  eengstr  25066  usgraexmplef  25184  konigsberg  25771  gx1  26046  ipval2  26399  opsqrlem2  27850  ssnnssfz  28419  nnindf  28434  nn0min  28436  isarchi3  28555  resvbas  28646  rge0scvg  28806  zlmds  28819  qqh0  28839  qqh1  28840  esumfzf  28941  esumfsup  28942  esumpcvgval  28950  voliune  29102  eulerpartgbij  29255  eulerpartlemgs2  29263  fib2  29285  rrvsum  29337  ballotlem4  29381  ballotlemi1  29385  ballotlemii  29386  ballotlemic  29389  ballotlem1c  29390  ballotlemi1OLD  29423  ballotlemiiOLD  29424  ballotlemicOLD  29427  ballotlem1cOLD  29428  faclimlem1  30429  nn0prpwlem  31028  nn0prpw  31029  poimirlem32  32018  ovoliunnfl  32028  voliunnfl  32030  volsupnfl  32031  incsequz  32123  bfplem1  32200  rrncmslem  32210  hlhilsbase  35556  bezoutr1  35882  jm2.23  35897  rmydioph  35915  rmxdioph  35917  expdiophlem2  35923  expdioph  35924  relexp2  36315  iunrelexpmin1  36346  iunrelexpmin2  36350  dftrcl3  36358  fvtrcllb1d  36360  cotrcltrcl  36363  corcltrcl  36377  cotrclrcl  36380  prmunb2  36704  sumsnd  37388  sumsnf  37733  mccl  37764  sumnnodd  37796  wallispilem4  38031  wallispi2lem1  38034  wallispi2lem2  38035  stirlinglem8  38044  stirlinglem11  38047  stirlinglem12  38048  stirlinglem13  38049  fourierdlem31  38101  fourierdlem31OLD  38102  nnfoctbdjlem  38398  hoicvr  38477  hoicvrrex  38485  hoidmvlelem3  38526  ovnhoilem1  38530  ovnhoilem2  38531  ovnlecvr2  38539  ovnsubadd2lem  38574  iccpartlt  38873  perfectALTVlem1  38978  perfectALTVlem2  38979  nnsum3primesprm  39020  bgoldbtbndlem1  39035  tgblthelfgott  39043  3exp4mod41  39051  41prothprmlem2  39053  baseltedgf  39241  basvtxval  39260  lfgrn1cycl  39920  nnsgrpmgm  40185  nnsgrpnmnd  40187  basendxnmulrndx  40323  blennn0elnn  40757  blen1  40764
  Copyright terms: Public domain W3C validator