Theorem 1nn 11889

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 10877	. . . 4 ⊢ 1 ∈ V
2		fr0g 8213	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8212	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7707	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 6937	. . . 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 2837	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 11879	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5592	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2767	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2839	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1543   ∈ wcel 2112  Vcvv 3423  ∅c0 4254   ↦ cmpt 5152  ran crn 5580   ↾ cres 5581   “ cima 5582   Fn wfn 6410  ‘cfv 6415  (class class class)co 7252  ωcom 7684  reccrdg 8187  1c1 10778   + caddc 10780  ℕcn 11878

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2114  ax-9 2122  ax-10 2143  ax-11 2160  ax-12 2177  ax-ext 2710  ax-sep 5216  ax-nul 5223  ax-pr 5346  ax-un 7563  ax-1cn 10835

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-3or 1090  df-3an 1091  df-tru 1546  df-fal 1556  df-ex 1788  df-nf 1792  df-sb 2073  df-mo 2541  df-eu 2570  df-clab 2717  df-cleq 2731  df-clel 2818  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3071  df-rab 3073  df-v 3425  df-sbc 3713  df-csb 3830  df-dif 3887  df-un 3889  df-in 3891  df-ss 3901  df-pss 3903  df-nul 4255  df-if 4457  df-pw 4532  df-sn 4559  df-pr 4561  df-tp 4563  df-op 4565  df-uni 4837  df-iun 4923  df-br 5071  df-opab 5133  df-mpt 5153  df-tr 5186  df-id 5479  df-eprel 5485  df-po 5493  df-so 5494  df-fr 5534  df-we 5536  df-xp 5585  df-rel 5586  df-cnv 5587  df-co 5588  df-dm 5589  df-rn 5590  df-res 5591  df-ima 5592  df-pred 6189  df-ord 6251  df-on 6252  df-lim 6253  df-suc 6254  df-iota 6373  df-fun 6417  df-fn 6418  df-f 6419  df-f1 6420  df-fo 6421  df-f1o 6422  df-fv 6423  df-om 7685  df-wrecs 8089  df-recs 8150  df-rdg 8188  df-nn 11879

This theorem is referenced by:  dfnn2  11891  dfnn3  11892  nnind  11896  nn1suc  11900  2nn  11951  nnunb  12134  1nn0  12154  nn0p1nn  12177  elz2  12242  1z  12255  neg1z  12261  nneo  12309  9p1e10  12343  elnn1uz2  12569  zq  12598  rpnnen1lem4  12624  rpnnen1lem5  12625  ser1const  13682  exp1  13691  nnexpcl  13698  expnbnd  13850  fac1  13894  faccl  13900  faclbnd3  13909  faclbnd4lem1  13910  faclbnd4lem2  13911  faclbnd4lem3  13912  faclbnd4lem4  13913  lsw0  14171  ccat2s1p1  14239  ccat2s1p1OLD  14241  cats1un  14337  revs1  14381  cats1fvn  14474  relexpsucnnl  14644  relexpaddg  14667  isercolllem2  15280  isercolllem3  15281  isercoll  15282  sumsnf  15358  climcndslem1  15464  climcndslem2  15465  fprodnncl  15568  prodsn  15575  prodsnf  15577  nnrisefaccl  15632  eftlub  15721  eirrlem  15816  rpnnen2lem5  15830  rpnnen2lem8  15833  rpnnen2lem12  15837  dvdsle  15922  ndvdsp1  16023  gcd1  16138  bezoutr1  16177  1nprm  16287  1idssfct  16288  isprm2lem  16289  qden1elz  16364  phi1  16377  phiprm  16381  pcpre1  16446  pczpre  16451  pcmptcl  16495  pcmpt  16496  infpnlem2  16515  prmreclem1  16520  prmreclem6  16525  mul4sq  16558  vdwmc2  16583  vdwlem8  16592  vdwlem13  16597  vdwnnlem3  16601  prmocl  16638  prmop1  16642  fvprmselelfz  16648  fvprmselgcd1  16649  prmolefac  16650  prmodvdslcmf  16651  prmgapprmo  16666  5prm  16713  7prm  16715  11prm  16719  13prm  16720  17prm  16721  19prm  16722  37prm  16725  43prm  16726  83prm  16727  139prm  16728  163prm  16729  317prm  16730  631prm  16731  1259lem4  16738  1259lem5  16739  1259prm  16740  2503lem3  16743  2503prm  16744  4001lem1  16745  4001lem2  16746  4001lem3  16747  4001lem4  16748  4001prm  16749  baseid  16818  basendx  16824  basendxnn  16825  basendxnnOLD  16826  1strstr  16830  2strstr  16835  ressval3dOLD  16858  basendxnplusgndxOLD  16894  basendxnmulrndxOLD  16907  rngstr  16909  lmodstr  16936  topgrpstr  16970  otpsstr  16984  ocndx  16989  ocid  16990  basendxltdsndx  16994  dsndxnplusgndx  16996  dsndxnmulrndx  16997  slotsdnscsi  16998  dsndxntsetndx  16999  basendxltunifndx  17003  unifndxntsetndx  17005  slotsbhcdif  17019  slotsbhcdifOLD  17020  oppcbasOLD  17321  rescbasOLD  17434  rescabs  17439  catstr  17565  estrreslem1OLD  17745  ipostr  18137  mulgfval  18592  mulg1  18601  mulg2  18603  oppgbasOLD  18847  symgvalstructOLD  18895  od1  19056  gex1  19086  efgsval2  19229  efgsp1  19233  torsubg  19345  pgpfaclem1  19574  mgpbasOLD  19617  mgpdsOLD  19624  opprbasOLD  19760  rmodislmodOLD  20082  srabaseOLD  20332  sradsOLD  20344  cnfldfun  20497  zlmbasOLD  20608  znbas2OLD  20632  thlbas  20788  thlle  20789  opsrbasOLD  21138  pmatcollpw3fi1lem2  21819  hauspwdom  22535  tuslemOLD  23302  imasdsf1olem  23409  setsmsds  23512  tmslemOLD  23519  tnglemOLD  23678  tngbasOLD  23680  tngdsOLD  23693  cphipval  24287  bcthlem4  24371  bcth3  24375  ovolmge0  24521  ovollb2  24533  ovolctb  24534  ovolunlem1a  24540  ovolunlem1  24541  ovoliunlem1  24546  ovoliun  24549  ovoliun2  24550  ovolicc1  24560  voliunlem1  24594  volsup  24600  ioombl1lem2  24603  ioombl1lem4  24605  uniioombllem1  24625  uniioombllem2  24627  uniioombllem6  24632  itg1climres  24759  itg2seq  24787  itg2monolem1  24795  itg2monolem2  24796  itg2monolem3  24797  itg2mono  24798  itg2i1fseq2  24801  itg2cnlem1  24806  aalioulem5  25376  aaliou2b  25381  aaliou3lem4  25386  aaliou3lem7  25389  log2ub  25979  emcllem6  26030  emcllem7  26031  lgam1  26093  gam1  26094  ftalem7  26108  efnnfsumcl  26132  vmaprm  26146  efvmacl  26149  efchtdvds  26188  vma1  26195  prmorcht  26207  sqff1o  26211  pclogsum  26243  perfectlem1  26257  perfectlem2  26258  bpos1  26311  bposlem5  26316  lgsdir  26360  lgs1  26369  lgsquad2lem2  26413  addsqn2reu  26469  addsqrexnreu  26470  dchrmusumlema  26521  dchrisum0lema  26542  slotsinbpsd  26682  slotslnbpsd  26683  trkgstr  26684  ttgbasOLD  27119  ttgplusgOLD  27121  ttgvscaOLD  27124  eengstr  27226  baseltedgf  27241  baseltedgfOLD  27242  usgrexmplef  27504  lfgrn1cycl  28046  clwwlkn1  28281  ipval2  28945  opsqrlem2  30379  ssnnssfz  30985  nnindf  31010  nn0min  31011  isarchi3  31318  resvbasOLD  31410  rge0scvg  31776  zlmds  31789  qqh0  31809  qqh1  31810  esumfzf  31912  esumfsup  31913  esumpcvgval  31921  voliune  32072  eulerpartgbij  32214  eulerpartlemgs2  32222  fib2  32244  rrvsum  32296  ballotlem4  32340  ballotlemi1  32344  ballotlemii  32345  ballotlemic  32348  ballotlem1c  32349  hgt750lem  32506  hgt750leme  32513  0nn0m1nnn0  32946  faclimlem1  33590  nn0prpwlem  34413  nn0prpw  34414  poimirlem32  35715  ovoliunnfl  35725  voliunnfl  35727  volsupnfl  35728  incsequz  35812  bfplem1  35886  rrncmslem  35896  hlhilsbaseOLD  39861  60gcd7e1  39920  12lcm5e60  39923  60lcm7e420  39925  lcm1un  39928  lcmineqlem10  39953  3lexlogpow5ineq1  39969  3lexlogpow5ineq2  39970  3lexlogpow5ineq4  39971  aks4d1p1p7  39988  sticksstones9  40010  sticksstones11  40012  nnmulcom  40195  3cubes  40400  jm2.23  40706  rmydioph  40724  rmxdioph  40726  expdiophlem2  40732  expdioph  40733  relexp2  41147  iunrelexpmin1  41178  iunrelexpmin2  41182  dftrcl3  41190  fvtrcllb1d  41192  cotrcltrcl  41195  corcltrcl  41209  cotrclrcl  41212  mnringbasedOLD  41692  prmunb2  41791  sumsnd  42431  nnn0  42780  xrralrecnnge  42793  iooiinicc  42943  iooiinioc  42957  mccl  43002  sumnnodd  43034  wallispilem4  43472  wallispi2lem1  43475  wallispi2lem2  43476  stirlinglem8  43485  stirlinglem11  43488  stirlinglem12  43489  stirlinglem13  43490  fourierdlem31  43542  nnfoctbdjlem  43856  hoicvr  43949  hoicvrrex  43957  hoidmvlelem3  43998  ovnhoilem1  44002  ovnhoilem2  44003  ovnlecvr2  44011  ovnsubadd2lem  44046  iinhoiicclem  44074  vonicclem2  44085  iccpartlt  44737  257prm  44874  fmtnoprmfac2lem1  44879  fmtno4prmfac193  44886  fmtno4nprmfac193  44887  fmtno5nprm  44896  3ndvds4  44908  139prmALT  44909  31prm  44910  127prm  44912  3exp4mod41  44929  41prothprmlem2  44931  perfectALTVlem1  45034  perfectALTVlem2  45035  2exp340mod341  45046  341fppr2  45047  4fppr1  45048  nnsum3primesprm  45103  bgoldbtbndlem1  45118  tgblthelfgott  45128  nnsgrpmgm  45231  nnsgrpnmnd  45233  blennn0elnn  45784  blen1  45791  ackval42  45903