Theorem 1nn 12145

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 11117	. . . 4 ⊢ 1 ∈ V
2		fr0g 8363	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8362	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7827	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7021	. . . 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 2830	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12135	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5634	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2756	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2832	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1541   ∈ wcel 2113  Vcvv 3437  ∅c0 4282   ↦ cmpt 5176  ran crn 5622   ↾ cres 5623   “ cima 5624   Fn wfn 6483  ‘cfv 6488  (class class class)co 7354  ωcom 7804  reccrdg 8336  1c1 11016   + caddc 11018  ℕcn 12134

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705  ax-sep 5238  ax-nul 5248  ax-pr 5374  ax-un 7676  ax-1cn 11073

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2725  df-clel 2808  df-nfc 2882  df-ne 2930  df-ral 3049  df-rex 3058  df-reu 3348  df-rab 3397  df-v 3439  df-sbc 3738  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-pss 3918  df-nul 4283  df-if 4477  df-pw 4553  df-sn 4578  df-pr 4580  df-op 4584  df-uni 4861  df-iun 4945  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5516  df-eprel 5521  df-po 5529  df-so 5530  df-fr 5574  df-we 5576  df-xp 5627  df-rel 5628  df-cnv 5629  df-co 5630  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634  df-pred 6255  df-ord 6316  df-on 6317  df-lim 6318  df-suc 6319  df-iota 6444  df-fun 6490  df-fn 6491  df-f 6492  df-f1 6493  df-fo 6494  df-f1o 6495  df-fv 6496  df-ov 7357  df-om 7805  df-2nd 7930  df-frecs 8219  df-wrecs 8250  df-recs 8299  df-rdg 8337  df-nn 12135

This theorem is referenced by:  dfnn2  12147  dfnn3  12148  nnind  12152  nn1suc  12156  2nn  12207  nnunb  12386  1nn0  12406  nn0p1nn  12429  elz2  12495  1z  12510  neg1z  12516  nneo  12565  9p1e10  12598  elnn1uz2  12827  zq  12856  rpnnen1lem4  12882  rpnnen1lem5  12883  1elfzo1  13618  ser1const  13969  exp1  13978  nnexpcl  13985  expnbnd  14143  fac1  14188  faccl  14194  faclbnd3  14203  faclbnd4lem1  14204  faclbnd4lem2  14205  faclbnd4lem3  14206  faclbnd4lem4  14207  lsw0  14476  ccat2s1p1  14541  cats1un  14632  revs1  14676  cats1fvn  14769  relexpsucnnl  14941  relexpaddg  14964  isercolllem2  15577  isercolllem3  15578  isercoll  15579  sumsnf  15654  climcndslem1  15760  climcndslem2  15761  fprodnncl  15866  prodsn  15873  prodsnf  15875  nnrisefaccl  15930  eftlub  16022  eirrlem  16117  rpnnen2lem5  16131  rpnnen2lem8  16134  rpnnen2lem12  16138  dvdsle  16225  ndvdsp1  16326  5ndvds6  16329  gcd1  16443  bezoutr1  16484  1nprm  16594  1idssfct  16595  isprm2lem  16596  qden1elz  16672  phi1  16688  phiprm  16692  pcpre1  16758  pczpre  16763  pcmptcl  16807  pcmpt  16808  infpnlem2  16827  prmreclem1  16832  prmreclem6  16837  mul4sq  16870  vdwmc2  16895  vdwlem8  16904  vdwlem13  16909  vdwnnlem3  16913  prmocl  16950  prmop1  16954  fvprmselelfz  16960  fvprmselgcd1  16961  prmolefac  16962  prmodvdslcmf  16963  prmgapprmo  16978  5prm  17024  7prm  17026  11prm  17030  13prm  17031  17prm  17032  19prm  17033  37prm  17036  43prm  17037  83prm  17038  139prm  17039  163prm  17040  317prm  17041  631prm  17042  1259lem4  17049  1259lem5  17050  1259prm  17051  2503lem3  17054  2503prm  17055  4001lem1  17056  4001lem2  17057  4001lem3  17058  4001lem4  17059  4001prm  17060  baseid  17127  basendx  17133  basendxnn  17134  rngstr  17206  lmodstr  17233  topgrpstr  17269  otpsstr  17284  ocndx  17289  ocid  17290  basendxnocndx  17291  plendxnocndx  17292  basendxltdsndx  17296  dsndxnplusgndx  17298  dsndxnmulrndx  17299  slotsdnscsi  17300  dsndxntsetndx  17301  slotsdifdsndx  17302  basendxltunifndx  17306  unifndxntsetndx  17308  slotsdifunifndx  17309  slotsbhcdif  17323  slotsdifocndx  17325  catstr  17871  ipostr  18439  mulgfval  18986  mulg1  18998  mulg2  19000  od1  19475  0subgALT  19484  gex1  19507  efgsval2  19649  efgsp1  19653  torsubg  19770  pgpfaclem1  19999  pmatcollpw3fi1lem2  22705  hauspwdom  23419  imasdsf1olem  24291  cphipval  25173  bcthlem4  25257  bcth3  25261  ovolmge0  25408  ovollb2  25420  ovolctb  25421  ovolunlem1a  25427  ovolunlem1  25428  ovoliunlem1  25433  ovoliun  25436  ovoliun2  25437  ovolicc1  25447  voliunlem1  25481  volsup  25487  ioombl1lem2  25490  ioombl1lem4  25492  uniioombllem1  25512  uniioombllem2  25514  uniioombllem6  25519  itg1climres  25645  itg2seq  25673  itg2monolem1  25681  itg2monolem2  25682  itg2monolem3  25683  itg2mono  25684  itg2i1fseq2  25687  itg2cnlem1  25692  aalioulem5  26274  aaliou2b  26279  aaliou3lem4  26284  aaliou3lem7  26287  log2ub  26889  emcllem6  26941  emcllem7  26942  lgam1  27004  gam1  27005  ftalem7  27019  efnnfsumcl  27043  vmaprm  27057  efvmacl  27060  efchtdvds  27099  vma1  27106  prmorcht  27118  sqff1o  27122  pclogsum  27156  perfectlem1  27170  perfectlem2  27171  bpos1  27224  bposlem5  27229  lgsdir  27273  lgs1  27282  lgsquad2lem2  27326  addsqn2reu  27382  addsqrexnreu  27383  dchrmusumlema  27434  dchrisum0lema  27455  slotsinbpsd  28422  slotslnbpsd  28423  trkgstr  28425  eengstr  28962  basendxltedgfndx  28976  usgrexmplef  29241  lfgrn1cycl  29787  clwwlkn1  30025  ipval2  30691  opsqrlem2  32125  ssnnssfz  32776  znumd  32802  zdend  32803  nnindf  32809  nn0min  32810  isarchi3  33165  eufndx  33265  eufid  33266  constrext2chnlem  33786  iconstr  33802  rge0scvg  33985  qqh0  34020  qqh1  34021  esumfzf  34105  esumfsup  34106  esumpcvgval  34114  voliune  34265  eulerpartgbij  34408  eulerpartlemgs2  34416  fib2  34438  rrvsum  34490  ballotlem4  34535  ballotlemi1  34539  ballotlemii  34540  ballotlemic  34543  ballotlem1c  34544  hgt750lem  34687  hgt750leme  34694  0nn0m1nnn0  35180  faclimlem1  35810  nn0prpwlem  36389  nn0prpw  36390  poimirlem32  37715  ovoliunnfl  37725  voliunnfl  37727  volsupnfl  37728  incsequz  37811  bfplem1  37885  rrncmslem  37895  60gcd7e1  42121  12lcm5e60  42124  60lcm7e420  42126  lcm1un  42129  lcmineqlem10  42154  3lexlogpow5ineq1  42170  3lexlogpow5ineq2  42171  3lexlogpow5ineq4  42172  aks4d1p1p7  42190  aks6d1c1p8  42231  sticksstones9  42270  sticksstones11  42272  aks6d1c7lem1  42296  nnmulcom  42393  3cubes  42810  jm2.23  43116  rmydioph  43134  rmxdioph  43136  expdiophlem2  43142  expdioph  43143  relexp2  43797  iunrelexpmin1  43828  iunrelexpmin2  43832  dftrcl3  43840  fvtrcllb1d  43842  cotrcltrcl  43845  corcltrcl  43859  cotrclrcl  43862  prmunb2  44431  sumsnd  45150  nnn0  45503  xrralrecnnge  45515  iooiinicc  45669  iooiinioc  45683  mccl  45725  sumnnodd  45757  wallispilem4  46193  wallispi2lem1  46196  wallispi2lem2  46197  stirlinglem8  46206  stirlinglem11  46209  stirlinglem12  46210  stirlinglem13  46211  fourierdlem31  46263  nnfoctbdjlem  46580  hoicvr  46673  hoicvrrex  46681  hoidmvlelem3  46722  ovnhoilem1  46726  ovnhoilem2  46727  ovnlecvr2  46735  ovnsubadd2lem  46770  iinhoiicclem  46798  vonicclem2  46809  nthrucw  47011  1elfzo1ceilhalf1  47464  iccpartlt  47551  257prm  47688  fmtnoprmfac2lem1  47693  fmtno4prmfac193  47700  fmtno4nprmfac193  47701  fmtno5nprm  47710  3ndvds4  47722  139prmALT  47723  31prm  47724  127prm  47726  3exp4mod41  47743  41prothprmlem2  47745  perfectALTVlem1  47848  perfectALTVlem2  47849  2exp340mod341  47860  341fppr2  47861  4fppr1  47862  nnsum3primesprm  47917  bgoldbtbndlem1  47932  tgblthelfgott  47942  nnsgrpmgm  48303  nnsgrpnmnd  48305  blennn0elnn  48705  blen1  48712  ackval42  48824