Theorem 1nn 12204

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 11177	. . . 4 ⊢ 1 ∈ V
2		fr0g 8407	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8406	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7868	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7055	. . . 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 2826	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12194	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5654	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2753	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2828	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3450  ∅c0 4299   ↦ cmpt 5191  ran crn 5642   ↾ cres 5643   “ cima 5644   Fn wfn 6509  ‘cfv 6514  (class class class)co 7390  ωcom 7845  reccrdg 8380  1c1 11076   + caddc 11078  ℕcn 12193

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390  ax-un 7714  ax-1cn 11133

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2534  df-eu 2563  df-clab 2709  df-cleq 2722  df-clel 2804  df-nfc 2879  df-ne 2927  df-ral 3046  df-rex 3055  df-reu 3357  df-rab 3409  df-v 3452  df-sbc 3757  df-csb 3866  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-pss 3937  df-nul 4300  df-if 4492  df-pw 4568  df-sn 4593  df-pr 4595  df-op 4599  df-uni 4875  df-iun 4960  df-br 5111  df-opab 5173  df-mpt 5192  df-tr 5218  df-id 5536  df-eprel 5541  df-po 5549  df-so 5550  df-fr 5594  df-we 5596  df-xp 5647  df-rel 5648  df-cnv 5649  df-co 5650  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654  df-pred 6277  df-ord 6338  df-on 6339  df-lim 6340  df-suc 6341  df-iota 6467  df-fun 6516  df-fn 6517  df-f 6518  df-f1 6519  df-fo 6520  df-f1o 6521  df-fv 6522  df-ov 7393  df-om 7846  df-2nd 7972  df-frecs 8263  df-wrecs 8294  df-recs 8343  df-rdg 8381  df-nn 12194

This theorem is referenced by:  dfnn2  12206  dfnn3  12207  nnind  12211  nn1suc  12215  2nn  12266  nnunb  12445  1nn0  12465  nn0p1nn  12488  elz2  12554  1z  12570  neg1z  12576  nneo  12625  9p1e10  12658  elnn1uz2  12891  zq  12920  rpnnen1lem4  12946  rpnnen1lem5  12947  1elfzo1  13682  ser1const  14030  exp1  14039  nnexpcl  14046  expnbnd  14204  fac1  14249  faccl  14255  faclbnd3  14264  faclbnd4lem1  14265  faclbnd4lem2  14266  faclbnd4lem3  14267  faclbnd4lem4  14268  lsw0  14537  ccat2s1p1  14601  cats1un  14693  revs1  14737  cats1fvn  14831  relexpsucnnl  15003  relexpaddg  15026  isercolllem2  15639  isercolllem3  15640  isercoll  15641  sumsnf  15716  climcndslem1  15822  climcndslem2  15823  fprodnncl  15928  prodsn  15935  prodsnf  15937  nnrisefaccl  15992  eftlub  16084  eirrlem  16179  rpnnen2lem5  16193  rpnnen2lem8  16196  rpnnen2lem12  16200  dvdsle  16287  ndvdsp1  16388  5ndvds6  16391  gcd1  16505  bezoutr1  16546  1nprm  16656  1idssfct  16657  isprm2lem  16658  qden1elz  16734  phi1  16750  phiprm  16754  pcpre1  16820  pczpre  16825  pcmptcl  16869  pcmpt  16870  infpnlem2  16889  prmreclem1  16894  prmreclem6  16899  mul4sq  16932  vdwmc2  16957  vdwlem8  16966  vdwlem13  16971  vdwnnlem3  16975  prmocl  17012  prmop1  17016  fvprmselelfz  17022  fvprmselgcd1  17023  prmolefac  17024  prmodvdslcmf  17025  prmgapprmo  17040  5prm  17086  7prm  17088  11prm  17092  13prm  17093  17prm  17094  19prm  17095  37prm  17098  43prm  17099  83prm  17100  139prm  17101  163prm  17102  317prm  17103  631prm  17104  1259lem4  17111  1259lem5  17112  1259prm  17113  2503lem3  17116  2503prm  17117  4001lem1  17118  4001lem2  17119  4001lem3  17120  4001lem4  17121  4001prm  17122  baseid  17189  basendx  17195  basendxnn  17196  rngstr  17268  lmodstr  17295  topgrpstr  17331  otpsstr  17346  ocndx  17351  ocid  17352  basendxnocndx  17353  plendxnocndx  17354  basendxltdsndx  17358  dsndxnplusgndx  17360  dsndxnmulrndx  17361  slotsdnscsi  17362  dsndxntsetndx  17363  slotsdifdsndx  17364  basendxltunifndx  17368  unifndxntsetndx  17370  slotsdifunifndx  17371  slotsbhcdif  17385  slotsdifocndx  17387  catstr  17929  ipostr  18495  mulgfval  19008  mulg1  19020  mulg2  19022  od1  19496  0subgALT  19505  gex1  19528  efgsval2  19670  efgsp1  19674  torsubg  19791  pgpfaclem1  20020  pmatcollpw3fi1lem2  22681  hauspwdom  23395  imasdsf1olem  24268  cphipval  25150  bcthlem4  25234  bcth3  25238  ovolmge0  25385  ovollb2  25397  ovolctb  25398  ovolunlem1a  25404  ovolunlem1  25405  ovoliunlem1  25410  ovoliun  25413  ovoliun2  25414  ovolicc1  25424  voliunlem1  25458  volsup  25464  ioombl1lem2  25467  ioombl1lem4  25469  uniioombllem1  25489  uniioombllem2  25491  uniioombllem6  25496  itg1climres  25622  itg2seq  25650  itg2monolem1  25658  itg2monolem2  25659  itg2monolem3  25660  itg2mono  25661  itg2i1fseq2  25664  itg2cnlem1  25669  aalioulem5  26251  aaliou2b  26256  aaliou3lem4  26261  aaliou3lem7  26264  log2ub  26866  emcllem6  26918  emcllem7  26919  lgam1  26981  gam1  26982  ftalem7  26996  efnnfsumcl  27020  vmaprm  27034  efvmacl  27037  efchtdvds  27076  vma1  27083  prmorcht  27095  sqff1o  27099  pclogsum  27133  perfectlem1  27147  perfectlem2  27148  bpos1  27201  bposlem5  27206  lgsdir  27250  lgs1  27259  lgsquad2lem2  27303  addsqn2reu  27359  addsqrexnreu  27360  dchrmusumlema  27411  dchrisum0lema  27432  slotsinbpsd  28375  slotslnbpsd  28376  trkgstr  28378  eengstr  28914  basendxltedgfndx  28928  usgrexmplef  29193  lfgrn1cycl  29742  clwwlkn1  29977  ipval2  30643  opsqrlem2  32077  ssnnssfz  32717  znumd  32744  zdend  32745  nnindf  32751  nn0min  32752  isarchi3  33148  eufndx  33247  eufid  33248  constrext2chnlem  33747  iconstr  33763  rge0scvg  33946  qqh0  33981  qqh1  33982  esumfzf  34066  esumfsup  34067  esumpcvgval  34075  voliune  34226  eulerpartgbij  34370  eulerpartlemgs2  34378  fib2  34400  rrvsum  34452  ballotlem4  34497  ballotlemi1  34501  ballotlemii  34502  ballotlemic  34505  ballotlem1c  34506  hgt750lem  34649  hgt750leme  34656  0nn0m1nnn0  35107  faclimlem1  35737  nn0prpwlem  36317  nn0prpw  36318  poimirlem32  37653  ovoliunnfl  37663  voliunnfl  37665  volsupnfl  37666  incsequz  37749  bfplem1  37823  rrncmslem  37833  60gcd7e1  42000  12lcm5e60  42003  60lcm7e420  42005  lcm1un  42008  lcmineqlem10  42033  3lexlogpow5ineq1  42049  3lexlogpow5ineq2  42050  3lexlogpow5ineq4  42051  aks4d1p1p7  42069  aks6d1c1p8  42110  sticksstones9  42149  sticksstones11  42151  aks6d1c7lem1  42175  nnmulcom  42267  3cubes  42685  jm2.23  42992  rmydioph  43010  rmxdioph  43012  expdiophlem2  43018  expdioph  43019  relexp2  43673  iunrelexpmin1  43704  iunrelexpmin2  43708  dftrcl3  43716  fvtrcllb1d  43718  cotrcltrcl  43721  corcltrcl  43735  cotrclrcl  43738  prmunb2  44307  sumsnd  45027  nnn0  45381  xrralrecnnge  45393  iooiinicc  45547  iooiinioc  45561  mccl  45603  sumnnodd  45635  wallispilem4  46073  wallispi2lem1  46076  wallispi2lem2  46077  stirlinglem8  46086  stirlinglem11  46089  stirlinglem12  46090  stirlinglem13  46091  fourierdlem31  46143  nnfoctbdjlem  46460  hoicvr  46553  hoicvrrex  46561  hoidmvlelem3  46602  ovnhoilem1  46606  ovnhoilem2  46607  ovnlecvr2  46615  ovnsubadd2lem  46650  iinhoiicclem  46678  vonicclem2  46689  1elfzo1ceilhalf1  47342  iccpartlt  47429  257prm  47566  fmtnoprmfac2lem1  47571  fmtno4prmfac193  47578  fmtno4nprmfac193  47579  fmtno5nprm  47588  3ndvds4  47600  139prmALT  47601  31prm  47602  127prm  47604  3exp4mod41  47621  41prothprmlem2  47623  perfectALTVlem1  47726  perfectALTVlem2  47727  2exp340mod341  47738  341fppr2  47739  4fppr1  47740  nnsum3primesprm  47795  bgoldbtbndlem1  47810  tgblthelfgott  47820  nnsgrpmgm  48168  nnsgrpnmnd  48170  blennn0elnn  48570  blen1  48577  ackval42  48689