Theorem 1nn 12386

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 11342	. . . 4 ⊢ 1 ∈ V
2		fr0g 8482	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8481	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7934	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7112	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 705	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2861	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12376	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5671	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2786	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2863	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   = wceq 1570   ∈ wcel 2147  Vcvv 3454  ∅c0 4281   ↦ cmpt 5192  ran crn 5659   ↾ cres 5660   “ cima 5661   Fn wfn 6561  ‘cfv 6566  (class class class)co 7451  ωcom 7911  reccrdg 8455  1c1 11240   + caddc 11242  ℕcn 12375

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5255  ax-nul 5266  ax-pr 5398  ax-un 7783  ax-1cn 11297

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-reu 3370  df-rab 3417  df-v 3456  df-sbc 3743  df-csb 3852  df-ss 3901  df-pss 4017  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-pw 4562  df-sn 4589  df-pr 4591  df-op 4841  df-uni 4873  df-iun 4958  df-br 5109  df-opab 5174  df-mpt 5193  df-tr 5219  df-id 5553  df-eprel 5558  df-po 5566  df-so 5567  df-fr 5611  df-we 5613  df-xp 5664  df-rel 5665  df-cnv 5666  df-co 5667  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671  df-pred 6330  df-ord 6391  df-on 6392  df-lim 6393  df-suc 6394  df-iota 6520  df-fun 6568  df-fn 6569  df-f 6570  df-f1 6571  df-fo 6572  df-f1o 6573  df-fv 6574  df-ov 7454  df-om 7912  df-2nd 8036  df-frecs 8337  df-wrecs 8368  df-recs 8417  df-rdg 8456  df-nn 12376

This theorem is used by:  dfnn2  12388  dfnn3  12389  nnind  12393  nn1suc  12397  nnmulcom  12436  2nn  12456  nnunb  12642  1nn0  12662  nn0p1nn  12685  elz2  12751  1z  12766  neg1z  12772  0nn0m1nnn0  12793  nneo  12823  9p1e10  12856  11nn  12879  elnn1uz2  13092  zq  13121  rpnnen1lem4  13148  rpnnen1lem5  13149  1elfzo1  13889  ser1const  14241  exp1  14250  nnexpcl  14257  expnbnd  14417  fac1  14462  faccl  14468  faclbnd3  14477  faclbnd4lem1  14478  faclbnd4lem2  14479  faclbnd4lem3  14480  faclbnd4lem4  14481  lsw0  14751  ccat2s1p1  14819  cats1un  14912  revs1  14956  cats1fvn  15051  relexpsucnnl  15226  relexpaddg  15249  isercolllem2  15877  isercolllem3  15878  isercoll  15879  sumsnf  15953  climcndslem1  16062  climcndslem2  16063  fprodnncl  16166  prodsn  16173  prodsnf  16175  nnrisefaccl  16230  eftlub  16321  eirrlem  16416  rpnnen2lem5  16430  rpnnen2lem8  16433  rpnnen2lem12  16437  dvdsle  16524  ndvdsp1  16625  5ndvds6  16628  gcd1  16745  bezoutr1  16788  1nprm  16898  1idssfct  16899  isprm2lem  16900  qden1elz  16977  phi1  16994  phiprm  16998  pcpre1  17064  pczpre  17069  pcmptcl  17113  pcmpt  17114  infpnlem2  17133  prmreclem1  17138  prmreclem6  17143  mul4sq  17176  vdwmc2  17201  vdwlem8  17210  vdwlem13  17215  vdwnnlem3  17219  prmocl  17256  prmop1  17260  fvprmselelfz  17266  fvprmselgcd1  17267  prmolefac  17268  prmodvdslcmf  17269  prmgapprmo  17284  5prm  17330  7prm  17332  10nprm  17335  11prm  17337  13prm  17338  17prm  17339  19prm  17340  37prm  17343  43prm  17344  83prm  17345  139prm  17346  163prm  17347  317prm  17348  631prm  17349  1259lem4  17356  1259lem5  17357  1259prm  17358  2503lem3  17361  2503prm  17362  4001lem1  17363  4001lem2  17364  4001lem3  17365  4001lem4  17366  4001prm  17367  baseid  17434  basendx  17440  basendxnn  17441  rngstr  17515  lmodstr  17542  topgrpstr  17578  otpsstr  17593  ocndx  17598  ocid  17599  basendxnocndx  17600  plendxnocndx  17601  basendxltdsndx  17605  dsndxnplusgndx  17607  dsndxnmulrndx  17608  slotsdnscsi  17609  dsndxntsetndx  17610  slotsdifdsndx  17611  basendxltunifndx  17615  unifndxntsetndx  17617  slotsdifunifndx  17618  eufndx  17632  eufid  17633  slotsbhcdif  17636  slotsdifocndx  17638  catstr  18185  ipostr  18753  mulgfval  19329  mulg1  19341  mulg2  19343  od1  19824  0subgALT  19833  gex1  19856  efgsval2  19998  efgsp1  20002  torsubg  20119  pgpfaclem1  20348  cnfldstr  21731  pmatcollpw3fi1lem2  23160  hauspwdom  23875  imasdsf1olem  24747  cphipval  25619  bcthlem4  25703  bcth3  25707  ovolmge0  25853  ovollb2  25865  ovolctb  25866  ovolunlem1a  25872  ovolunlem1  25873  ovoliunlem1  25878  ovoliun  25881  ovoliun2  25882  ovolicc1  25892  voliunlem1  25926  volsup  25932  ioombl1lem2  25935  ioombl1lem4  25937  uniioombllem1  25957  uniioombllem2  25959  uniioombllem6  25964  itg1climres  26090  itg2seq  26118  itg2monolem1  26126  itg2monolem2  26127  itg2monolem3  26128  itg2mono  26129  itg2i1fseq2  26132  itg2cnlem1  26137  aalioulem5  26720  aaliou2b  26725  aaliou3lem4  26730  aaliou3lem7  26733  log2ub  27334  emcllem6  27385  emcllem7  27386  lgam1  27448  gam1  27449  ftalem7  27463  efnnfsumcl  27487  vmaprm  27501  efvmacl  27504  efchtdvds  27543  vma1  27550  prmorcht  27562  sqff1o  27566  pclogsum  27599  perfectlem1  27613  perfectlem2  27614  bpos1  27667  bposlem5  27672  lgsdir  27716  lgs1  27725  lgsquad2lem2  27769  addsqn2reu  27825  addsqrexnreu  27826  dchrmusumlema  27877  dchrisum0lema  27898  slotsinbpsd  28960  slotslnbpsd  28961  trkgstr  28963  angmgmlem  29452  angmgmbas  29455  eengstr  29615  basendxltedgfndx  29629  usgrexmplef  29897  lfgrn1cycl  30451  clwwlkn1  30689  ipval2  31366  opsqrlem2  32800  ssnnssfz  33475  znumd  33500  zdend  33501  nnindf  33507  nn0min  33508  isarchi3  33847  constrext2chnlem  34493  iconstr  34509  rge0scvg  34692  qqh0  34727  qqh1  34728  esumfzf  34812  esumfsup  34813  esumpcvgval  34821  voliune  34973  eulerpartgbij  35115  eulerpartlemgs2  35123  fib2  35145  rrvsum  35197  ballotlem4  35242  ballotlemi1  35246  ballotlemii  35247  ballotlemic  35250  ballotlem1c  35251  hgt750lem  35391  hgt750leme  35398  faclimlem1  36723  nn0prpwlem  37325  nn0prpw  37326  poimirlem32  38838  ovoliunnfl  38848  voliunnfl  38850  volsupnfl  38851  incsequz  38948  bfplem1  39022  rrncmslem  39032  60gcd7e1  43321  12lcm5e60  43324  60lcm7e420  43326  lcm1un  43329  lcmineqlem10  43354  3lexlogpow5ineq1  43370  3lexlogpow5ineq2  43371  aks4d1p1p7  43390  aks6d1c1p8  43431  sticksstones9  43470  sticksstones11  43472  aks6d1c7lem1  43496  3cubes  43966  jm2.23  44269  rmydioph  44287  rmxdioph  44289  expdiophlem2  44295  expdioph  44296  relexp2  44938  iunrelexpmin1  44969  iunrelexpmin2  44973  dftrcl3  44981  fvtrcllb1d  44983  cotrcltrcl  44986  corcltrcl  45000  cotrclrcl  45003  prmunb2  45556  sumsnd  46317  nnn0  46662  xrralrecnnge  46674  iooiinicc  46827  iooiinioc  46841  mccl  46883  sumnnodd  46915  wallispilem4  47351  wallispi2lem1  47354  wallispi2lem2  47355  stirlinglem8  47364  stirlinglem11  47367  stirlinglem12  47368  stirlinglem13  47369  fourierdlem31  47421  nnfoctbdjlem  47738  hoicvrrex  47839  hoidmvlelem3  47880  ovnhoilem1  47884  ovnhoilem2  47885  ovnlecvr2  47893  ovnsubadd2lem  47928  iinhoiicclem  47956  vonicclem2  47967  numtowerdt  48189  1elfzo1ceilhalf1  48684  iccpartlt  48779  257prm  48919  fmtnoprmfac2lem1  48924  fmtno4prmfac193  48931  fmtno4nprmfac193  48932  fmtno5nprm  48941  3ndvds4  48953  139prmALT  48954  31prm  48955  127prm  48957  3exp4mod41  48974  41prothprmlem2  48976  perfectALTVlem1  49092  perfectALTVlem2  49093  2exp340mod341  49104  341fppr2  49105  4fppr1  49106  nnsum3primesprm  49161  bgoldbtbndlem1  49176  tgblthelfgott  49186  nnsgrpmgm  49546  nnsgrpnmnd  49548  bru1  49750  blennn0elnn  50020  blen1  50027  ackval42  50139  1elfz13  51371  veronesevrowd  51407  veronesematrowd  51409  veroquadgsumlem  51411  veroquadmodzerod  51412  veroquadnolindfd  51413