Theorem 1nn 12197

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 11170	. . . 4 ⊢ 1 ∈ V
2		fr0g 8404	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8403	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7865	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7052	. . . 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 2825	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12187	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5651	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2752	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2827	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1540   ∈ wcel 2109  Vcvv 3447  ∅c0 4296   ↦ cmpt 5188  ran crn 5639   ↾ cres 5640   “ cima 5641   Fn wfn 6506  ‘cfv 6511  (class class class)co 7387  ωcom 7842  reccrdg 8377  1c1 11069   + caddc 11071  ℕcn 12186

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 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387  ax-un 7711  ax-1cn 11126

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 2533  df-eu 2562  df-clab 2708  df-cleq 2721  df-clel 2803  df-nfc 2878  df-ne 2926  df-ral 3045  df-rex 3054  df-reu 3355  df-rab 3406  df-v 3449  df-sbc 3754  df-csb 3863  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-pss 3934  df-nul 4297  df-if 4489  df-pw 4565  df-sn 4590  df-pr 4592  df-op 4596  df-uni 4872  df-iun 4957  df-br 5108  df-opab 5170  df-mpt 5189  df-tr 5215  df-id 5533  df-eprel 5538  df-po 5546  df-so 5547  df-fr 5591  df-we 5593  df-xp 5644  df-rel 5645  df-cnv 5646  df-co 5647  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651  df-pred 6274  df-ord 6335  df-on 6336  df-lim 6337  df-suc 6338  df-iota 6464  df-fun 6513  df-fn 6514  df-f 6515  df-f1 6516  df-fo 6517  df-f1o 6518  df-fv 6519  df-ov 7390  df-om 7843  df-2nd 7969  df-frecs 8260  df-wrecs 8291  df-recs 8340  df-rdg 8378  df-nn 12187

This theorem is referenced by:  dfnn2  12199  dfnn3  12200  nnind  12204  nn1suc  12208  2nn  12259  nnunb  12438  1nn0  12458  nn0p1nn  12481  elz2  12547  1z  12563  neg1z  12569  nneo  12618  9p1e10  12651  elnn1uz2  12884  zq  12913  rpnnen1lem4  12939  rpnnen1lem5  12940  1elfzo1  13675  ser1const  14023  exp1  14032  nnexpcl  14039  expnbnd  14197  fac1  14242  faccl  14248  faclbnd3  14257  faclbnd4lem1  14258  faclbnd4lem2  14259  faclbnd4lem3  14260  faclbnd4lem4  14261  lsw0  14530  ccat2s1p1  14594  cats1un  14686  revs1  14730  cats1fvn  14824  relexpsucnnl  14996  relexpaddg  15019  isercolllem2  15632  isercolllem3  15633  isercoll  15634  sumsnf  15709  climcndslem1  15815  climcndslem2  15816  fprodnncl  15921  prodsn  15928  prodsnf  15930  nnrisefaccl  15985  eftlub  16077  eirrlem  16172  rpnnen2lem5  16186  rpnnen2lem8  16189  rpnnen2lem12  16193  dvdsle  16280  ndvdsp1  16381  5ndvds6  16384  gcd1  16498  bezoutr1  16539  1nprm  16649  1idssfct  16650  isprm2lem  16651  qden1elz  16727  phi1  16743  phiprm  16747  pcpre1  16813  pczpre  16818  pcmptcl  16862  pcmpt  16863  infpnlem2  16882  prmreclem1  16887  prmreclem6  16892  mul4sq  16925  vdwmc2  16950  vdwlem8  16959  vdwlem13  16964  vdwnnlem3  16968  prmocl  17005  prmop1  17009  fvprmselelfz  17015  fvprmselgcd1  17016  prmolefac  17017  prmodvdslcmf  17018  prmgapprmo  17033  5prm  17079  7prm  17081  11prm  17085  13prm  17086  17prm  17087  19prm  17088  37prm  17091  43prm  17092  83prm  17093  139prm  17094  163prm  17095  317prm  17096  631prm  17097  1259lem4  17104  1259lem5  17105  1259prm  17106  2503lem3  17109  2503prm  17110  4001lem1  17111  4001lem2  17112  4001lem3  17113  4001lem4  17114  4001prm  17115  baseid  17182  basendx  17188  basendxnn  17189  rngstr  17261  lmodstr  17288  topgrpstr  17324  otpsstr  17339  ocndx  17344  ocid  17345  basendxnocndx  17346  plendxnocndx  17347  basendxltdsndx  17351  dsndxnplusgndx  17353  dsndxnmulrndx  17354  slotsdnscsi  17355  dsndxntsetndx  17356  slotsdifdsndx  17357  basendxltunifndx  17361  unifndxntsetndx  17363  slotsdifunifndx  17364  slotsbhcdif  17378  slotsdifocndx  17380  catstr  17922  ipostr  18488  mulgfval  19001  mulg1  19013  mulg2  19015  od1  19489  0subgALT  19498  gex1  19521  efgsval2  19663  efgsp1  19667  torsubg  19784  pgpfaclem1  20013  pmatcollpw3fi1lem2  22674  hauspwdom  23388  imasdsf1olem  24261  cphipval  25143  bcthlem4  25227  bcth3  25231  ovolmge0  25378  ovollb2  25390  ovolctb  25391  ovolunlem1a  25397  ovolunlem1  25398  ovoliunlem1  25403  ovoliun  25406  ovoliun2  25407  ovolicc1  25417  voliunlem1  25451  volsup  25457  ioombl1lem2  25460  ioombl1lem4  25462  uniioombllem1  25482  uniioombllem2  25484  uniioombllem6  25489  itg1climres  25615  itg2seq  25643  itg2monolem1  25651  itg2monolem2  25652  itg2monolem3  25653  itg2mono  25654  itg2i1fseq2  25657  itg2cnlem1  25662  aalioulem5  26244  aaliou2b  26249  aaliou3lem4  26254  aaliou3lem7  26257  log2ub  26859  emcllem6  26911  emcllem7  26912  lgam1  26974  gam1  26975  ftalem7  26989  efnnfsumcl  27013  vmaprm  27027  efvmacl  27030  efchtdvds  27069  vma1  27076  prmorcht  27088  sqff1o  27092  pclogsum  27126  perfectlem1  27140  perfectlem2  27141  bpos1  27194  bposlem5  27199  lgsdir  27243  lgs1  27252  lgsquad2lem2  27296  addsqn2reu  27352  addsqrexnreu  27353  dchrmusumlema  27404  dchrisum0lema  27425  slotsinbpsd  28368  slotslnbpsd  28369  trkgstr  28371  eengstr  28907  basendxltedgfndx  28921  usgrexmplef  29186  lfgrn1cycl  29735  clwwlkn1  29970  ipval2  30636  opsqrlem2  32070  ssnnssfz  32710  znumd  32737  zdend  32738  nnindf  32744  nn0min  32745  isarchi3  33141  eufndx  33240  eufid  33241  constrext2chnlem  33740  iconstr  33756  rge0scvg  33939  qqh0  33974  qqh1  33975  esumfzf  34059  esumfsup  34060  esumpcvgval  34068  voliune  34219  eulerpartgbij  34363  eulerpartlemgs2  34371  fib2  34393  rrvsum  34445  ballotlem4  34490  ballotlemi1  34494  ballotlemii  34495  ballotlemic  34498  ballotlem1c  34499  hgt750lem  34642  hgt750leme  34649  0nn0m1nnn0  35100  faclimlem1  35730  nn0prpwlem  36310  nn0prpw  36311  poimirlem32  37646  ovoliunnfl  37656  voliunnfl  37658  volsupnfl  37659  incsequz  37742  bfplem1  37816  rrncmslem  37826  60gcd7e1  41993  12lcm5e60  41996  60lcm7e420  41998  lcm1un  42001  lcmineqlem10  42026  3lexlogpow5ineq1  42042  3lexlogpow5ineq2  42043  3lexlogpow5ineq4  42044  aks4d1p1p7  42062  aks6d1c1p8  42103  sticksstones9  42142  sticksstones11  42144  aks6d1c7lem1  42168  nnmulcom  42260  3cubes  42678  jm2.23  42985  rmydioph  43003  rmxdioph  43005  expdiophlem2  43011  expdioph  43012  relexp2  43666  iunrelexpmin1  43697  iunrelexpmin2  43701  dftrcl3  43709  fvtrcllb1d  43711  cotrcltrcl  43714  corcltrcl  43728  cotrclrcl  43731  prmunb2  44300  sumsnd  45020  nnn0  45374  xrralrecnnge  45386  iooiinicc  45540  iooiinioc  45554  mccl  45596  sumnnodd  45628  wallispilem4  46066  wallispi2lem1  46069  wallispi2lem2  46070  stirlinglem8  46079  stirlinglem11  46082  stirlinglem12  46083  stirlinglem13  46084  fourierdlem31  46136  nnfoctbdjlem  46453  hoicvr  46546  hoicvrrex  46554  hoidmvlelem3  46595  ovnhoilem1  46599  ovnhoilem2  46600  ovnlecvr2  46608  ovnsubadd2lem  46643  iinhoiicclem  46671  vonicclem2  46682  1elfzo1ceilhalf1  47338  iccpartlt  47425  257prm  47562  fmtnoprmfac2lem1  47567  fmtno4prmfac193  47574  fmtno4nprmfac193  47575  fmtno5nprm  47584  3ndvds4  47596  139prmALT  47597  31prm  47598  127prm  47600  3exp4mod41  47617  41prothprmlem2  47619  perfectALTVlem1  47722  perfectALTVlem2  47723  2exp340mod341  47734  341fppr2  47735  4fppr1  47736  nnsum3primesprm  47791  bgoldbtbndlem1  47806  tgblthelfgott  47816  nnsgrpmgm  48164  nnsgrpnmnd  48166  blennn0elnn  48566  blen1  48573  ackval42  48685