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

Theorem 1nn 9847
Description: Peano postulate: 1 is a natural number. (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 8923 . . . 4  |-  1  e.  _V
2 fr0g 6535 . . . 4  |-  ( 1  e.  _V  ->  (
( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1 )
31, 2ax-mp 8 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  =  1
4 frfnom 6534 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 4757 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5745 . . . 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 653 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2429 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 9837 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4784 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2378 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2431 1  |-  1  e.  NN
Colors of variables: wff set class
Syntax hints:    = wceq 1642    e. wcel 1710   _Vcvv 2864   (/)c0 3531    e. cmpt 4158   omcom 4738   ran crn 4772    |` cres 4773   "cima 4774    Fn wfn 5332   ` cfv 5337  (class class class)co 5945   reccrdg 6509   1c1 8828    + caddc 8830   NNcn 9836
This theorem is referenced by:  dfnn2  9849  dfnn3  9850  nnind  9854  nn1suc  9857  2nn  9969  nnunb  10053  1nn0  10073  nn0p1nn  10095  elz2  10132  1z  10145  nneo  10187  elnn1uz2  10386  zq  10414  rpnnen1lem4  10437  rpnnen1lem5  10438  ser1const  11194  exp1  11202  nnexpcl  11209  expnbnd  11323  fac1  11385  faccl  11391  faclbnd3  11398  faclbnd4lem1  11399  faclbnd4lem2  11400  faclbnd4lem3  11401  faclbnd4lem4  11402  cats1un  11572  revs1  11579  cats1fvn  11604  isercolllem2  12235  isercolllem3  12236  isercoll  12237  sumsn  12310  climcndslem1  12405  climcndslem2  12406  eftlub  12486  eirrlem  12579  xpnnenOLD  12585  rpnnen2lem5  12594  rpnnen2lem8  12597  rpnnen2  12601  nthruz  12627  dvdsle  12671  ndvdsp1  12705  bitsfzolem  12722  bitsfzo  12723  bitsinv1lem  12729  gcd1  12808  1nprm  12860  1idssfct  12861  qden1elz  12925  phi1  12938  phiprm  12942  pcpre1  12992  pczpre  12997  pcmptcl  13036  pcmpt  13037  infpnlem2  13055  prmreclem1  13060  prmreclem6  13065  mul4sq  13098  vdwmc2  13123  vdwlem8  13132  vdwlem13  13137  vdwnnlem3  13141  5prm  13207  7prm  13209  11prm  13213  13prm  13214  17prm  13215  19prm  13216  37prm  13219  43prm  13220  83prm  13221  139prm  13222  163prm  13223  317prm  13224  631prm  13225  1259lem4  13229  1259lem5  13230  1259prm  13231  2503lem3  13234  2503prm  13235  4001lem1  13236  4001lem2  13237  4001lem3  13238  4001lem4  13239  4001prm  13240  baseid  13287  basendx  13290  2strstr  13341  rngstr  13352  lmodstr  13369  topgrpstr  13392  otpsstr  13399  ocndx  13404  ocid  13405  ressds  13417  resshom  13422  ressco  13423  oppcbas  13720  rescbas  13805  rescco  13808  rescabs  13809  catstr  13930  ipostr  14355  mulg1  14673  mulg2  14675  oppgbas  14923  od1  14971  gex1  15001  efgsval2  15141  efgsp1  15145  torsubg  15245  pgpfaclem1  15415  mgpbas  15430  mgpds  15434  opprbas  15510  srabase  16030  srads  16037  opsrbas  16319  zlmbas  16578  znbas2  16599  thlbas  16702  thlle  16703  hauspwdom  17333  imasdsf1olem  18039  setsmsds  18124  tmslem  18130  tnglem  18258  tngbas  18259  tngds  18266  bcthlem4  18853  bcth3  18857  ovolmge0  18940  ovollb2  18952  ovolctb  18953  ovolunlem1a  18959  ovolunlem1  18960  ovoliunlem1  18965  ovoliun  18968  ovoliun2  18969  ovolicc1  18979  voliunlem1  19011  volsup  19017  ioombl1lem2  19020  ioombl1lem4  19022  uniioombllem1  19040  uniioombllem2  19042  uniioombllem6  19047  itg1climres  19173  itg2seq  19201  itg2monolem1  19209  itg2monolem2  19210  itg2monolem3  19211  itg2mono  19212  itg2i1fseq2  19215  itg2cnlem1  19220  aalioulem5  19820  aaliou2b  19825  aaliou3lem4  19830  aaliou3lem7  19833  dcubic1lem  20250  dcubic2  20251  mcubic  20254  log2ub  20356  emcllem6  20406  emcllem7  20407  ftalem7  20428  efnnfsumcl  20452  vmaprm  20467  efvmacl  20470  efchtdvds  20509  vma1  20516  prmorcht  20528  sqff1o  20532  pclogsum  20566  perfectlem1  20580  perfectlem2  20581  bpos1  20634  bposlem5  20639  lgsdir  20681  1lgs  20688  lgs1  20689  lgsquad2lem2  20710  dchrmusumlema  20754  dchrisum0lema  20775  gx1  21041  ipval2  21394  opsqrlem2  22835  ssnnssfz  23350  rge0scvg  23491  ressunif  23561  tuslem  23565  zlmds  23623  qqh0  23641  qqh1  23642  esumfzf  23725  esumfsup  23726  esumpcvgval  23734  voliune  23849  rrvsum  23961  ballotlem4  24005  ballotlemi1  24009  ballotlemii  24010  ballotlemic  24013  ballotlem1c  24014  lgam1  24097  gam1  24098  konigsberg  24315  fprodnncl  24582  prodsn  24587  nnrisefaccl  24625  gamma1  24645  faclimlem1  24654  ovoliunnfl  25488  voliunnfl  25490  volsupnfl  25491  nn0prpwlem  25562  nn0prpw  25563  incsequz  25782  bfplem1  25869  rrncmslem  25879  bezoutr1  26396  jm2.23  26412  rmydioph  26430  rmxdioph  26432  expdiophlem2  26438  expdioph  26439  sumsnd  27020  wallispilem4  27140  wallispi2lem1  27143  wallispi2lem2  27144  stirlinglem8  27153  stirlinglem11  27156  stirlinglem12  27157  stirlinglem13  27158  usgraexmpl  27574  hlhilsbase  32201
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339  ax-sep 4222  ax-nul 4230  ax-pow 4269  ax-pr 4295  ax-un 4594  ax-1cn 8885
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2213  df-mo 2214  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ne 2523  df-ral 2624  df-rex 2625  df-reu 2626  df-rab 2628  df-v 2866  df-sbc 3068  df-csb 3158  df-dif 3231  df-un 3233  df-in 3235  df-ss 3242  df-pss 3244  df-nul 3532  df-if 3642  df-pw 3703  df-sn 3722  df-pr 3723  df-tp 3724  df-op 3725  df-uni 3909  df-iun 3988  df-br 4105  df-opab 4159  df-mpt 4160  df-tr 4195  df-eprel 4387  df-id 4391  df-po 4396  df-so 4397  df-fr 4434  df-we 4436  df-ord 4477  df-on 4478  df-lim 4479  df-suc 4480  df-om 4739  df-xp 4777  df-rel 4778  df-cnv 4779  df-co 4780  df-dm 4781  df-rn 4782  df-res 4783  df-ima 4784  df-iota 5301  df-fun 5339  df-fn 5340  df-f 5341  df-f1 5342  df-fo 5343  df-f1o 5344  df-fv 5345  df-recs 6475  df-rdg 6510  df-nn 9837
  Copyright terms: Public domain W3C validator