Theorem 1nn 11685

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 10675	. . . 4 ⊢ 1 ∈ V
2		fr0g 8081	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8080	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7600	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 6839	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 691	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2849	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 11675	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5537	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2781	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2851	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1538   ∈ wcel 2111  Vcvv 3409  ∅c0 4225   ↦ cmpt 5112  ran crn 5525   ↾ cres 5526   “ cima 5527   Fn wfn 6330  ‘cfv 6335  (class class class)co 7150  ωcom 7579  reccrdg 8055  1c1 10576   + caddc 10578  ℕcn 11674

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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298  ax-un 7459  ax-1cn 10633

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-ral 3075  df-rex 3076  df-reu 3077  df-rab 3079  df-v 3411  df-sbc 3697  df-csb 3806  df-dif 3861  df-un 3863  df-in 3865  df-ss 3875  df-pss 3877  df-nul 4226  df-if 4421  df-pw 4496  df-sn 4523  df-pr 4525  df-tp 4527  df-op 4529  df-uni 4799  df-iun 4885  df-br 5033  df-opab 5095  df-mpt 5113  df-tr 5139  df-id 5430  df-eprel 5435  df-po 5443  df-so 5444  df-fr 5483  df-we 5485  df-xp 5530  df-rel 5531  df-cnv 5532  df-co 5533  df-dm 5534  df-rn 5535  df-res 5536  df-ima 5537  df-pred 6126  df-ord 6172  df-on 6173  df-lim 6174  df-suc 6175  df-iota 6294  df-fun 6337  df-fn 6338  df-f 6339  df-f1 6340  df-fo 6341  df-f1o 6342  df-fv 6343  df-om 7580  df-wrecs 7957  df-recs 8018  df-rdg 8056  df-nn 11675

This theorem is referenced by:  dfnn2  11687  dfnn3  11688  nnind  11692  nn1suc  11696  2nn  11747  nnunb  11930  1nn0  11950  nn0p1nn  11973  elz2  12038  1z  12051  neg1z  12057  nneo  12105  9p1e10  12139  elnn1uz2  12365  zq  12394  rpnnen1lem4  12420  rpnnen1lem5  12421  ser1const  13476  exp1  13485  nnexpcl  13492  expnbnd  13643  fac1  13687  faccl  13693  faclbnd3  13702  faclbnd4lem1  13703  faclbnd4lem2  13704  faclbnd4lem3  13705  faclbnd4lem4  13706  lsw0  13964  ccat2s1p1  14032  ccat2s1p1OLD  14034  cats1un  14130  revs1  14174  cats1fvn  14267  relexpsucnnl  14437  relexpaddg  14460  isercolllem2  15070  isercolllem3  15071  isercoll  15072  sumsnf  15147  climcndslem1  15252  climcndslem2  15253  fprodnncl  15357  prodsn  15364  prodsnf  15366  nnrisefaccl  15421  eftlub  15510  eirrlem  15605  rpnnen2lem5  15619  rpnnen2lem8  15622  rpnnen2lem12  15626  dvdsle  15711  ndvdsp1  15812  gcd1  15927  bezoutr1  15965  1nprm  16075  1idssfct  16076  isprm2lem  16077  qden1elz  16152  phi1  16165  phiprm  16169  pcpre1  16234  pczpre  16239  pcmptcl  16282  pcmpt  16283  infpnlem2  16302  prmreclem1  16307  prmreclem6  16312  mul4sq  16345  vdwmc2  16370  vdwlem8  16379  vdwlem13  16384  vdwnnlem3  16388  prmocl  16425  prmop1  16429  fvprmselelfz  16435  fvprmselgcd1  16436  prmolefac  16437  prmodvdslcmf  16438  prmgapprmo  16453  5prm  16500  7prm  16502  11prm  16506  13prm  16507  17prm  16508  19prm  16509  37prm  16512  43prm  16513  83prm  16514  139prm  16515  163prm  16516  317prm  16517  631prm  16518  1259lem4  16525  1259lem5  16526  1259prm  16527  2503lem3  16530  2503prm  16531  4001lem1  16532  4001lem2  16533  4001lem3  16534  4001lem4  16535  4001prm  16536  baseid  16601  basendx  16605  basendxnn  16606  ressval3d  16619  1strstr  16656  2strstr  16660  basendxnplusgndx  16666  basendxnmulrndx  16676  rngstr  16677  lmodstr  16694  topgrpstr  16719  otpsstr  16726  ocndx  16731  ocid  16732  ressds  16744  resshom  16749  ressco  16750  slotsbhcdif  16751  oppcbas  17046  rescbas  17158  rescabs  17162  catstr  17286  estrreslem1  17453  ipostr  17829  mulgfval  18293  mulg1  18302  mulg2  18304  oppgbas  18546  symgvalstruct  18592  od1  18753  gex1  18783  efgsval2  18926  efgsp1  18930  torsubg  19042  pgpfaclem1  19271  mgpbas  19313  mgpds  19317  opprbas  19450  rmodislmod  19770  srabase  20018  srads  20026  cnfldfun  20178  zlmbas  20287  znbas2  20307  thlbas  20461  thlle  20462  opsrbas  20810  pmatcollpw3fi1lem2  21487  hauspwdom  22201  ressunif  22963  tuslem  22968  imasdsf1olem  23075  setsmsds  23178  tmslem  23184  tnglem  23342  tngbas  23343  tngds  23350  cphipval  23943  bcthlem4  24027  bcth3  24031  ovolmge0  24177  ovollb2  24189  ovolctb  24190  ovolunlem1a  24196  ovolunlem1  24197  ovoliunlem1  24202  ovoliun  24205  ovoliun2  24206  ovolicc1  24216  voliunlem1  24250  volsup  24256  ioombl1lem2  24259  ioombl1lem4  24261  uniioombllem1  24281  uniioombllem2  24283  uniioombllem6  24288  itg1climres  24414  itg2seq  24442  itg2monolem1  24450  itg2monolem2  24451  itg2monolem3  24452  itg2mono  24453  itg2i1fseq2  24456  itg2cnlem1  24461  aalioulem5  25031  aaliou2b  25036  aaliou3lem4  25041  aaliou3lem7  25044  log2ub  25634  emcllem6  25685  emcllem7  25686  lgam1  25748  gam1  25749  ftalem7  25763  efnnfsumcl  25787  vmaprm  25801  efvmacl  25804  efchtdvds  25843  vma1  25850  prmorcht  25862  sqff1o  25866  pclogsum  25898  perfectlem1  25912  perfectlem2  25913  bpos1  25966  bposlem5  25971  lgsdir  26015  lgs1  26024  lgsquad2lem2  26068  addsqn2reu  26124  addsqrexnreu  26125  dchrmusumlema  26176  dchrisum0lema  26197  trkgstr  26337  ttgbas  26770  ttgplusg  26771  ttgvsca  26773  eengstr  26873  baseltedgf  26886  usgrexmplef  27148  lfgrn1cycl  27690  clwwlkn1  27925  ipval2  28589  opsqrlem2  30023  ssnnssfz  30632  nnindf  30657  nn0min  30658  isarchi3  30967  resvbas  31057  rge0scvg  31420  zlmds  31433  qqh0  31453  qqh1  31454  esumfzf  31556  esumfsup  31557  esumpcvgval  31565  voliune  31716  eulerpartgbij  31858  eulerpartlemgs2  31866  fib2  31888  rrvsum  31940  ballotlem4  31984  ballotlemi1  31988  ballotlemii  31989  ballotlemic  31992  ballotlem1c  31993  hgt750lem  32150  hgt750leme  32157  0nn0m1nnn0  32579  faclimlem1  33224  nn0prpwlem  34060  nn0prpw  34061  bj-endbase  35010  poimirlem32  35369  ovoliunnfl  35379  voliunnfl  35381  volsupnfl  35382  incsequz  35466  bfplem1  35540  rrncmslem  35550  hlhilsbase  39515  60gcd7e1  39572  12lcm5e60  39575  60lcm7e420  39577  lcm1un  39580  lcmineqlem10  39605  3lexlogpow5ineq1  39621  3lexlogpow5ineq2  39622  3lexlogpow5ineq4  39623  aks4d1p1p7  39640  nnmulcom  39804  3cubes  40004  jm2.23  40310  rmydioph  40328  rmxdioph  40330  expdiophlem2  40336  expdioph  40337  relexp2  40751  iunrelexpmin1  40782  iunrelexpmin2  40786  dftrcl3  40794  fvtrcllb1d  40796  cotrcltrcl  40799  corcltrcl  40813  cotrclrcl  40816  mnringbased  41296  prmunb2  41388  sumsnd  42028  nnn0  42379  xrralrecnnge  42393  iooiinicc  42545  iooiinioc  42559  mccl  42606  sumnnodd  42638  wallispilem4  43076  wallispi2lem1  43079  wallispi2lem2  43080  stirlinglem8  43089  stirlinglem11  43092  stirlinglem12  43093  stirlinglem13  43094  fourierdlem31  43146  nnfoctbdjlem  43460  hoicvr  43553  hoicvrrex  43561  hoidmvlelem3  43602  ovnhoilem1  43606  ovnhoilem2  43607  ovnlecvr2  43615  ovnsubadd2lem  43650  iinhoiicclem  43678  vonicclem2  43689  iccpartlt  44309  257prm  44446  fmtnoprmfac2lem1  44451  fmtno4prmfac193  44458  fmtno4nprmfac193  44459  fmtno5nprm  44468  3ndvds4  44480  139prmALT  44481  31prm  44482  127prm  44484  3exp4mod41  44501  41prothprmlem2  44503  perfectALTVlem1  44606  perfectALTVlem2  44607  2exp340mod341  44618  341fppr2  44619  4fppr1  44620  nnsum3primesprm  44675  bgoldbtbndlem1  44690  tgblthelfgott  44700  nnsgrpmgm  44803  nnsgrpnmnd  44805  blennn0elnn  45356  blen1  45363  ackval42  45475