Theorem 1nn 12277

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 11257	. . . 4 ⊢ 1 ∈ V
2		fr0g 8476	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8475	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7910	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7100	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 692	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2838	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12267	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5698	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2765	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2840	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1540   ∈ wcel 2108  Vcvv 3480  ∅c0 4333   ↦ cmpt 5225  ran crn 5686   ↾ cres 5687   “ cima 5688   Fn wfn 6556  ‘cfv 6561  (class class class)co 7431  ωcom 7887  reccrdg 8449  1c1 11156   + caddc 11158  ℕcn 12266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432  ax-un 7755  ax-1cn 11213

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-ral 3062  df-rex 3071  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-pss 3971  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-tr 5260  df-id 5578  df-eprel 5584  df-po 5592  df-so 5593  df-fr 5637  df-we 5639  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-pred 6321  df-ord 6387  df-on 6388  df-lim 6389  df-suc 6390  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-ov 7434  df-om 7888  df-2nd 8015  df-frecs 8306  df-wrecs 8337  df-recs 8411  df-rdg 8450  df-nn 12267

This theorem is referenced by:  dfnn2  12279  dfnn3  12280  nnind  12284  nn1suc  12288  2nn  12339  nnunb  12522  1nn0  12542  nn0p1nn  12565  elz2  12631  1z  12647  neg1z  12653  nneo  12702  9p1e10  12735  elnn1uz2  12967  zq  12996  rpnnen1lem4  13022  rpnnen1lem5  13023  ser1const  14099  exp1  14108  nnexpcl  14115  expnbnd  14271  fac1  14316  faccl  14322  faclbnd3  14331  faclbnd4lem1  14332  faclbnd4lem2  14333  faclbnd4lem3  14334  faclbnd4lem4  14335  lsw0  14603  ccat2s1p1  14667  cats1un  14759  revs1  14803  cats1fvn  14897  relexpsucnnl  15069  relexpaddg  15092  isercolllem2  15702  isercolllem3  15703  isercoll  15704  sumsnf  15779  climcndslem1  15885  climcndslem2  15886  fprodnncl  15991  prodsn  15998  prodsnf  16000  nnrisefaccl  16055  eftlub  16145  eirrlem  16240  rpnnen2lem5  16254  rpnnen2lem8  16257  rpnnen2lem12  16261  dvdsle  16347  ndvdsp1  16448  5ndvds6  16451  gcd1  16565  bezoutr1  16606  1nprm  16716  1idssfct  16717  isprm2lem  16718  qden1elz  16794  phi1  16810  phiprm  16814  pcpre1  16880  pczpre  16885  pcmptcl  16929  pcmpt  16930  infpnlem2  16949  prmreclem1  16954  prmreclem6  16959  mul4sq  16992  vdwmc2  17017  vdwlem8  17026  vdwlem13  17031  vdwnnlem3  17035  prmocl  17072  prmop1  17076  fvprmselelfz  17082  fvprmselgcd1  17083  prmolefac  17084  prmodvdslcmf  17085  prmgapprmo  17100  5prm  17146  7prm  17148  11prm  17152  13prm  17153  17prm  17154  19prm  17155  37prm  17158  43prm  17159  83prm  17160  139prm  17161  163prm  17162  317prm  17163  631prm  17164  1259lem4  17171  1259lem5  17172  1259prm  17173  2503lem3  17176  2503prm  17177  4001lem1  17178  4001lem2  17179  4001lem3  17180  4001lem4  17181  4001prm  17182  baseid  17250  basendx  17256  basendxnn  17257  1strstr  17261  2strstr  17267  basendxnmulrndxOLD  17340  rngstr  17342  lmodstr  17369  topgrpstr  17405  otpsstr  17420  ocndx  17425  ocid  17426  basendxnocndx  17427  plendxnocndx  17428  basendxltdsndx  17432  dsndxnplusgndx  17434  dsndxnmulrndx  17435  slotsdnscsi  17436  dsndxntsetndx  17437  slotsdifdsndx  17438  basendxltunifndx  17442  unifndxntsetndx  17444  slotsdifunifndx  17445  slotsbhcdif  17459  slotsbhcdifOLD  17460  slotsdifocndx  17462  rescabsOLD  17878  catstr  18005  estrreslem1OLD  18182  ipostr  18574  mulgfval  19087  mulg1  19099  mulg2  19101  symgvalstructOLD  19415  od1  19577  0subgALT  19586  gex1  19609  efgsval2  19751  efgsp1  19755  torsubg  19872  pgpfaclem1  20101  opprbasOLD  20342  srabaseOLD  21178  sradsOLD  21192  cnfldfunALTOLDOLD  21393  zlmbasOLD  21530  znbas2OLD  21556  thlbasOLD  21715  thlleOLD  21717  opsrbasOLD  22070  pmatcollpw3fi1lem2  22793  hauspwdom  23509  tuslemOLD  24276  imasdsf1olem  24383  setsmsdsOLD  24488  tmslemOLD  24495  tnglemOLD  24654  tngbasOLD  24656  tngdsOLD  24669  cphipval  25277  bcthlem4  25361  bcth3  25365  ovolmge0  25512  ovollb2  25524  ovolctb  25525  ovolunlem1a  25531  ovolunlem1  25532  ovoliunlem1  25537  ovoliun  25540  ovoliun2  25541  ovolicc1  25551  voliunlem1  25585  volsup  25591  ioombl1lem2  25594  ioombl1lem4  25596  uniioombllem1  25616  uniioombllem2  25618  uniioombllem6  25623  itg1climres  25749  itg2seq  25777  itg2monolem1  25785  itg2monolem2  25786  itg2monolem3  25787  itg2mono  25788  itg2i1fseq2  25791  itg2cnlem1  25796  aalioulem5  26378  aaliou2b  26383  aaliou3lem4  26388  aaliou3lem7  26391  log2ub  26992  emcllem6  27044  emcllem7  27045  lgam1  27107  gam1  27108  ftalem7  27122  efnnfsumcl  27146  vmaprm  27160  efvmacl  27163  efchtdvds  27202  vma1  27209  prmorcht  27221  sqff1o  27225  pclogsum  27259  perfectlem1  27273  perfectlem2  27274  bpos1  27327  bposlem5  27332  lgsdir  27376  lgs1  27385  lgsquad2lem2  27429  addsqn2reu  27485  addsqrexnreu  27486  dchrmusumlema  27537  dchrisum0lema  27558  slotsinbpsd  28449  slotslnbpsd  28450  trkgstr  28452  ttgbasOLD  28888  ttgplusgOLD  28890  ttgvscaOLD  28893  eengstr  28995  basendxltedgfndx  29010  baseltedgfOLD  29011  usgrexmplef  29276  lfgrn1cycl  29825  clwwlkn1  30060  ipval2  30726  opsqrlem2  32160  ssnnssfz  32789  znumd  32814  zdend  32815  nnindf  32821  nn0min  32822  isarchi3  33194  eufndx  33293  eufid  33294  resvbasOLD  33360  rge0scvg  33948  zlmdsOLD  33962  qqh0  33985  qqh1  33986  esumfzf  34070  esumfsup  34071  esumpcvgval  34079  voliune  34230  eulerpartgbij  34374  eulerpartlemgs2  34382  fib2  34404  rrvsum  34456  ballotlem4  34501  ballotlemi1  34505  ballotlemii  34506  ballotlemic  34509  ballotlem1c  34510  hgt750lem  34666  hgt750leme  34673  0nn0m1nnn0  35118  faclimlem1  35743  nn0prpwlem  36323  nn0prpw  36324  poimirlem32  37659  ovoliunnfl  37669  voliunnfl  37671  volsupnfl  37672  incsequz  37755  bfplem1  37829  rrncmslem  37839  hlhilsbaseOLD  41943  60gcd7e1  42006  12lcm5e60  42009  60lcm7e420  42011  lcm1un  42014  lcmineqlem10  42039  3lexlogpow5ineq1  42055  3lexlogpow5ineq2  42056  3lexlogpow5ineq4  42057  aks4d1p1p7  42075  aks6d1c1p8  42116  sticksstones9  42155  sticksstones11  42157  aks6d1c7lem1  42181  nnmulcom  42307  3cubes  42701  jm2.23  43008  rmydioph  43026  rmxdioph  43028  expdiophlem2  43034  expdioph  43035  relexp2  43690  iunrelexpmin1  43721  iunrelexpmin2  43725  dftrcl3  43733  fvtrcllb1d  43735  cotrcltrcl  43738  corcltrcl  43752  cotrclrcl  43755  mnringbasedOLD  44231  prmunb2  44330  sumsnd  45031  nnn0  45389  xrralrecnnge  45401  iooiinicc  45555  iooiinioc  45569  mccl  45613  sumnnodd  45645  wallispilem4  46083  wallispi2lem1  46086  wallispi2lem2  46087  stirlinglem8  46096  stirlinglem11  46099  stirlinglem12  46100  stirlinglem13  46101  fourierdlem31  46153  nnfoctbdjlem  46470  hoicvr  46563  hoicvrrex  46571  hoidmvlelem3  46612  ovnhoilem1  46616  ovnhoilem2  46617  ovnlecvr2  46625  ovnsubadd2lem  46660  iinhoiicclem  46688  vonicclem2  46699  iccpartlt  47411  257prm  47548  fmtnoprmfac2lem1  47553  fmtno4prmfac193  47560  fmtno4nprmfac193  47561  fmtno5nprm  47570  3ndvds4  47582  139prmALT  47583  31prm  47584  127prm  47586  3exp4mod41  47603  41prothprmlem2  47605  perfectALTVlem1  47708  perfectALTVlem2  47709  2exp340mod341  47720  341fppr2  47721  4fppr1  47722  nnsum3primesprm  47777  bgoldbtbndlem1  47792  tgblthelfgott  47802  nnsgrpmgm  48092  nnsgrpnmnd  48094  blennn0elnn  48498  blen1  48505  ackval42  48617