Theorem 1nn 12170

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 11142	. . . 4 ⊢ 1 ∈ V
2		fr0g 8379	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8378	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7843	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7036	. . . 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 12160	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5647	. . 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 5635   ↾ cres 5636   “ cima 5637   Fn wfn 6497  ‘cfv 6502  (class class class)co 7370  ωcom 7820  reccrdg 8352  1c1 11041   + caddc 11043  ℕcn 12159

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 5245  ax-nul 5255  ax-pr 5381  ax-un 7692  ax-1cn 11098

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 5529  df-eprel 5534  df-po 5542  df-so 5543  df-fr 5587  df-we 5589  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-pred 6269  df-ord 6330  df-on 6331  df-lim 6332  df-suc 6333  df-iota 6458  df-fun 6504  df-fn 6505  df-f 6506  df-f1 6507  df-fo 6508  df-f1o 6509  df-fv 6510  df-ov 7373  df-om 7821  df-2nd 7946  df-frecs 8235  df-wrecs 8266  df-recs 8315  df-rdg 8353  df-nn 12160

This theorem is referenced by:  dfnn2  12172  dfnn3  12173  nnind  12177  nn1suc  12181  2nn  12232  nnunb  12411  1nn0  12431  nn0p1nn  12454  elz2  12520  1z  12535  neg1z  12541  nneo  12590  9p1e10  12623  elnn1uz2  12852  zq  12881  rpnnen1lem4  12907  rpnnen1lem5  12908  1elfzo1  13644  ser1const  13995  exp1  14004  nnexpcl  14011  expnbnd  14169  fac1  14214  faccl  14220  faclbnd3  14229  faclbnd4lem1  14230  faclbnd4lem2  14231  faclbnd4lem3  14232  faclbnd4lem4  14233  lsw0  14502  ccat2s1p1  14567  cats1un  14658  revs1  14702  cats1fvn  14795  relexpsucnnl  14967  relexpaddg  14990  isercolllem2  15603  isercolllem3  15604  isercoll  15605  sumsnf  15680  climcndslem1  15786  climcndslem2  15787  fprodnncl  15892  prodsn  15899  prodsnf  15901  nnrisefaccl  15956  eftlub  16048  eirrlem  16143  rpnnen2lem5  16157  rpnnen2lem8  16160  rpnnen2lem12  16164  dvdsle  16251  ndvdsp1  16352  5ndvds6  16355  gcd1  16469  bezoutr1  16510  1nprm  16620  1idssfct  16621  isprm2lem  16622  qden1elz  16698  phi1  16714  phiprm  16718  pcpre1  16784  pczpre  16789  pcmptcl  16833  pcmpt  16834  infpnlem2  16853  prmreclem1  16858  prmreclem6  16863  mul4sq  16896  vdwmc2  16921  vdwlem8  16930  vdwlem13  16935  vdwnnlem3  16939  prmocl  16976  prmop1  16980  fvprmselelfz  16986  fvprmselgcd1  16987  prmolefac  16988  prmodvdslcmf  16989  prmgapprmo  17004  5prm  17050  7prm  17052  11prm  17056  13prm  17057  17prm  17058  19prm  17059  37prm  17062  43prm  17063  83prm  17064  139prm  17065  163prm  17066  317prm  17067  631prm  17068  1259lem4  17075  1259lem5  17076  1259prm  17077  2503lem3  17080  2503prm  17081  4001lem1  17082  4001lem2  17083  4001lem3  17084  4001lem4  17085  4001prm  17086  baseid  17153  basendx  17159  basendxnn  17160  rngstr  17232  lmodstr  17259  topgrpstr  17295  otpsstr  17310  ocndx  17315  ocid  17316  basendxnocndx  17317  plendxnocndx  17318  basendxltdsndx  17322  dsndxnplusgndx  17324  dsndxnmulrndx  17325  slotsdnscsi  17326  dsndxntsetndx  17327  slotsdifdsndx  17328  basendxltunifndx  17332  unifndxntsetndx  17334  slotsdifunifndx  17335  slotsbhcdif  17349  slotsdifocndx  17351  catstr  17898  ipostr  18466  mulgfval  19016  mulg1  19028  mulg2  19030  od1  19505  0subgALT  19514  gex1  19537  efgsval2  19679  efgsp1  19683  torsubg  19800  pgpfaclem1  20029  pmatcollpw3fi1lem2  22748  hauspwdom  23462  imasdsf1olem  24334  cphipval  25216  bcthlem4  25300  bcth3  25304  ovolmge0  25451  ovollb2  25463  ovolctb  25464  ovolunlem1a  25470  ovolunlem1  25471  ovoliunlem1  25476  ovoliun  25479  ovoliun2  25480  ovolicc1  25490  voliunlem1  25524  volsup  25530  ioombl1lem2  25533  ioombl1lem4  25535  uniioombllem1  25555  uniioombllem2  25557  uniioombllem6  25562  itg1climres  25688  itg2seq  25716  itg2monolem1  25724  itg2monolem2  25725  itg2monolem3  25726  itg2mono  25727  itg2i1fseq2  25730  itg2cnlem1  25735  aalioulem5  26317  aaliou2b  26322  aaliou3lem4  26327  aaliou3lem7  26330  log2ub  26932  emcllem6  26984  emcllem7  26985  lgam1  27047  gam1  27048  ftalem7  27062  efnnfsumcl  27086  vmaprm  27100  efvmacl  27103  efchtdvds  27142  vma1  27149  prmorcht  27161  sqff1o  27165  pclogsum  27199  perfectlem1  27213  perfectlem2  27214  bpos1  27267  bposlem5  27272  lgsdir  27316  lgs1  27325  lgsquad2lem2  27369  addsqn2reu  27425  addsqrexnreu  27426  dchrmusumlema  27477  dchrisum0lema  27498  slotsinbpsd  28530  slotslnbpsd  28531  trkgstr  28533  eengstr  29071  basendxltedgfndx  29085  usgrexmplef  29350  lfgrn1cycl  29896  clwwlkn1  30134  ipval2  30801  opsqrlem2  32235  ssnnssfz  32884  znumd  32910  zdend  32911  nnindf  32917  nn0min  32918  isarchi3  33287  eufndx  33390  eufid  33391  constrext2chnlem  33934  iconstr  33950  rge0scvg  34133  qqh0  34168  qqh1  34169  esumfzf  34253  esumfsup  34254  esumpcvgval  34262  voliune  34413  eulerpartgbij  34556  eulerpartlemgs2  34564  fib2  34586  rrvsum  34638  ballotlem4  34683  ballotlemi1  34687  ballotlemii  34688  ballotlemic  34691  ballotlem1c  34692  hgt750lem  34835  hgt750leme  34842  0nn0m1nnn0  35335  faclimlem1  35965  nn0prpwlem  36544  nn0prpw  36545  poimirlem32  37932  ovoliunnfl  37942  voliunnfl  37944  volsupnfl  37945  incsequz  38028  bfplem1  38102  rrncmslem  38112  60gcd7e1  42404  12lcm5e60  42407  60lcm7e420  42409  lcm1un  42412  lcmineqlem10  42437  3lexlogpow5ineq1  42453  3lexlogpow5ineq2  42454  3lexlogpow5ineq4  42455  aks4d1p1p7  42473  aks6d1c1p8  42514  sticksstones9  42553  sticksstones11  42555  aks6d1c7lem1  42579  nnmulcom  42671  3cubes  43076  jm2.23  43382  rmydioph  43400  rmxdioph  43402  expdiophlem2  43408  expdioph  43409  relexp2  44062  iunrelexpmin1  44093  iunrelexpmin2  44097  dftrcl3  44105  fvtrcllb1d  44107  cotrcltrcl  44110  corcltrcl  44124  cotrclrcl  44127  prmunb2  44696  sumsnd  45415  nnn0  45765  xrralrecnnge  45777  iooiinicc  45931  iooiinioc  45945  mccl  45987  sumnnodd  46019  wallispilem4  46455  wallispi2lem1  46458  wallispi2lem2  46459  stirlinglem8  46468  stirlinglem11  46471  stirlinglem12  46472  stirlinglem13  46473  fourierdlem31  46525  nnfoctbdjlem  46842  hoicvrrex  46943  hoidmvlelem3  46984  ovnhoilem1  46988  ovnhoilem2  46989  ovnlecvr2  46997  ovnsubadd2lem  47032  iinhoiicclem  47060  vonicclem2  47071  nthrucw  47273  1elfzo1ceilhalf1  47726  iccpartlt  47813  257prm  47950  fmtnoprmfac2lem1  47955  fmtno4prmfac193  47962  fmtno4nprmfac193  47963  fmtno5nprm  47972  3ndvds4  47984  139prmALT  47985  31prm  47986  127prm  47988  3exp4mod41  48005  41prothprmlem2  48007  perfectALTVlem1  48110  perfectALTVlem2  48111  2exp340mod341  48122  341fppr2  48123  4fppr1  48124  nnsum3primesprm  48179  bgoldbtbndlem1  48194  tgblthelfgott  48204  nnsgrpmgm  48565  nnsgrpnmnd  48567  blennn0elnn  48966  blen1  48973  ackval42  49085