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

Theorem 1nn 10553
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 9594 . . . 4  |-  1  e.  _V
2 fr0g 7103 . . . 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 7102 . . . 4  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )  Fn  om
5 peano1 6704 . . . 4  |-  (/)  e.  om
6 fnfvelrn 6013 . . . 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 672 . . 3  |-  ( ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om ) `  (/) )  e. 
ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
83, 7eqeltrri 2528 . 2  |-  1  e.  ran  ( rec (
( x  e.  _V  |->  ( x  +  1
) ) ,  1 )  |`  om )
9 df-nn 10543 . . 3  |-  NN  =  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 ) " om )
10 df-ima 5002 . . 3  |-  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 ) " om )  =  ran  ( rec ( ( x  e. 
_V  |->  ( x  + 
1 ) ) ,  1 )  |`  om )
119, 10eqtri 2472 . 2  |-  NN  =  ran  ( rec ( ( x  e.  _V  |->  ( x  +  1 ) ) ,  1 )  |`  om )
128, 11eleqtrri 2530 1  |-  1  e.  NN
Colors of variables: wff setvar class
Syntax hints:    = wceq 1383    e. wcel 1804   _Vcvv 3095   (/)c0 3770    |-> cmpt 4495   ran crn 4990    |` cres 4991   "cima 4992    Fn wfn 5573   ` cfv 5578  (class class class)co 6281   omcom 6685   reccrdg 7077   1c1 9496    + caddc 9498   NNcn 10542
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577  ax-1cn 9553
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-om 6686  df-recs 7044  df-rdg 7078  df-nn 10543
This theorem is referenced by:  dfnn2  10555  dfnn3  10556  nnind  10560  nn1suc  10563  2nn  10699  nnunb  10797  1nn0  10817  nn0p1nn  10841  elz2  10887  1z  10900  neg1z  10906  nneo  10952  elnn1uz2  11167  zq  11197  rpnnen1lem4  11220  rpnnen1lem5  11221  ser1const  12142  exp1  12151  nnexpcl  12158  expnbnd  12274  fac1  12336  faccl  12342  faclbnd3  12349  faclbnd4lem1  12350  faclbnd4lem2  12351  faclbnd4lem3  12352  faclbnd4lem4  12353  lsw0  12565  ccat2s1p1  12611  cats1un  12680  revs1  12718  cats1fvn  12802  isercolllem2  13467  isercolllem3  13468  isercoll  13469  sumsn  13542  climcndslem1  13640  climcndslem2  13641  eftlub  13721  eirrlem  13814  xpnnenOLD  13820  rpnnen2lem5  13829  rpnnen2lem8  13832  rpnnen2  13836  dvdsle  13908  n2dvds1  13912  ndvdsp1  13944  gcd1  14047  1nprm  14099  1idssfct  14100  qden1elz  14167  phi1  14180  phiprm  14184  pcpre1  14243  pczpre  14248  pcmptcl  14287  pcmpt  14288  infpnlem2  14306  prmreclem1  14311  prmreclem6  14316  mul4sq  14349  vdwmc2  14374  vdwlem8  14383  vdwlem13  14388  vdwnnlem3  14392  5prm  14471  7prm  14473  11prm  14477  13prm  14478  17prm  14479  19prm  14480  37prm  14483  43prm  14484  83prm  14485  139prm  14486  163prm  14487  317prm  14488  631prm  14489  1259lem4  14493  1259lem5  14494  1259prm  14495  2503lem3  14498  2503prm  14499  4001lem1  14500  4001lem2  14501  4001lem3  14502  4001lem4  14503  4001prm  14504  baseid  14555  basendx  14559  2strstr  14610  rngstr  14621  lmodstr  14638  topgrpstr  14663  otpsstr  14670  ocndx  14675  ocid  14676  ressds  14688  resshom  14693  ressco  14694  oppcbas  14990  rescbas  15075  rescabs  15079  catstr  15200  ipostr  15657  mulg1  16023  mulg2  16025  oppgbas  16260  od1  16455  gex1  16485  efgsval2  16625  efgsp1  16629  torsubg  16734  pgpfaclem1  17006  mgpbas  17021  mgpds  17025  opprbas  17152  srabase  17698  srads  17706  opsrbas  18017  zlmbas  18428  znbas2  18451  thlbas  18600  thlle  18601  pmatcollpw3fi1lem2  19161  hauspwdom  19875  ressunif  20638  tuslem  20643  imasdsf1olem  20749  setsmsds  20852  tmslem  20858  tnglem  21027  tngbas  21028  tngds  21035  bcthlem4  21639  bcth3  21643  ovolmge0  21761  ovollb2  21773  ovolctb  21774  ovolunlem1a  21780  ovolunlem1  21781  ovoliunlem1  21786  ovoliun  21789  ovoliun2  21790  ovolicc1  21800  voliunlem1  21833  volsup  21839  ioombl1lem2  21842  ioombl1lem4  21844  uniioombllem1  21863  uniioombllem2  21865  uniioombllem6  21870  itg1climres  21994  itg2seq  22022  itg2monolem1  22030  itg2monolem2  22031  itg2monolem3  22032  itg2mono  22033  itg2i1fseq2  22036  itg2cnlem1  22041  aalioulem5  22604  aaliou2b  22609  aaliou3lem4  22614  aaliou3lem7  22617  dcubic1lem  23046  dcubic2  23047  mcubic  23050  log2ub  23152  emcllem6  23202  emcllem7  23203  ftalem7  23224  efnnfsumcl  23248  vmaprm  23263  efvmacl  23266  efchtdvds  23305  vma1  23312  prmorcht  23324  sqff1o  23328  pclogsum  23362  perfectlem1  23376  perfectlem2  23377  bpos1  23430  bposlem5  23435  lgsdir  23477  1lgs  23484  lgs1  23485  lgsquad2lem2  23506  dchrmusumlema  23550  dchrisum0lema  23571  trkgstr  23712  ttgbas  24052  ttgplusg  24053  ttgvsca  24055  eengstr  24155  usgraexmpl  24273  konigsberg  24859  gx1  25136  ipval2  25489  opsqrlem2  26932  ssnnssfz  27469  nnindf  27483  nn0min  27484  isarchi3  27604  resvbas  27695  rge0scvg  27804  zlmds  27818  qqh0  27838  qqh1  27839  esumfzf  27948  esumfsup  27949  esumpcvgval  27957  voliune  28074  eulerpartgbij  28184  eulerpartlemgs2  28192  fib2  28214  rrvsum  28266  ballotlem4  28310  ballotlemi1  28314  ballotlemii  28315  ballotlemic  28318  ballotlem1c  28319  lgam1  28479  gam1  28480  fprodnncl  29062  prodsn  29067  nnrisefaccl  29116  faclimlem1  29143  ovoliunnfl  30031  voliunnfl  30033  volsupnfl  30034  nn0prpwlem  30115  nn0prpw  30116  incsequz  30216  bfplem1  30293  rrncmslem  30303  bezoutr1  30899  jm2.23  30913  rmydioph  30931  rmxdioph  30933  expdiophlem2  30939  expdioph  30940  prmunb2  31167  sumsnd  31355  sumnnodd  31544  wallispilem4  31739  wallispi2lem1  31742  wallispi2lem2  31743  stirlinglem8  31752  stirlinglem11  31755  stirlinglem12  31756  stirlinglem13  31757  fourierdlem31  31809  uhgrepe  32216  nnsgrpmgm  32341  nnsgrpnmnd  32343  ressval3d  32393  slotsbhcdif  32394  1strstr  32395  basendxnmulrndx  32470  estrreslem1  32492  hlhilsbase  37409
  Copyright terms: Public domain W3C validator