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

Theorem 1nn 9773
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 8849 . . . 4  |-  1  e.  _V
2 fr0g 6464 . . . 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 6463 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 4691 . . . 4  |-  (/)  e.  om
6 fnfvelrn 5678 . . . 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 2367 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 9763 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 4718 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2316 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2369 1  |-  1  e.  NN
Colors of variables: wff set class
Syntax hints:    = wceq 1632    e. wcel 1696   _Vcvv 2801   (/)c0 3468    e. cmpt 4093   omcom 4672   ran crn 4706    |` cres 4707   "cima 4708    Fn wfn 5266   ` cfv 5271  (class class class)co 5874   reccrdg 6438   1c1 8754    + caddc 8756   NNcn 9762
This theorem is referenced by:  dfnn2  9775  dfnn3  9776  nnind  9780  nn1suc  9783  2nn  9893  nnunb  9977  1nn0  9997  nn0p1nn  10019  elz2  10056  1z  10069  nneo  10111  elnn1uz2  10310  zq  10338  rpnnen1lem4  10361  rpnnen1lem5  10362  ser1const  11118  exp1  11125  nnexpcl  11132  expnbnd  11246  fac1  11308  faccl  11314  faclbnd3  11321  faclbnd4lem1  11322  faclbnd4lem2  11323  faclbnd4lem3  11324  faclbnd4lem4  11325  cats1un  11492  revs1  11499  cats1fvn  11524  isercolllem2  12155  isercolllem3  12156  isercoll  12157  sumsn  12229  climcndslem1  12324  climcndslem2  12325  eftlub  12405  eirrlem  12498  xpnnenOLD  12504  rpnnen2lem5  12513  rpnnen2lem8  12516  rpnnen2  12520  nthruz  12546  dvdsle  12590  ndvdsp1  12624  bitsfzolem  12641  bitsfzo  12642  bitsinv1lem  12648  gcd1  12727  1nprm  12779  1idssfct  12780  qden1elz  12844  phi1  12857  phiprm  12861  pcpre1  12911  pczpre  12916  pcmptcl  12955  pcmpt  12956  infpnlem2  12974  prmreclem1  12979  prmreclem6  12984  mul4sq  13017  vdwmc2  13042  vdwlem8  13051  vdwlem13  13056  vdwnnlem3  13060  5prm  13126  7prm  13128  11prm  13132  13prm  13133  17prm  13134  19prm  13135  37prm  13138  43prm  13139  83prm  13140  139prm  13141  163prm  13142  317prm  13143  631prm  13144  1259lem4  13148  1259lem5  13149  1259prm  13150  2503lem3  13153  2503prm  13154  4001lem1  13155  4001lem2  13156  4001lem3  13157  4001lem4  13158  4001prm  13159  baseid  13206  basendx  13209  2strstr  13260  rngstr  13271  lmodstr  13288  topgrpstr  13311  otpsstr  13318  ocndx  13323  ocid  13324  ressds  13334  resshom  13339  ressco  13340  oppcbas  13637  rescbas  13722  rescco  13725  rescabs  13726  catstr  13847  ipostr  14272  mulg1  14590  mulg2  14592  oppgbas  14840  od1  14888  gex1  14918  efgsval2  15058  efgsp1  15062  torsubg  15162  pgpfaclem1  15332  mgpbas  15347  mgpds  15351  opprbas  15427  srabase  15947  srads  15954  opsrbas  16236  zlmbas  16488  znbas2  16509  thlbas  16612  thlle  16613  hauspwdom  17243  imasdsf1olem  17953  setsmsds  18038  tmslem  18044  tnglem  18172  tngbas  18173  tngds  18180  bcthlem4  18765  bcth3  18769  ovolmge0  18852  ovollb2  18864  ovolctb  18865  ovolunlem1a  18871  ovolunlem1  18872  ovoliunlem1  18877  ovoliun  18880  ovoliun2  18881  ovolicc1  18891  voliunlem1  18923  volsup  18929  ioombl1lem2  18932  ioombl1lem4  18934  uniioombllem1  18952  uniioombllem2  18954  uniioombllem6  18959  itg1climres  19085  itg2seq  19113  itg2monolem1  19121  itg2monolem2  19122  itg2monolem3  19123  itg2mono  19124  itg2i1fseq2  19127  itg2cnlem1  19132  aalioulem5  19732  aaliou2b  19737  aaliou3lem4  19742  aaliou3lem7  19745  dcubic1lem  20155  dcubic2  20156  mcubic  20159  log2ub  20261  emcllem6  20310  emcllem7  20311  ftalem7  20332  efnnfsumcl  20356  vmaprm  20371  efvmacl  20374  efchtdvds  20413  vma1  20420  prmorcht  20432  sqff1o  20436  pclogsum  20470  perfectlem1  20484  perfectlem2  20485  bpos1  20538  bposlem5  20543  lgsdir  20585  1lgs  20592  lgs1  20593  lgsquad2lem2  20614  dchrmusumlema  20658  dchrisum0lema  20679  gx1  20945  ipval2  21296  opsqrlem2  22737  ballotlem4  23073  ballotlemi1  23077  ballotlemii  23078  ballotlemic  23081  ballotlem1c  23082  ssnnssfz  23292  rge0scvg  23388  esumpcvgval  23461  konigsberg  23926  faclimlem3  24119  faclimlem8  24124  faclim  24126  ovoliunnfl  25001  cntrset  25705  cnegvex2b  25765  rnegvex2b  25766  1iskle  26092  fnckle  26148  pgapspf2  26156  nn0prpwlem  26341  nn0prpw  26342  incsequz  26561  bfplem1  26649  rrncmslem  26659  bezoutr1  27176  jm2.23  27192  rmydioph  27210  rmxdioph  27212  expdiophlem2  27218  expdioph  27219  sumsnd  27800  wallispilem4  27920  wallispi2lem1  27923  wallispi2lem2  27924  stirlinglem8  27933  stirlinglem11  27936  stirlinglem12  27937  stirlinglem13  27938  usgraexmpl  28267  hlhilsbase  32754
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528  ax-1cn 8811
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-om 4673  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-recs 6404  df-rdg 6439  df-nn 9763
  Copyright terms: Public domain W3C validator