Theorem 1nn 9757

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.

Step	Hyp	Ref	Expression
1		1ex 8833	. . . 4 |- 1 e. _V
2		fr0g 6448	. . . 4 |- ( 1 e. _V -> ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) ` (/) ) = 1 )
3	1, 2	ax-mp 8	. . 3 |- ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) ` (/) ) = 1
4		frfnom 6447	. . . 4 |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) Fn om
5		peano1 4675	. . . 4 |- (/) e. om
6		fnfvelrn 5662	. . . 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 ) )
7	4, 5, 6	mp2an 653	. . 3 |- ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
8	3, 7	eqeltrri 2354	. 2 |- 1 e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
9		df-nn 9747	. . 3 |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om )
10		df-ima 4702	. . 3 |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om ) = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
11	9, 10	eqtri 2303	. 2 |- NN = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
12	8, 11	eleqtrri 2356	1 |- 1 e. NN

Syntax hints:   = wceq 1623   e. wcel 1684   _Vcvv 2788   (/)c0 3455   e. cmpt 4077   omcom 4656   ran crn 4690   |` cres 4691   "cima 4692   Fn wfn 5250   ` cfv 5255  (class class class)co 5858   reccrdg 6422   1c1 8738   + caddc 8740   NNcn 9746

This theorem is referenced by:  dfnn2  9759  dfnn3  9760  nnind  9764  nn1suc  9767  2nn  9877  nnunb  9961  1nn0  9981  nn0p1nn  10003  elz2  10040  1z  10053  nneo  10095  elnn1uz2  10294  zq  10322  rpnnen1lem4  10345  rpnnen1lem5  10346  ser1const  11102  exp1  11109  nnexpcl  11116  expnbnd  11230  fac1  11292  faccl  11298  faclbnd3  11305  faclbnd4lem1  11306  faclbnd4lem2  11307  faclbnd4lem3  11308  faclbnd4lem4  11309  cats1un  11476  revs1  11483  cats1fvn  11508  isercolllem2  12139  isercolllem3  12140  isercoll  12141  sumsn  12213  climcndslem1  12308  climcndslem2  12309  eftlub  12389  eirrlem  12482  xpnnenOLD  12488  rpnnen2lem5  12497  rpnnen2lem8  12500  rpnnen2  12504  nthruz  12530  dvdsle  12574  ndvdsp1  12608  bitsfzolem  12625  bitsfzo  12626  bitsinv1lem  12632  gcd1  12711  1nprm  12763  1idssfct  12764  qden1elz  12828  phi1  12841  phiprm  12845  pcpre1  12895  pczpre  12900  pcmptcl  12939  pcmpt  12940  infpnlem2  12958  prmreclem1  12963  prmreclem6  12968  mul4sq  13001  vdwmc2  13026  vdwlem8  13035  vdwlem13  13040  vdwnnlem3  13044  5prm  13110  7prm  13112  11prm  13116  13prm  13117  17prm  13118  19prm  13119  37prm  13122  43prm  13123  83prm  13124  139prm  13125  163prm  13126  317prm  13127  631prm  13128  1259lem4  13132  1259lem5  13133  1259prm  13134  2503lem3  13137  2503prm  13138  4001lem1  13139  4001lem2  13140  4001lem3  13141  4001lem4  13142  4001prm  13143  baseid  13190  basendx  13193  2strstr  13244  rngstr  13255  lmodstr  13272  topgrpstr  13295  otpsstr  13302  ocndx  13307  ocid  13308  ressds  13318  resshom  13323  ressco  13324  oppcbas  13621  rescbas  13706  rescco  13709  rescabs  13710  catstr  13831  ipostr  14256  mulg1  14574  mulg2  14576  oppgbas  14824  od1  14872  gex1  14902  efgsval2  15042  efgsp1  15046  torsubg  15146  pgpfaclem1  15316  mgpbas  15331  mgpds  15335  opprbas  15411  srabase  15931  srads  15938  opsrbas  16220  zlmbas  16472  znbas2  16493  thlbas  16596  thlle  16597  hauspwdom  17227  imasdsf1olem  17937  setsmsds  18022  tmslem  18028  tnglem  18156  tngbas  18157  tngds  18164  bcthlem4  18749  bcth3  18753  ovolmge0  18836  ovollb2  18848  ovolctb  18849  ovolunlem1a  18855  ovolunlem1  18856  ovoliunlem1  18861  ovoliun  18864  ovoliun2  18865  ovolicc1  18875  voliunlem1  18907  volsup  18913  ioombl1lem2  18916  ioombl1lem4  18918  uniioombllem1  18936  uniioombllem2  18938  uniioombllem6  18943  itg1climres  19069  itg2seq  19097  itg2monolem1  19105  itg2monolem2  19106  itg2monolem3  19107  itg2mono  19108  itg2i1fseq2  19111  itg2cnlem1  19116  aalioulem5  19716  aaliou2b  19721  aaliou3lem4  19726  aaliou3lem7  19729  dcubic1lem  20139  dcubic2  20140  mcubic  20143  log2ub  20245  emcllem6  20294  emcllem7  20295  ftalem7  20316  efnnfsumcl  20340  vmaprm  20355  efvmacl  20358  efchtdvds  20397  vma1  20404  prmorcht  20416  sqff1o  20420  pclogsum  20454  perfectlem1  20468  perfectlem2  20469  bpos1  20522  bposlem5  20527  lgsdir  20569  1lgs  20576  lgs1  20577  lgsquad2lem2  20598  dchrmusumlema  20642  dchrisum0lema  20663  gx1  20929  ipval2  21280  opsqrlem2  22721  ballotlem4  23057  ballotlemi1  23061  ballotlemii  23062  ballotlemic  23065  ballotlem1c  23066  ssnnssfz  23277  rge0scvg  23373  esumpcvgval  23446  konigsberg  23911  cntrset  25602  cnegvex2b  25662  rnegvex2b  25663  1iskle  25989  fnckle  26045  pgapspf2  26053  nn0prpwlem  26238  nn0prpw  26239  incsequz  26458  bfplem1  26546  rrncmslem  26556  bezoutr1  27073  jm2.23  27089  rmydioph  27107  rmxdioph  27109  expdiophlem2  27115  expdioph  27116  sumsnd  27697  wallispilem4  27817  wallispi2lem1  27820  wallispi2lem2  27821  stirlinglem8  27830  stirlinglem11  27833  stirlinglem12  27834  stirlinglem13  27835  usgraexmpl  28133  hlhilsbase  32132

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512  ax-1cn 8795

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 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-pss 3168  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-tp 3648  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-tr 4114  df-eprel 4305  df-id 4309  df-po 4314  df-so 4315  df-fr 4352  df-we 4354  df-ord 4395  df-on 4396  df-lim 4397  df-suc 4398  df-om 4657  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-recs 6388  df-rdg 6423  df-nn 9747