Theorem 1nn 11984

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 10971	. . . 4 ⊢ 1 ∈ V
2		fr0g 8267	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8266	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7735	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 6958	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 689	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2836	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 11974	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5602	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2766	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2838	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1539   ∈ wcel 2106  Vcvv 3432  ∅c0 4256   ↦ cmpt 5157  ran crn 5590   ↾ cres 5591   “ cima 5592   Fn wfn 6428  ‘cfv 6433  (class class class)co 7275  ωcom 7712  reccrdg 8240  1c1 10872   + caddc 10874  ℕcn 11973

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352  ax-un 7588  ax-1cn 10929

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3or 1087  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-reu 3072  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-pss 3906  df-nul 4257  df-if 4460  df-pw 4535  df-sn 4562  df-pr 4564  df-op 4568  df-uni 4840  df-iun 4926  df-br 5075  df-opab 5137  df-mpt 5158  df-tr 5192  df-id 5489  df-eprel 5495  df-po 5503  df-so 5504  df-fr 5544  df-we 5546  df-xp 5595  df-rel 5596  df-cnv 5597  df-co 5598  df-dm 5599  df-rn 5600  df-res 5601  df-ima 5602  df-pred 6202  df-ord 6269  df-on 6270  df-lim 6271  df-suc 6272  df-iota 6391  df-fun 6435  df-fn 6436  df-f 6437  df-f1 6438  df-fo 6439  df-f1o 6440  df-fv 6441  df-ov 7278  df-om 7713  df-2nd 7832  df-frecs 8097  df-wrecs 8128  df-recs 8202  df-rdg 8241  df-nn 11974

This theorem is referenced by:  dfnn2  11986  dfnn3  11987  nnind  11991  nn1suc  11995  2nn  12046  nnunb  12229  1nn0  12249  nn0p1nn  12272  elz2  12337  1z  12350  neg1z  12356  nneo  12404  9p1e10  12439  elnn1uz2  12665  zq  12694  rpnnen1lem4  12720  rpnnen1lem5  12721  ser1const  13779  exp1  13788  nnexpcl  13795  expnbnd  13947  fac1  13991  faccl  13997  faclbnd3  14006  faclbnd4lem1  14007  faclbnd4lem2  14008  faclbnd4lem3  14009  faclbnd4lem4  14010  lsw0  14268  ccat2s1p1  14336  ccat2s1p1OLD  14338  cats1un  14434  revs1  14478  cats1fvn  14571  relexpsucnnl  14741  relexpaddg  14764  isercolllem2  15377  isercolllem3  15378  isercoll  15379  sumsnf  15455  climcndslem1  15561  climcndslem2  15562  fprodnncl  15665  prodsn  15672  prodsnf  15674  nnrisefaccl  15729  eftlub  15818  eirrlem  15913  rpnnen2lem5  15927  rpnnen2lem8  15930  rpnnen2lem12  15934  dvdsle  16019  ndvdsp1  16120  gcd1  16235  bezoutr1  16274  1nprm  16384  1idssfct  16385  isprm2lem  16386  qden1elz  16461  phi1  16474  phiprm  16478  pcpre1  16543  pczpre  16548  pcmptcl  16592  pcmpt  16593  infpnlem2  16612  prmreclem1  16617  prmreclem6  16622  mul4sq  16655  vdwmc2  16680  vdwlem8  16689  vdwlem13  16694  vdwnnlem3  16698  prmocl  16735  prmop1  16739  fvprmselelfz  16745  fvprmselgcd1  16746  prmolefac  16747  prmodvdslcmf  16748  prmgapprmo  16763  5prm  16810  7prm  16812  11prm  16816  13prm  16817  17prm  16818  19prm  16819  37prm  16822  43prm  16823  83prm  16824  139prm  16825  163prm  16826  317prm  16827  631prm  16828  1259lem4  16835  1259lem5  16836  1259prm  16837  2503lem3  16840  2503prm  16841  4001lem1  16842  4001lem2  16843  4001lem3  16844  4001lem4  16845  4001prm  16846  baseid  16915  basendx  16921  basendxnn  16922  basendxnnOLD  16923  1strstr  16927  2strstr  16934  ressval3dOLD  16957  basendxnplusgndxOLD  16993  basendxnmulrndxOLD  17006  rngstr  17008  lmodstr  17035  topgrpstr  17071  otpsstr  17086  ocndx  17091  ocid  17092  basendxnocndx  17093  plendxnocndx  17094  basendxltdsndx  17098  dsndxnplusgndx  17100  dsndxnmulrndx  17101  slotsdnscsi  17102  dsndxntsetndx  17103  slotsdifdsndx  17104  basendxltunifndx  17108  unifndxntsetndx  17110  slotsdifunifndx  17111  slotsbhcdif  17125  slotsbhcdifOLD  17126  slotsdifocndx  17128  oppcbasOLD  17429  rescbasOLD  17542  rescabsOLD  17548  catstr  17674  estrreslem1OLD  17854  ipostr  18247  mulgfval  18702  mulg1  18711  mulg2  18713  oppgbasOLD  18957  symgvalstructOLD  19005  od1  19166  gex1  19196  efgsval2  19339  efgsp1  19343  torsubg  19455  pgpfaclem1  19684  mgpbasOLD  19727  mgpdsOLD  19734  opprbasOLD  19870  rmodislmodOLD  20192  srabaseOLD  20442  sradsOLD  20456  cnfldfunALTOLD  20611  zlmbasOLD  20721  znbas2OLD  20745  thlbasOLD  20902  thlleOLD  20904  opsrbasOLD  21253  pmatcollpw3fi1lem2  21936  hauspwdom  22652  tuslemOLD  23419  imasdsf1olem  23526  setsmsdsOLD  23631  tmslemOLD  23638  tnglemOLD  23797  tngbasOLD  23799  tngdsOLD  23812  cphipval  24407  bcthlem4  24491  bcth3  24495  ovolmge0  24641  ovollb2  24653  ovolctb  24654  ovolunlem1a  24660  ovolunlem1  24661  ovoliunlem1  24666  ovoliun  24669  ovoliun2  24670  ovolicc1  24680  voliunlem1  24714  volsup  24720  ioombl1lem2  24723  ioombl1lem4  24725  uniioombllem1  24745  uniioombllem2  24747  uniioombllem6  24752  itg1climres  24879  itg2seq  24907  itg2monolem1  24915  itg2monolem2  24916  itg2monolem3  24917  itg2mono  24918  itg2i1fseq2  24921  itg2cnlem1  24926  aalioulem5  25496  aaliou2b  25501  aaliou3lem4  25506  aaliou3lem7  25509  log2ub  26099  emcllem6  26150  emcllem7  26151  lgam1  26213  gam1  26214  ftalem7  26228  efnnfsumcl  26252  vmaprm  26266  efvmacl  26269  efchtdvds  26308  vma1  26315  prmorcht  26327  sqff1o  26331  pclogsum  26363  perfectlem1  26377  perfectlem2  26378  bpos1  26431  bposlem5  26436  lgsdir  26480  lgs1  26489  lgsquad2lem2  26533  addsqn2reu  26589  addsqrexnreu  26590  dchrmusumlema  26641  dchrisum0lema  26662  slotsinbpsd  26802  slotslnbpsd  26803  trkgstr  26805  ttgbasOLD  27241  ttgplusgOLD  27243  ttgvscaOLD  27246  eengstr  27348  basendxltedgfndx  27363  baseltedgfOLD  27364  usgrexmplef  27626  lfgrn1cycl  28170  clwwlkn1  28405  ipval2  29069  opsqrlem2  30503  ssnnssfz  31108  nnindf  31133  nn0min  31134  isarchi3  31441  resvbasOLD  31533  rge0scvg  31899  zlmdsOLD  31913  qqh0  31934  qqh1  31935  esumfzf  32037  esumfsup  32038  esumpcvgval  32046  voliune  32197  eulerpartgbij  32339  eulerpartlemgs2  32347  fib2  32369  rrvsum  32421  ballotlem4  32465  ballotlemi1  32469  ballotlemii  32470  ballotlemic  32473  ballotlem1c  32474  hgt750lem  32631  hgt750leme  32638  0nn0m1nnn0  33071  faclimlem1  33709  nn0prpwlem  34511  nn0prpw  34512  poimirlem32  35809  ovoliunnfl  35819  voliunnfl  35821  volsupnfl  35822  incsequz  35906  bfplem1  35980  rrncmslem  35990  hlhilsbaseOLD  39955  60gcd7e1  40013  12lcm5e60  40016  60lcm7e420  40018  lcm1un  40021  lcmineqlem10  40046  3lexlogpow5ineq1  40062  3lexlogpow5ineq2  40063  3lexlogpow5ineq4  40064  aks4d1p1p7  40082  sticksstones9  40110  sticksstones11  40112  nnmulcom  40302  3cubes  40512  jm2.23  40818  rmydioph  40836  rmxdioph  40838  expdiophlem2  40844  expdioph  40845  relexp2  41285  iunrelexpmin1  41316  iunrelexpmin2  41320  dftrcl3  41328  fvtrcllb1d  41330  cotrcltrcl  41333  corcltrcl  41347  cotrclrcl  41350  mnringbasedOLD  41830  prmunb2  41929  sumsnd  42569  nnn0  42917  xrralrecnnge  42930  iooiinicc  43080  iooiinioc  43094  mccl  43139  sumnnodd  43171  wallispilem4  43609  wallispi2lem1  43612  wallispi2lem2  43613  stirlinglem8  43622  stirlinglem11  43625  stirlinglem12  43626  stirlinglem13  43627  fourierdlem31  43679  nnfoctbdjlem  43993  hoicvr  44086  hoicvrrex  44094  hoidmvlelem3  44135  ovnhoilem1  44139  ovnhoilem2  44140  ovnlecvr2  44148  ovnsubadd2lem  44183  iinhoiicclem  44211  vonicclem2  44222  iccpartlt  44876  257prm  45013  fmtnoprmfac2lem1  45018  fmtno4prmfac193  45025  fmtno4nprmfac193  45026  fmtno5nprm  45035  3ndvds4  45047  139prmALT  45048  31prm  45049  127prm  45051  3exp4mod41  45068  41prothprmlem2  45070  perfectALTVlem1  45173  perfectALTVlem2  45174  2exp340mod341  45185  341fppr2  45186  4fppr1  45187  nnsum3primesprm  45242  bgoldbtbndlem1  45257  tgblthelfgott  45267  nnsgrpmgm  45370  nnsgrpnmnd  45372  blennn0elnn  45923  blen1  45930  ackval42  46042