Theorem 1nn 12219

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 ∈ ℕ

Proof of Theorem 1nn

Dummy variable 𝑥 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		1ex 11206	. . . 4 ⊢ 1 ∈ V
2		fr0g 8431	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8430	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7874	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7078	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 691	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2831	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12209	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5688	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2761	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2833	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1542   ∈ wcel 2107  Vcvv 3475  ∅c0 4321   ↦ cmpt 5230  ran crn 5676   ↾ cres 5677   “ cima 5678   Fn wfn 6535  ‘cfv 6540  (class class class)co 7404  ωcom 7850  reccrdg 8404  1c1 11107   + caddc 11109  ℕcn 12208

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5298  ax-nul 5305  ax-pr 5426  ax-un 7720  ax-1cn 11164

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6297  df-ord 6364  df-on 6365  df-lim 6366  df-suc 6367  df-iota 6492  df-fun 6542  df-fn 6543  df-f 6544  df-f1 6545  df-fo 6546  df-f1o 6547  df-fv 6548  df-ov 7407  df-om 7851  df-2nd 7971  df-frecs 8261  df-wrecs 8292  df-recs 8366  df-rdg 8405  df-nn 12209

This theorem is referenced by:  dfnn2  12221  dfnn3  12222  nnind  12226  nn1suc  12230  2nn  12281  nnunb  12464  1nn0  12484  nn0p1nn  12507  elz2  12572  1z  12588  neg1z  12594  nneo  12642  9p1e10  12675  elnn1uz2  12905  zq  12934  rpnnen1lem4  12960  rpnnen1lem5  12961  ser1const  14020  exp1  14029  nnexpcl  14036  expnbnd  14191  fac1  14233  faccl  14239  faclbnd3  14248  faclbnd4lem1  14249  faclbnd4lem2  14250  faclbnd4lem3  14251  faclbnd4lem4  14252  lsw0  14511  ccat2s1p1  14575  cats1un  14667  revs1  14711  cats1fvn  14805  relexpsucnnl  14973  relexpaddg  14996  isercolllem2  15608  isercolllem3  15609  isercoll  15610  sumsnf  15685  climcndslem1  15791  climcndslem2  15792  fprodnncl  15895  prodsn  15902  prodsnf  15904  nnrisefaccl  15959  eftlub  16048  eirrlem  16143  rpnnen2lem5  16157  rpnnen2lem8  16160  rpnnen2lem12  16164  dvdsle  16249  ndvdsp1  16350  gcd1  16465  bezoutr1  16502  1nprm  16612  1idssfct  16613  isprm2lem  16614  qden1elz  16689  phi1  16702  phiprm  16706  pcpre1  16771  pczpre  16776  pcmptcl  16820  pcmpt  16821  infpnlem2  16840  prmreclem1  16845  prmreclem6  16850  mul4sq  16883  vdwmc2  16908  vdwlem8  16917  vdwlem13  16922  vdwnnlem3  16926  prmocl  16963  prmop1  16967  fvprmselelfz  16973  fvprmselgcd1  16974  prmolefac  16975  prmodvdslcmf  16976  prmgapprmo  16991  5prm  17038  7prm  17040  11prm  17044  13prm  17045  17prm  17046  19prm  17047  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  baseid  17143  basendx  17149  basendxnn  17150  basendxnnOLD  17151  1strstr  17155  2strstr  17162  ressval3dOLD  17188  basendxnplusgndxOLD  17224  basendxnmulrndxOLD  17237  rngstr  17239  lmodstr  17266  topgrpstr  17302  otpsstr  17317  ocndx  17322  ocid  17323  basendxnocndx  17324  plendxnocndx  17325  basendxltdsndx  17329  dsndxnplusgndx  17331  dsndxnmulrndx  17332  slotsdnscsi  17333  dsndxntsetndx  17334  slotsdifdsndx  17335  basendxltunifndx  17339  unifndxntsetndx  17341  slotsdifunifndx  17342  slotsbhcdif  17356  slotsbhcdifOLD  17357  slotsdifocndx  17359  oppcbasOLD  17660  rescbasOLD  17773  rescabsOLD  17779  catstr  17905  estrreslem1OLD  18085  ipostr  18478  mulgfval  18946  mulg1  18955  mulg2  18957  oppgbasOLD  19210  symgvalstructOLD  19258  od1  19420  0subgALT  19429  gex1  19452  efgsval2  19594  efgsp1  19598  torsubg  19714  pgpfaclem1  19943  mgpbasOLD  19986  mgpdsOLD  19993  opprbasOLD  20147  rmodislmodOLD  20529  srabaseOLD  20781  sradsOLD  20795  cnfldfunALTOLD  20943  zlmbasOLD  21053  znbas2OLD  21077  thlbasOLD  21234  thlleOLD  21236  opsrbasOLD  21589  pmatcollpw3fi1lem2  22271  hauspwdom  22987  tuslemOLD  23754  imasdsf1olem  23861  setsmsdsOLD  23966  tmslemOLD  23973  tnglemOLD  24132  tngbasOLD  24134  tngdsOLD  24147  cphipval  24742  bcthlem4  24826  bcth3  24830  ovolmge0  24976  ovollb2  24988  ovolctb  24989  ovolunlem1a  24995  ovolunlem1  24996  ovoliunlem1  25001  ovoliun  25004  ovoliun2  25005  ovolicc1  25015  voliunlem1  25049  volsup  25055  ioombl1lem2  25058  ioombl1lem4  25060  uniioombllem1  25080  uniioombllem2  25082  uniioombllem6  25087  itg1climres  25214  itg2seq  25242  itg2monolem1  25250  itg2monolem2  25251  itg2monolem3  25252  itg2mono  25253  itg2i1fseq2  25256  itg2cnlem1  25261  aalioulem5  25831  aaliou2b  25836  aaliou3lem4  25841  aaliou3lem7  25844  log2ub  26434  emcllem6  26485  emcllem7  26486  lgam1  26548  gam1  26549  ftalem7  26563  efnnfsumcl  26587  vmaprm  26601  efvmacl  26604  efchtdvds  26643  vma1  26650  prmorcht  26662  sqff1o  26666  pclogsum  26698  perfectlem1  26712  perfectlem2  26713  bpos1  26766  bposlem5  26771  lgsdir  26815  lgs1  26824  lgsquad2lem2  26868  addsqn2reu  26924  addsqrexnreu  26925  dchrmusumlema  26976  dchrisum0lema  26997  slotsinbpsd  27672  slotslnbpsd  27673  trkgstr  27675  ttgbasOLD  28111  ttgplusgOLD  28113  ttgvscaOLD  28116  eengstr  28218  basendxltedgfndx  28233  baseltedgfOLD  28234  usgrexmplef  28496  lfgrn1cycl  29039  clwwlkn1  29274  ipval2  29938  opsqrlem2  31372  ssnnssfz  31976  nnindf  32003  nn0min  32004  isarchi3  32311  resvbasOLD  32417  rge0scvg  32867  zlmdsOLD  32881  qqh0  32902  qqh1  32903  esumfzf  33005  esumfsup  33006  esumpcvgval  33014  voliune  33165  eulerpartgbij  33309  eulerpartlemgs2  33317  fib2  33339  rrvsum  33391  ballotlem4  33435  ballotlemi1  33439  ballotlemii  33440  ballotlemic  33443  ballotlem1c  33444  hgt750lem  33601  hgt750leme  33608  0nn0m1nnn0  34040  faclimlem1  34651  nn0prpwlem  35145  nn0prpw  35146  poimirlem32  36458  ovoliunnfl  36468  voliunnfl  36470  volsupnfl  36471  incsequz  36554  bfplem1  36628  rrncmslem  36638  hlhilsbaseOLD  40750  60gcd7e1  40808  12lcm5e60  40811  60lcm7e420  40813  lcm1un  40816  lcmineqlem10  40841  3lexlogpow5ineq1  40857  3lexlogpow5ineq2  40858  3lexlogpow5ineq4  40859  aks4d1p1p7  40877  sticksstones9  40908  sticksstones11  40910  nnmulcom  41136  3cubes  41361  jm2.23  41668  rmydioph  41686  rmxdioph  41688  expdiophlem2  41694  expdioph  41695  relexp2  42361  iunrelexpmin1  42392  iunrelexpmin2  42396  dftrcl3  42404  fvtrcllb1d  42406  cotrcltrcl  42409  corcltrcl  42423  cotrclrcl  42426  mnringbasedOLD  42904  prmunb2  43003  sumsnd  43643  nnn0  44023  xrralrecnnge  44035  iooiinicc  44190  iooiinioc  44204  mccl  44249  sumnnodd  44281  wallispilem4  44719  wallispi2lem1  44722  wallispi2lem2  44723  stirlinglem8  44732  stirlinglem11  44735  stirlinglem12  44736  stirlinglem13  44737  fourierdlem31  44789  nnfoctbdjlem  45106  hoicvr  45199  hoicvrrex  45207  hoidmvlelem3  45248  ovnhoilem1  45252  ovnhoilem2  45253  ovnlecvr2  45261  ovnsubadd2lem  45296  iinhoiicclem  45324  vonicclem2  45335  iccpartlt  46027  257prm  46164  fmtnoprmfac2lem1  46169  fmtno4prmfac193  46176  fmtno4nprmfac193  46177  fmtno5nprm  46186  3ndvds4  46198  139prmALT  46199  31prm  46200  127prm  46202  3exp4mod41  46219  41prothprmlem2  46221  perfectALTVlem1  46324  perfectALTVlem2  46325  2exp340mod341  46336  341fppr2  46337  4fppr1  46338  nnsum3primesprm  46393  bgoldbtbndlem1  46408  tgblthelfgott  46418  nnsgrpmgm  46521  nnsgrpnmnd  46523  blennn0elnn  47165  blen1  47172  ackval42  47284