Theorem 1nn 9975

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 9050	. . . 4 |- 1 e. _V
2		fr0g 6660	. . . 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 6659	. . . 4 |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) Fn om
5		peano1 4831	. . . 4 |- (/) e. om
6		fnfvelrn 5834	. . . 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 654	. . 3 |- ( ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om ) ` (/) ) e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
8	3, 7	eqeltrri 2483	. 2 |- 1 e. ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
9		df-nn 9965	. . 3 |- NN = ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om )
10		df-ima 4858	. . 3 |- ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) " om ) = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
11	9, 10	eqtri 2432	. 2 |- NN = ran ( rec ( ( x e. _V |-> ( x + 1 ) ) , 1 ) |` om )
12	8, 11	eleqtrri 2485	1 |- 1 e. NN

Syntax hints:   = wceq 1649   e. wcel 1721   _Vcvv 2924   (/)c0 3596   e. cmpt 4234   omcom 4812   ran crn 4846   |` cres 4847   "cima 4848   Fn wfn 5416   ` cfv 5421  (class class class)co 6048   reccrdg 6634   1c1 8955   + caddc 8957   NNcn 9964

This theorem is referenced by:  dfnn2  9977  dfnn3  9978  nnind  9982  nn1suc  9985  2nn  10097  nnunb  10181  1nn0  10201  nn0p1nn  10223  elz2  10262  1z  10275  nneo  10317  elnn1uz2  10516  zq  10544  rpnnen1lem4  10567  rpnnen1lem5  10568  ser1const  11342  exp1  11350  nnexpcl  11357  expnbnd  11471  fac1  11533  faccl  11539  faclbnd3  11546  faclbnd4lem1  11547  faclbnd4lem2  11548  faclbnd4lem3  11549  faclbnd4lem4  11550  cats1un  11753  revs1  11760  cats1fvn  11785  isercolllem2  12422  isercolllem3  12423  isercoll  12424  sumsn  12497  climcndslem1  12592  climcndslem2  12593  eftlub  12673  eirrlem  12766  xpnnenOLD  12772  rpnnen2lem5  12781  rpnnen2lem8  12784  rpnnen2  12788  nthruz  12814  dvdsle  12858  ndvdsp1  12892  bitsfzolem  12909  bitsfzo  12910  bitsinv1lem  12916  gcd1  12995  1nprm  13047  1idssfct  13048  qden1elz  13112  phi1  13125  phiprm  13129  pcpre1  13179  pczpre  13184  pcmptcl  13223  pcmpt  13224  infpnlem2  13242  prmreclem1  13247  prmreclem6  13252  mul4sq  13285  vdwmc2  13310  vdwlem8  13319  vdwlem13  13324  vdwnnlem3  13328  5prm  13394  7prm  13396  11prm  13400  13prm  13401  17prm  13402  19prm  13403  37prm  13406  43prm  13407  83prm  13408  139prm  13409  163prm  13410  317prm  13411  631prm  13412  1259lem4  13416  1259lem5  13417  1259prm  13418  2503lem3  13421  2503prm  13422  4001lem1  13423  4001lem2  13424  4001lem3  13425  4001lem4  13426  4001prm  13427  baseid  13474  basendx  13477  2strstr  13528  rngstr  13539  lmodstr  13556  topgrpstr  13579  otpsstr  13586  ocndx  13591  ocid  13592  ressds  13604  resshom  13609  ressco  13610  oppcbas  13907  rescbas  13992  rescabs  13996  catstr  14117  ipostr  14542  mulg1  14860  mulg2  14862  oppgbas  15110  od1  15158  gex1  15188  efgsval2  15328  efgsp1  15332  torsubg  15432  pgpfaclem1  15602  mgpbas  15617  mgpds  15621  opprbas  15697  srabase  16213  srads  16220  opsrbas  16502  zlmbas  16762  znbas2  16783  thlbas  16886  thlle  16887  hauspwdom  17525  ressunif  18253  tuslem  18258  imasdsf1olem  18364  setsmsds  18467  tmslem  18473  tnglem  18642  tngbas  18643  tngds  18650  bcthlem4  19241  bcth3  19245  ovolmge0  19334  ovollb2  19346  ovolctb  19347  ovolunlem1a  19353  ovolunlem1  19354  ovoliunlem1  19359  ovoliun  19362  ovoliun2  19363  ovolicc1  19373  voliunlem1  19405  volsup  19411  ioombl1lem2  19414  ioombl1lem4  19416  uniioombllem1  19434  uniioombllem2  19436  uniioombllem6  19441  itg1climres  19567  itg2seq  19595  itg2monolem1  19603  itg2monolem2  19604  itg2monolem3  19605  itg2mono  19606  itg2i1fseq2  19609  itg2cnlem1  19614  aalioulem5  20214  aaliou2b  20219  aaliou3lem4  20224  aaliou3lem7  20227  dcubic1lem  20644  dcubic2  20645  mcubic  20648  log2ub  20750  emcllem6  20800  emcllem7  20801  ftalem7  20822  efnnfsumcl  20846  vmaprm  20861  efvmacl  20864  efchtdvds  20903  vma1  20910  prmorcht  20922  sqff1o  20926  pclogsum  20960  perfectlem1  20974  perfectlem2  20975  bpos1  21028  bposlem5  21033  lgsdir  21075  1lgs  21082  lgs1  21083  lgsquad2lem2  21104  dchrmusumlema  21148  dchrisum0lema  21169  usgraexmpl  21381  konigsberg  21670  gx1  21811  ipval2  22164  opsqrlem2  23605  ssnnssfz  24109  rge0scvg  24296  zlmds  24309  qqh0  24329  qqh1  24330  esumfzf  24420  esumfsup  24421  esumpcvgval  24429  voliune  24546  rrvsum  24673  ballotlem4  24717  ballotlemi1  24721  ballotlemii  24722  ballotlemic  24725  ballotlem1c  24726  lgam1  24809  gam1  24810  fprodnncl  25242  prodsn  25247  nnrisefaccl  25295  faclimlem1  25318  ovoliunnfl  26155  voliunnfl  26157  volsupnfl  26158  nn0prpwlem  26223  nn0prpw  26224  incsequz  26350  bfplem1  26429  rrncmslem  26439  bezoutr1  26949  jm2.23  26965  rmydioph  26983  rmxdioph  26985  expdiophlem2  26991  expdioph  26992  sumsnd  27572  wallispilem4  27692  wallispi2lem1  27695  wallispi2lem2  27696  stirlinglem8  27705  stirlinglem11  27708  stirlinglem12  27709  stirlinglem13  27710  hlhilsbase  32437

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393  ax-sep 4298  ax-nul 4306  ax-pow 4345  ax-pr 4371  ax-un 4668  ax-1cn 9012

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2266  df-mo 2267  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-ne 2577  df-ral 2679  df-rex 2680  df-reu 2681  df-rab 2683  df-v 2926  df-sbc 3130  df-csb 3220  df-dif 3291  df-un 3293  df-in 3295  df-ss 3302  df-pss 3304  df-nul 3597  df-if 3708  df-pw 3769  df-sn 3788  df-pr 3789  df-tp 3790  df-op 3791  df-uni 3984  df-iun 4063  df-br 4181  df-opab 4235  df-mpt 4236  df-tr 4271  df-eprel 4462  df-id 4466  df-po 4471  df-so 4472  df-fr 4509  df-we 4511  df-ord 4552  df-on 4553  df-lim 4554  df-suc 4555  df-om 4813  df-xp 4851  df-rel 4852  df-cnv 4853  df-co 4854  df-dm 4855  df-rn 4856  df-res 4857  df-ima 4858  df-iota 5385  df-fun 5423  df-fn 5424  df-f 5425  df-f1 5426  df-fo 5427  df-f1o 5428  df-fv 5429  df-recs 6600  df-rdg 6635  df-nn 9965