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

Theorem 1nn 10463
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 9502 . . . 4  |-  1  e.  _V
2 fr0g 7019 . . . 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 7018 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6618 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5930 . . . 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 670 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2467 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10453 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4926 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2411 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2469 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1399    e. wcel 1826   _Vcvv 3034   (/)c0 3711    |-> cmpt 4425   ran crn 4914    |` cres 4915   "cima 4916    Fn wfn 5491   ` cfv 5496  (class class class)co 6196   omcom 6599   reccrdg 6993   1c1 9404    + caddc 9406   NNcn 10452
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1626  ax-4 1639  ax-5 1712  ax-6 1755  ax-7 1798  ax-8 1828  ax-9 1830  ax-10 1845  ax-11 1850  ax-12 1862  ax-13 2006  ax-ext 2360  ax-sep 4488  ax-nul 4496  ax-pow 4543  ax-pr 4601  ax-un 6491  ax-1cn 9461
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3or 972  df-3an 973  df-tru 1402  df-ex 1621  df-nf 1625  df-sb 1748  df-eu 2222  df-mo 2223  df-clab 2368  df-cleq 2374  df-clel 2377  df-nfc 2532  df-ne 2579  df-ral 2737  df-rex 2738  df-reu 2739  df-rab 2741  df-v 3036  df-sbc 3253  df-csb 3349  df-dif 3392  df-un 3394  df-in 3396  df-ss 3403  df-pss 3405  df-nul 3712  df-if 3858  df-pw 3929  df-sn 3945  df-pr 3947  df-tp 3949  df-op 3951  df-uni 4164  df-iun 4245  df-br 4368  df-opab 4426  df-mpt 4427  df-tr 4461  df-eprel 4705  df-id 4709  df-po 4714  df-so 4715  df-fr 4752  df-we 4754  df-ord 4795  df-on 4796  df-lim 4797  df-suc 4798  df-xp 4919  df-rel 4920  df-cnv 4921  df-co 4922  df-dm 4923  df-rn 4924  df-res 4925  df-ima 4926  df-iota 5460  df-fun 5498  df-fn 5499  df-f 5500  df-f1 5501  df-fo 5502  df-f1o 5503  df-fv 5504  df-om 6600  df-recs 6960  df-rdg 6994  df-nn 10453
This theorem is referenced by:  dfnn2  10465  dfnn3  10466  nnind  10470  nn1suc  10473  2nn  10610  nnunb  10708  1nn0  10728  nn0p1nn  10752  elz2  10798  1z  10811  neg1z  10817  nneo  10863  elnn1uz2  11077  zq  11107  rpnnen1lem4  11130  rpnnen1lem5  11131  ser1const  12066  exp1  12075  nnexpcl  12082  expnbnd  12197  fac1  12259  faccl  12265  faclbnd3  12272  faclbnd4lem1  12273  faclbnd4lem2  12274  faclbnd4lem3  12275  faclbnd4lem4  12276  lsw0  12494  eqs1  12530  ccat2s1p1  12541  cats1un  12612  revs1  12650  cats1fvn  12734  relexpsucnnl  12867  relexpaddg  12888  isercolllem2  13490  isercolllem3  13491  isercoll  13492  sumsn  13565  climcndslem1  13663  climcndslem2  13664  fprodnncl  13764  prodsn  13769  eftlub  13846  eirrlem  13939  rpnnen2lem5  13954  rpnnen2lem8  13957  rpnnen2  13961  dvdsle  14033  n2dvds1  14037  ndvdsp1  14069  gcd1  14172  1nprm  14224  1idssfct  14225  qden1elz  14292  phi1  14305  phiprm  14309  pcpre1  14368  pczpre  14373  pcmptcl  14412  pcmpt  14413  infpnlem2  14431  prmreclem1  14436  prmreclem6  14441  mul4sq  14474  vdwmc2  14499  vdwlem8  14508  vdwlem13  14513  vdwnnlem3  14517  5prm  14596  7prm  14598  11prm  14602  13prm  14603  17prm  14604  19prm  14605  37prm  14608  43prm  14609  83prm  14610  139prm  14611  163prm  14612  317prm  14613  631prm  14614  1259lem4  14618  1259lem5  14619  1259prm  14620  2503lem3  14623  2503prm  14624  4001lem1  14625  4001lem2  14626  4001lem3  14627  4001lem4  14628  4001prm  14629  baseid  14682  basendx  14686  ressval3d  14698  1strstr  14738  2strstr  14742  rngstr  14753  lmodstr  14770  topgrpstr  14795  otpsstr  14802  ocndx  14807  ocid  14808  ressds  14820  resshom  14825  ressco  14826  slotsbhcdif  14827  oppcbas  15124  rescbas  15235  rescabs  15239  catstr  15363  estrreslem1  15523  ipostr  15900  mulg1  16266  mulg2  16268  oppgbas  16503  od1  16698  gex1  16728  efgsval2  16868  efgsp1  16872  torsubg  16977  pgpfaclem1  17245  mgpbas  17260  mgpds  17264  opprbas  17391  srabase  17937  srads  17945  opsrbas  18256  zlmbas  18648  znbas2  18669  thlbas  18818  thlle  18819  pmatcollpw3fi1lem2  19373  hauspwdom  20087  ressunif  20850  tuslem  20855  imasdsf1olem  20961  setsmsds  21064  tmslem  21070  tnglem  21239  tngbas  21240  tngds  21247  bcthlem4  21851  bcth3  21855  ovolmge0  21973  ovollb2  21985  ovolctb  21986  ovolunlem1a  21992  ovolunlem1  21993  ovoliunlem1  21998  ovoliun  22001  ovoliun2  22002  ovolicc1  22012  voliunlem1  22045  volsup  22051  ioombl1lem2  22054  ioombl1lem4  22056  uniioombllem1  22075  uniioombllem2  22077  uniioombllem6  22082  itg1climres  22206  itg2seq  22234  itg2monolem1  22242  itg2monolem2  22243  itg2monolem3  22244  itg2mono  22245  itg2i1fseq2  22248  itg2cnlem1  22253  aalioulem5  22817  aaliou2b  22822  aaliou3lem4  22827  aaliou3lem7  22830  dcubic1lem  23290  dcubic2  23291  mcubic  23294  log2ub  23396  emcllem6  23447  emcllem7  23448  ftalem7  23469  efnnfsumcl  23493  vmaprm  23508  efvmacl  23511  efchtdvds  23550  vma1  23557  prmorcht  23569  sqff1o  23573  pclogsum  23607  perfectlem1  23621  perfectlem2  23622  bpos1  23675  bposlem5  23680  lgsdir  23722  1lgs  23729  lgs1  23730  lgsquad2lem2  23751  dchrmusumlema  23795  dchrisum0lema  23816  trkgstr  23957  ttgbas  24301  ttgplusg  24302  ttgvsca  24304  eengstr  24404  usgraexmpl  24522  konigsberg  25108  gx1  25381  ipval2  25734  opsqrlem2  27176  ssnnssfz  27750  nnindf  27763  nn0min  27764  isarchi3  27884  resvbas  27976  rge0scvg  28085  zlmds  28098  qqh0  28118  qqh1  28119  esumfzf  28217  esumfsup  28218  esumpcvgval  28226  voliune  28357  eulerpartgbij  28494  eulerpartlemgs2  28502  fib2  28524  rrvsum  28576  ballotlem4  28620  ballotlemi1  28624  ballotlemii  28625  ballotlemic  28628  ballotlem1c  28629  lgam1  28795  gam1  28796  nnrisefaccl  29307  faclimlem1  29334  ovoliunnfl  30221  voliunnfl  30223  volsupnfl  30224  nn0prpwlem  30306  nn0prpw  30307  incsequz  30407  bfplem1  30484  rrncmslem  30494  bezoutr1  31089  jm2.23  31104  rmydioph  31122  rmxdioph  31124  expdiophlem2  31130  expdioph  31131  prmunb2  31359  sumsnd  31568  sumsnf  31736  prodsnf  31753  mccl  31772  sumnnodd  31802  wallispilem4  32016  wallispi2lem1  32019  wallispi2lem2  32020  stirlinglem8  32029  stirlinglem11  32032  stirlinglem12  32033  stirlinglem13  32034  fourierdlem31  32086  perfectALTVlem1  32543  perfectALTVlem2  32544  3exp4mod41  32550  41prothprmlem2  32552  uhgrepe  32696  nnsgrpmgm  32822  nnsgrpnmnd  32824  basendxnmulrndx  32960  blennn0elnn  33398  blen1  33405  hlhilsbase  38082  relexp2  38216  iunrelexpmin1  38225  iunrelexpmin2  38226  dftrcl3  38231  corcltrcl  38249  cotrclrcl  38250  cotrcltrcl  38251
  Copyright terms: Public domain W3C validator