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

Theorem 1nn 10320
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 9368 . . . 4  |-  1  e.  _V
2 fr0g 6877 . . . 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 6876 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6484 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5828 . . . 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 665 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2504 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10310 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4840 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2453 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2506 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1362    e. wcel 1755   _Vcvv 2962   (/)c0 3625    e. cmpt 4338   ran crn 4828    |` cres 4829   "cima 4830    Fn wfn 5401   ` cfv 5406  (class class class)co 6080   omcom 6465   reccrdg 6851   1c1 9270    + caddc 9272   NNcn 10309
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-8 1757  ax-9 1759  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414  ax-sep 4401  ax-nul 4409  ax-pow 4458  ax-pr 4519  ax-un 6361  ax-1cn 9327
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 959  df-3an 960  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-eu 2258  df-mo 2259  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-ne 2598  df-ral 2710  df-rex 2711  df-reu 2712  df-rab 2714  df-v 2964  df-sbc 3176  df-csb 3277  df-dif 3319  df-un 3321  df-in 3323  df-ss 3330  df-pss 3332  df-nul 3626  df-if 3780  df-pw 3850  df-sn 3866  df-pr 3868  df-tp 3870  df-op 3872  df-uni 4080  df-iun 4161  df-br 4281  df-opab 4339  df-mpt 4340  df-tr 4374  df-eprel 4619  df-id 4623  df-po 4628  df-so 4629  df-fr 4666  df-we 4668  df-ord 4709  df-on 4710  df-lim 4711  df-suc 4712  df-xp 4833  df-rel 4834  df-cnv 4835  df-co 4836  df-dm 4837  df-rn 4838  df-res 4839  df-ima 4840  df-iota 5369  df-fun 5408  df-fn 5409  df-f 5410  df-f1 5411  df-fo 5412  df-f1o 5413  df-fv 5414  df-om 6466  df-recs 6818  df-rdg 6852  df-nn 10310
This theorem is referenced by:  dfnn2  10322  dfnn3  10323  nnind  10327  nn1suc  10330  2nn  10466  nnunb  10562  1nn0  10582  nn0p1nn  10606  elz2  10650  1z  10663  neg1z  10668  nneo  10712  elnn1uz2  10918  zq  10946  rpnnen1lem4  10969  rpnnen1lem5  10970  ser1const  11845  exp1  11854  nnexpcl  11861  expnbnd  11976  fac1  12038  faccl  12044  faclbnd3  12051  faclbnd4lem1  12052  faclbnd4lem2  12053  faclbnd4lem3  12054  faclbnd4lem4  12055  lsw0  12250  cats1un  12353  revs1  12388  cats1fvn  12468  isercolllem2  13126  isercolllem3  13127  isercoll  13128  sumsn  13200  climcndslem1  13294  climcndslem2  13295  eftlub  13375  eirrlem  13468  xpnnenOLD  13474  rpnnen2lem5  13483  rpnnen2lem8  13486  rpnnen2  13490  dvdsle  13560  n2dvds1  13564  ndvdsp1  13595  gcd1  13698  1nprm  13750  1idssfct  13751  qden1elz  13817  phi1  13830  phiprm  13834  pcpre1  13891  pczpre  13896  pcmptcl  13935  pcmpt  13936  infpnlem2  13954  prmreclem1  13959  prmreclem6  13964  mul4sq  13997  vdwmc2  14022  vdwlem8  14031  vdwlem13  14036  vdwnnlem3  14040  5prm  14118  7prm  14120  11prm  14124  13prm  14125  17prm  14126  19prm  14127  37prm  14130  43prm  14131  83prm  14132  139prm  14133  163prm  14134  317prm  14135  631prm  14136  1259lem4  14140  1259lem5  14141  1259prm  14142  2503lem3  14145  2503prm  14146  4001lem1  14147  4001lem2  14148  4001lem3  14149  4001lem4  14150  4001prm  14151  baseid  14202  basendx  14205  2strstr  14256  rngstr  14267  lmodstr  14284  topgrpstr  14309  otpsstr  14316  ocndx  14321  ocid  14322  ressds  14334  resshom  14339  ressco  14340  oppcbas  14639  rescbas  14724  rescabs  14728  catstr  14849  ipostr  15305  mulg1  15613  mulg2  15615  oppgbas  15845  od1  16039  gex1  16069  efgsval2  16209  efgsp1  16213  torsubg  16315  pgpfaclem1  16555  mgpbas  16570  mgpds  16574  opprbas  16654  srabase  17180  srads  17188  opsrbas  17491  zlmbas  17790  znbas2  17813  thlbas  17962  thlle  17963  m2detleiblem1  18271  hauspwdom  18946  ressunif  19678  tuslem  19683  imasdsf1olem  19789  setsmsds  19892  tmslem  19898  tnglem  20067  tngbas  20068  tngds  20075  bcthlem4  20679  bcth3  20683  ovolmge0  20801  ovollb2  20813  ovolctb  20814  ovolunlem1a  20820  ovolunlem1  20821  ovoliunlem1  20826  ovoliun  20829  ovoliun2  20830  ovolicc1  20840  voliunlem1  20872  volsup  20878  ioombl1lem2  20881  ioombl1lem4  20883  uniioombllem1  20902  uniioombllem2  20904  uniioombllem6  20909  itg1climres  21033  itg2seq  21061  itg2monolem1  21069  itg2monolem2  21070  itg2monolem3  21071  itg2mono  21072  itg2i1fseq2  21075  itg2cnlem1  21080  aalioulem5  21686  aaliou2b  21691  aaliou3lem4  21696  aaliou3lem7  21699  dcubic1lem  22122  dcubic2  22123  mcubic  22126  log2ub  22228  emcllem6  22278  emcllem7  22279  ftalem7  22300  efnnfsumcl  22324  vmaprm  22339  efvmacl  22342  efchtdvds  22381  vma1  22388  prmorcht  22400  sqff1o  22404  pclogsum  22438  perfectlem1  22452  perfectlem2  22453  bpos1  22506  bposlem5  22511  lgsdir  22553  1lgs  22560  lgs1  22561  lgsquad2lem2  22582  dchrmusumlema  22626  dchrisum0lema  22647  trkgstr  22789  ttgbas  22945  ttgplusg  22946  ttgvsca  22948  eengstr  23048  usgraexmpl  23141  konigsberg  23430  gx1  23571  ipval2  23924  opsqrlem2  25367  ssnnssfz  25898  nnindf  25911  nn0min  25912  isarchi3  26027  resvbas  26153  rge0scvg  26232  zlmds  26246  qqh0  26266  qqh1  26267  esumfzf  26371  esumfsup  26372  esumpcvgval  26380  voliune  26498  eulerpartgbij  26602  eulerpartlemgs2  26610  fib2  26632  rrvsum  26684  ballotlem4  26728  ballotlemi1  26732  ballotlemii  26733  ballotlemic  26736  ballotlem1c  26737  signswbase  26802  signswplusg  26803  lgam1  26897  gam1  26898  fprodnncl  27314  prodsn  27319  nnrisefaccl  27368  faclimlem1  27395  ovoliunnfl  28274  voliunnfl  28276  volsupnfl  28277  nn0prpwlem  28358  nn0prpw  28359  incsequz  28485  bfplem1  28562  rrncmslem  28572  bezoutr1  29171  jm2.23  29187  rmydioph  29205  rmxdioph  29207  expdiophlem2  29213  expdioph  29214  sumsnd  29590  wallispilem4  29706  wallispi2lem1  29709  wallispi2lem2  29710  stirlinglem8  29719  stirlinglem11  29722  stirlinglem12  29723  stirlinglem13  29724  ccat2s1p1  30108  hlhilsbase  35157
  Copyright terms: Public domain W3C validator