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

Theorem 1nn 10620
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 9637 . . . 4  |-  1  e.  _V
2 fr0g 7161 . . . 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 7160 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6726 . . . 4  |-  (/)  e.  om
6 fnfvelrn 6034 . . . 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 676 . . 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 10610 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4867 . . 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 2516 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1437    e. wcel 1870   _Vcvv 3087   (/)c0 3767    |-> cmpt 4484   ran crn 4855    |` cres 4856   "cima 4857    Fn wfn 5596   ` cfv 5601  (class class class)co 6305   omcom 6706   reccrdg 7135   1c1 9539    + caddc 9541   NNcn 10609
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597  ax-1cn 9596
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-om 6707  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-nn 10610
This theorem is referenced by:  dfnn2  10622  dfnn3  10623  nnind  10627  nn1suc  10630  2nn  10767  nnunb  10865  1nn0  10885  nn0p1nn  10909  elz2  10954  1z  10967  neg1z  10973  nneo  11019  elnn1uz2  11235  zq  11270  rpnnen1lem4  11293  rpnnen1lem5  11294  ser1const  12266  exp1  12275  nnexpcl  12282  expnbnd  12398  fac1  12460  faccl  12466  faclbnd3  12474  faclbnd4lem1  12475  faclbnd4lem2  12476  faclbnd4lem3  12477  faclbnd4lem4  12478  lsw0  12699  eqs1  12735  ccat2s1p1  12746  cats1un  12817  revs1  12855  cats1fvn  12939  relexpsucnnl  13074  relexpaddg  13095  isercolllem2  13707  isercolllem3  13708  isercoll  13709  sumsn  13785  climcndslem1  13885  climcndslem2  13886  fprodnncl  13987  prodsn  13994  prodsnf  13996  nnrisefaccl  14050  eftlub  14141  eirrlem  14234  rpnnen2lem5  14249  rpnnen2lem8  14252  rpnnen2  14256  dvdsle  14328  n2dvds1  14332  ndvdsp1  14365  gcd1  14470  lcmslefacOLD  14557  1nprm  14600  1idssfct  14601  qden1elz  14677  phi1  14690  phiprm  14694  pcpre1  14755  pczpre  14760  pcmptcl  14799  pcmpt  14800  infpnlem2  14818  prmreclem1  14823  prmreclem6  14828  mul4sq  14861  vdwmc2  14892  vdwlem8  14901  vdwlem13  14906  vdwnnlem3  14910  prmocl  14955  prmop1  14959  fvprmselelfz  14965  fvprmselgcd1  14966  prmolefac  14967  prmodvdslcmf  14968  prmormapnnOLD  14977  prmorlefacOLD  14981  prmordvdslcmfOLD  14982  prmordvdslcmsOLDOLD  14984  prmgapprmo  14996  5prm  15043  7prm  15045  11prm  15049  13prm  15050  17prm  15051  19prm  15052  37prm  15055  43prm  15056  83prm  15057  139prm  15058  163prm  15059  317prm  15060  631prm  15061  1259lem4  15068  1259lem5  15069  1259prm  15070  2503lem3  15073  2503prm  15074  4001lem1  15075  4001lem2  15076  4001lem3  15077  4001lem4  15078  4001prm  15079  baseid  15132  basendx  15136  ressval3d  15148  1strstr  15188  2strstr  15192  rngstr  15203  lmodstr  15220  topgrpstr  15245  otpsstr  15252  ocndx  15257  ocid  15258  ressds  15270  resshom  15275  ressco  15276  slotsbhcdif  15277  oppcbas  15574  rescbas  15685  rescabs  15689  catstr  15813  estrreslem1  15973  ipostr  16350  mulg1  16716  mulg2  16718  oppgbas  16953  od1  17148  gex1  17178  efgsval2  17318  efgsp1  17322  torsubg  17427  pgpfaclem1  17649  mgpbas  17664  mgpds  17668  opprbas  17792  srabase  18336  srads  18344  opsrbas  18637  zlmbas  19020  znbas2  19041  thlbas  19190  thlle  19191  pmatcollpw3fi1lem2  19742  hauspwdom  20447  ressunif  21208  tuslem  21213  imasdsf1olem  21319  setsmsds  21422  tmslem  21428  tnglem  21579  tngbas  21580  tngds  21587  bcthlem4  22188  bcth3  22192  ovolmge0  22308  ovollb2  22320  ovolctb  22321  ovolunlem1a  22327  ovolunlem1  22328  ovoliunlem1  22333  ovoliun  22336  ovoliun2  22337  ovolicc1  22347  voliunlem1  22380  volsup  22386  ioombl1lem2  22389  ioombl1lem4  22391  uniioombllem1  22415  uniioombllem2  22417  uniioombllem2OLD  22418  uniioombllem6  22423  itg1climres  22549  itg2seq  22577  itg2monolem1  22585  itg2monolem2  22586  itg2monolem3  22587  itg2mono  22588  itg2i1fseq2  22591  itg2cnlem1  22596  aalioulem5  23157  aaliou2b  23162  aaliou3lem4  23167  aaliou3lem7  23170  dcubic1lem  23634  dcubic2  23635  mcubic  23638  log2ub  23740  emcllem6  23791  emcllem7  23792  lgam1  23854  gam1  23855  ftalem7  23868  efnnfsumcl  23892  vmaprm  23907  efvmacl  23910  efchtdvds  23949  vma1  23956  prmorcht  23968  sqff1o  23972  pclogsum  24006  perfectlem1  24020  perfectlem2  24021  bpos1  24074  bposlem5  24079  lgsdir  24121  1lgs  24128  lgs1  24129  lgsquad2lem2  24150  dchrmusumlema  24194  dchrisum0lema  24215  trkgstr  24355  ttgbas  24753  ttgplusg  24754  ttgvsca  24756  eengstr  24856  usgraexmpl  24974  konigsberg  25560  gx1  25835  ipval2  26188  opsqrlem2  27629  ssnnssfz  28203  nnindf  28220  nn0min  28222  isarchi3  28342  resvbas  28434  rge0scvg  28594  zlmds  28607  qqh0  28627  qqh1  28628  esumfzf  28729  esumfsup  28730  esumpcvgval  28738  voliune  28891  eulerpartgbij  29031  eulerpartlemgs2  29039  fib2  29061  rrvsum  29113  ballotlem4  29157  ballotlemi1  29161  ballotlemii  29162  ballotlemic  29165  ballotlem1c  29166  faclimlem1  30166  nn0prpwlem  30763  nn0prpw  30764  poimirlem32  31675  ovoliunnfl  31685  voliunnfl  31687  volsupnfl  31688  incsequz  31780  bfplem1  31857  rrncmslem  31867  hlhilsbase  35218  bezoutr1  35541  jm2.23  35556  rmydioph  35574  rmxdioph  35576  expdiophlem2  35582  expdioph  35583  relexp2  35907  iunrelexpmin1  35938  iunrelexpmin2  35942  dftrcl3  35950  fvtrcllb1d  35952  cotrcltrcl  35955  corcltrcl  35969  cotrclrcl  35972  prmunb2  36295  sumsnd  36986  sumsnf  37222  mccl  37249  sumnnodd  37281  wallispilem4  37498  wallispi2lem1  37501  wallispi2lem2  37502  stirlinglem8  37511  stirlinglem11  37514  stirlinglem12  37515  stirlinglem13  37516  fourierdlem31  37568  nnfoctbdjlem  37801  iccpartlt  38127  perfectALTVlem1  38232  perfectALTVlem2  38233  nnsum3primesprm  38274  bgoldbtbndlem1  38289  tgblthelfgott  38297  3exp4mod41  38305  41prothprmlem2  38307  uhgrepe  38447  nnsgrpmgm  38573  nnsgrpnmnd  38575  basendxnmulrndx  38711  blennn0elnn  39148  blen1  39155
  Copyright terms: Public domain W3C validator