Theorem 1nn 12168

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 11140	. . . 4 ⊢ 1 ∈ V
2		fr0g 8377	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8376	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7841	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7034	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 693	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2834	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12158	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5645	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2760	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2836	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1542   ∈ wcel 2114  Vcvv 3442  ∅c0 4287   ↦ cmpt 5181  ran crn 5633   ↾ cres 5634   “ cima 5635   Fn wfn 6495  ‘cfv 6500  (class class class)co 7368  ωcom 7818  reccrdg 8350  1c1 11039   + caddc 11041  ℕcn 12157

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2709  ax-sep 5243  ax-nul 5253  ax-pr 5379  ax-un 7690  ax-1cn 11096

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-nf 1786  df-sb 2069  df-mo 2540  df-eu 2570  df-clab 2716  df-cleq 2729  df-clel 2812  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3063  df-reu 3353  df-rab 3402  df-v 3444  df-sbc 3743  df-csb 3852  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-pss 3923  df-nul 4288  df-if 4482  df-pw 4558  df-sn 4583  df-pr 4585  df-op 4589  df-uni 4866  df-iun 4950  df-br 5101  df-opab 5163  df-mpt 5182  df-tr 5208  df-id 5527  df-eprel 5532  df-po 5540  df-so 5541  df-fr 5585  df-we 5587  df-xp 5638  df-rel 5639  df-cnv 5640  df-co 5641  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645  df-pred 6267  df-ord 6328  df-on 6329  df-lim 6330  df-suc 6331  df-iota 6456  df-fun 6502  df-fn 6503  df-f 6504  df-f1 6505  df-fo 6506  df-f1o 6507  df-fv 6508  df-ov 7371  df-om 7819  df-2nd 7944  df-frecs 8233  df-wrecs 8264  df-recs 8313  df-rdg 8351  df-nn 12158

This theorem is referenced by:  dfnn2  12170  dfnn3  12171  nnind  12175  nn1suc  12179  2nn  12230  nnunb  12409  1nn0  12429  nn0p1nn  12452  elz2  12518  1z  12533  neg1z  12539  nneo  12588  9p1e10  12621  elnn1uz2  12850  zq  12879  rpnnen1lem4  12905  rpnnen1lem5  12906  1elfzo1  13642  ser1const  13993  exp1  14002  nnexpcl  14009  expnbnd  14167  fac1  14212  faccl  14218  faclbnd3  14227  faclbnd4lem1  14228  faclbnd4lem2  14229  faclbnd4lem3  14230  faclbnd4lem4  14231  lsw0  14500  ccat2s1p1  14565  cats1un  14656  revs1  14700  cats1fvn  14793  relexpsucnnl  14965  relexpaddg  14988  isercolllem2  15601  isercolllem3  15602  isercoll  15603  sumsnf  15678  climcndslem1  15784  climcndslem2  15785  fprodnncl  15890  prodsn  15897  prodsnf  15899  nnrisefaccl  15954  eftlub  16046  eirrlem  16141  rpnnen2lem5  16155  rpnnen2lem8  16158  rpnnen2lem12  16162  dvdsle  16249  ndvdsp1  16350  5ndvds6  16353  gcd1  16467  bezoutr1  16508  1nprm  16618  1idssfct  16619  isprm2lem  16620  qden1elz  16696  phi1  16712  phiprm  16716  pcpre1  16782  pczpre  16787  pcmptcl  16831  pcmpt  16832  infpnlem2  16851  prmreclem1  16856  prmreclem6  16861  mul4sq  16894  vdwmc2  16919  vdwlem8  16928  vdwlem13  16933  vdwnnlem3  16937  prmocl  16974  prmop1  16978  fvprmselelfz  16984  fvprmselgcd1  16985  prmolefac  16986  prmodvdslcmf  16987  prmgapprmo  17002  5prm  17048  7prm  17050  11prm  17054  13prm  17055  17prm  17056  19prm  17057  37prm  17060  43prm  17061  83prm  17062  139prm  17063  163prm  17064  317prm  17065  631prm  17066  1259lem4  17073  1259lem5  17074  1259prm  17075  2503lem3  17078  2503prm  17079  4001lem1  17080  4001lem2  17081  4001lem3  17082  4001lem4  17083  4001prm  17084  baseid  17151  basendx  17157  basendxnn  17158  rngstr  17230  lmodstr  17257  topgrpstr  17293  otpsstr  17308  ocndx  17313  ocid  17314  basendxnocndx  17315  plendxnocndx  17316  basendxltdsndx  17320  dsndxnplusgndx  17322  dsndxnmulrndx  17323  slotsdnscsi  17324  dsndxntsetndx  17325  slotsdifdsndx  17326  basendxltunifndx  17330  unifndxntsetndx  17332  slotsdifunifndx  17333  slotsbhcdif  17347  slotsdifocndx  17349  catstr  17896  ipostr  18464  mulgfval  19011  mulg1  19023  mulg2  19025  od1  19500  0subgALT  19509  gex1  19532  efgsval2  19674  efgsp1  19678  torsubg  19795  pgpfaclem1  20024  pmatcollpw3fi1lem2  22743  hauspwdom  23457  imasdsf1olem  24329  cphipval  25211  bcthlem4  25295  bcth3  25299  ovolmge0  25446  ovollb2  25458  ovolctb  25459  ovolunlem1a  25465  ovolunlem1  25466  ovoliunlem1  25471  ovoliun  25474  ovoliun2  25475  ovolicc1  25485  voliunlem1  25519  volsup  25525  ioombl1lem2  25528  ioombl1lem4  25530  uniioombllem1  25550  uniioombllem2  25552  uniioombllem6  25557  itg1climres  25683  itg2seq  25711  itg2monolem1  25719  itg2monolem2  25720  itg2monolem3  25721  itg2mono  25722  itg2i1fseq2  25725  itg2cnlem1  25730  aalioulem5  26312  aaliou2b  26317  aaliou3lem4  26322  aaliou3lem7  26325  log2ub  26927  emcllem6  26979  emcllem7  26980  lgam1  27042  gam1  27043  ftalem7  27057  efnnfsumcl  27081  vmaprm  27095  efvmacl  27098  efchtdvds  27137  vma1  27144  prmorcht  27156  sqff1o  27160  pclogsum  27194  perfectlem1  27208  perfectlem2  27209  bpos1  27262  bposlem5  27267  lgsdir  27311  lgs1  27320  lgsquad2lem2  27364  addsqn2reu  27420  addsqrexnreu  27421  dchrmusumlema  27472  dchrisum0lema  27493  slotsinbpsd  28525  slotslnbpsd  28526  trkgstr  28528  eengstr  29065  basendxltedgfndx  29079  usgrexmplef  29344  lfgrn1cycl  29890  clwwlkn1  30128  ipval2  30794  opsqrlem2  32228  ssnnssfz  32877  znumd  32903  zdend  32904  nnindf  32910  nn0min  32911  isarchi3  33280  eufndx  33383  eufid  33384  constrext2chnlem  33927  iconstr  33943  rge0scvg  34126  qqh0  34161  qqh1  34162  esumfzf  34246  esumfsup  34247  esumpcvgval  34255  voliune  34406  eulerpartgbij  34549  eulerpartlemgs2  34557  fib2  34579  rrvsum  34631  ballotlem4  34676  ballotlemi1  34680  ballotlemii  34681  ballotlemic  34684  ballotlem1c  34685  hgt750lem  34828  hgt750leme  34835  0nn0m1nnn0  35326  faclimlem1  35956  nn0prpwlem  36535  nn0prpw  36536  poimirlem32  37900  ovoliunnfl  37910  voliunnfl  37912  volsupnfl  37913  incsequz  37996  bfplem1  38070  rrncmslem  38080  60gcd7e1  42372  12lcm5e60  42375  60lcm7e420  42377  lcm1un  42380  lcmineqlem10  42405  3lexlogpow5ineq1  42421  3lexlogpow5ineq2  42422  3lexlogpow5ineq4  42423  aks4d1p1p7  42441  aks6d1c1p8  42482  sticksstones9  42521  sticksstones11  42523  aks6d1c7lem1  42547  nnmulcom  42639  3cubes  43044  jm2.23  43350  rmydioph  43368  rmxdioph  43370  expdiophlem2  43376  expdioph  43377  relexp2  44030  iunrelexpmin1  44061  iunrelexpmin2  44065  dftrcl3  44073  fvtrcllb1d  44075  cotrcltrcl  44078  corcltrcl  44092  cotrclrcl  44095  prmunb2  44664  sumsnd  45383  nnn0  45733  xrralrecnnge  45745  iooiinicc  45899  iooiinioc  45913  mccl  45955  sumnnodd  45987  wallispilem4  46423  wallispi2lem1  46426  wallispi2lem2  46427  stirlinglem8  46436  stirlinglem11  46439  stirlinglem12  46440  stirlinglem13  46441  fourierdlem31  46493  nnfoctbdjlem  46810  hoicvr  46903  hoicvrrex  46911  hoidmvlelem3  46952  ovnhoilem1  46956  ovnhoilem2  46957  ovnlecvr2  46965  ovnsubadd2lem  47000  iinhoiicclem  47028  vonicclem2  47039  nthrucw  47241  1elfzo1ceilhalf1  47694  iccpartlt  47781  257prm  47918  fmtnoprmfac2lem1  47923  fmtno4prmfac193  47930  fmtno4nprmfac193  47931  fmtno5nprm  47940  3ndvds4  47952  139prmALT  47953  31prm  47954  127prm  47956  3exp4mod41  47973  41prothprmlem2  47975  perfectALTVlem1  48078  perfectALTVlem2  48079  2exp340mod341  48090  341fppr2  48091  4fppr1  48092  nnsum3primesprm  48147  bgoldbtbndlem1  48162  tgblthelfgott  48172  nnsgrpmgm  48533  nnsgrpnmnd  48535  blennn0elnn  48934  blen1  48941  ackval42  49053