Theorem 1nn 11636

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 10626	. . . 4 ⊢ 1 ∈ V
2		fr0g 8054	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8053	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7581	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 6825	. . . 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 2887	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 11626	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5532	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2821	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2889	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1538   ∈ wcel 2111  Vcvv 3441  ∅c0 4243   ↦ cmpt 5110  ran crn 5520   ↾ cres 5521   “ cima 5522   Fn wfn 6319  ‘cfv 6324  (class class class)co 7135  ωcom 7560  reccrdg 8028  1c1 10527   + caddc 10529  ℕcn 11625

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 2770  ax-sep 5167  ax-nul 5174  ax-pow 5231  ax-pr 5295  ax-un 7441  ax-1cn 10584

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ne 2988  df-ral 3111  df-rex 3112  df-reu 3113  df-rab 3115  df-v 3443  df-sbc 3721  df-csb 3829  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-pss 3900  df-nul 4244  df-if 4426  df-pw 4499  df-sn 4526  df-pr 4528  df-tp 4530  df-op 4532  df-uni 4801  df-iun 4883  df-br 5031  df-opab 5093  df-mpt 5111  df-tr 5137  df-id 5425  df-eprel 5430  df-po 5438  df-so 5439  df-fr 5478  df-we 5480  df-xp 5525  df-rel 5526  df-cnv 5527  df-co 5528  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532  df-pred 6116  df-ord 6162  df-on 6163  df-lim 6164  df-suc 6165  df-iota 6283  df-fun 6326  df-fn 6327  df-f 6328  df-f1 6329  df-fo 6330  df-f1o 6331  df-fv 6332  df-om 7561  df-wrecs 7930  df-recs 7991  df-rdg 8029  df-nn 11626

This theorem is referenced by:  dfnn2  11638  dfnn3  11639  nnind  11643  nn1suc  11647  2nn  11698  nnunb  11881  1nn0  11901  nn0p1nn  11924  elz2  11987  1z  12000  neg1z  12006  nneo  12054  9p1e10  12088  elnn1uz2  12313  zq  12342  rpnnen1lem4  12367  rpnnen1lem5  12368  ser1const  13422  exp1  13431  nnexpcl  13438  expnbnd  13589  fac1  13633  faccl  13639  faclbnd3  13648  faclbnd4lem1  13649  faclbnd4lem2  13650  faclbnd4lem3  13651  faclbnd4lem4  13652  lsw0  13908  ccat2s1p1  13976  ccat2s1p1OLD  13978  cats1un  14074  revs1  14118  cats1fvn  14211  relexpsucnnl  14381  relexpaddg  14404  isercolllem2  15014  isercolllem3  15015  isercoll  15016  sumsnf  15091  climcndslem1  15196  climcndslem2  15197  fprodnncl  15301  prodsn  15308  prodsnf  15310  nnrisefaccl  15365  eftlub  15454  eirrlem  15549  rpnnen2lem5  15563  rpnnen2lem8  15566  rpnnen2lem12  15570  dvdsle  15652  ndvdsp1  15752  gcd1  15866  bezoutr1  15903  1nprm  16013  1idssfct  16014  isprm2lem  16015  qden1elz  16087  phi1  16100  phiprm  16104  pcpre1  16169  pczpre  16174  pcmptcl  16217  pcmpt  16218  infpnlem2  16237  prmreclem1  16242  prmreclem6  16247  mul4sq  16280  vdwmc2  16305  vdwlem8  16314  vdwlem13  16319  vdwnnlem3  16323  prmocl  16360  prmop1  16364  fvprmselelfz  16370  fvprmselgcd1  16371  prmolefac  16372  prmodvdslcmf  16373  prmgapprmo  16388  5prm  16434  7prm  16436  11prm  16440  13prm  16441  17prm  16442  19prm  16443  37prm  16446  43prm  16447  83prm  16448  139prm  16449  163prm  16450  317prm  16451  631prm  16452  1259lem4  16459  1259lem5  16460  1259prm  16461  2503lem3  16464  2503prm  16465  4001lem1  16466  4001lem2  16467  4001lem3  16468  4001lem4  16469  4001prm  16470  baseid  16535  basendx  16539  basendxnn  16540  ressval3d  16553  1strstr  16590  2strstr  16594  basendxnplusgndx  16600  basendxnmulrndx  16610  rngstr  16611  lmodstr  16628  topgrpstr  16653  otpsstr  16660  ocndx  16665  ocid  16666  ressds  16678  resshom  16683  ressco  16684  slotsbhcdif  16685  oppcbas  16980  rescbas  17091  rescabs  17095  catstr  17219  estrreslem1  17379  ipostr  17755  mulgfval  18218  mulg1  18227  mulg2  18229  oppgbas  18471  symgvalstruct  18517  od1  18678  gex1  18708  efgsval2  18851  efgsp1  18855  torsubg  18967  pgpfaclem1  19196  mgpbas  19238  mgpds  19242  opprbas  19375  rmodislmod  19695  srabase  19943  srads  19951  cnfldfun  20103  zlmbas  20211  znbas2  20231  thlbas  20385  thlle  20386  opsrbas  20718  pmatcollpw3fi1lem2  21392  hauspwdom  22106  ressunif  22868  tuslem  22873  imasdsf1olem  22980  setsmsds  23083  tmslem  23089  tnglem  23246  tngbas  23247  tngds  23254  cphipval  23847  bcthlem4  23931  bcth3  23935  ovolmge0  24081  ovollb2  24093  ovolctb  24094  ovolunlem1a  24100  ovolunlem1  24101  ovoliunlem1  24106  ovoliun  24109  ovoliun2  24110  ovolicc1  24120  voliunlem1  24154  volsup  24160  ioombl1lem2  24163  ioombl1lem4  24165  uniioombllem1  24185  uniioombllem2  24187  uniioombllem6  24192  itg1climres  24318  itg2seq  24346  itg2monolem1  24354  itg2monolem2  24355  itg2monolem3  24356  itg2mono  24357  itg2i1fseq2  24360  itg2cnlem1  24365  aalioulem5  24932  aaliou2b  24937  aaliou3lem4  24942  aaliou3lem7  24945  log2ub  25535  emcllem6  25586  emcllem7  25587  lgam1  25649  gam1  25650  ftalem7  25664  efnnfsumcl  25688  vmaprm  25702  efvmacl  25705  efchtdvds  25744  vma1  25751  prmorcht  25763  sqff1o  25767  pclogsum  25799  perfectlem1  25813  perfectlem2  25814  bpos1  25867  bposlem5  25872  lgsdir  25916  lgs1  25925  lgsquad2lem2  25969  addsqn2reu  26025  addsqrexnreu  26026  dchrmusumlema  26077  dchrisum0lema  26098  trkgstr  26238  ttgbas  26671  ttgplusg  26672  ttgvsca  26674  eengstr  26774  baseltedgf  26787  usgrexmplef  27049  lfgrn1cycl  27591  clwwlkn1  27826  ipval2  28490  opsqrlem2  29924  ssnnssfz  30536  nnindf  30561  nn0min  30562  isarchi3  30866  resvbas  30956  rge0scvg  31302  zlmds  31315  qqh0  31335  qqh1  31336  esumfzf  31438  esumfsup  31439  esumpcvgval  31447  voliune  31598  eulerpartgbij  31740  eulerpartlemgs2  31748  fib2  31770  rrvsum  31822  ballotlem4  31866  ballotlemi1  31870  ballotlemii  31871  ballotlemic  31874  ballotlem1c  31875  hgt750lem  32032  hgt750leme  32039  0nn0m1nnn0  32461  faclimlem1  33088  nn0prpwlem  33783  nn0prpw  33784  bj-endbase  34730  poimirlem32  35089  ovoliunnfl  35099  voliunnfl  35101  volsupnfl  35102  incsequz  35186  bfplem1  35260  rrncmslem  35270  hlhilsbase  39235  60gcd7e1  39293  12lcm5e60  39296  60lcm7e420  39298  lcm1un  39301  lcmineqlem10  39326  nnmulcom  39473  3cubes  39631  jm2.23  39937  rmydioph  39955  rmxdioph  39957  expdiophlem2  39963  expdioph  39964  relexp2  40378  iunrelexpmin1  40409  iunrelexpmin2  40413  dftrcl3  40421  fvtrcllb1d  40423  cotrcltrcl  40426  corcltrcl  40440  cotrclrcl  40443  mnringbased  40923  prmunb2  41015  sumsnd  41655  nnn0  42011  xrralrecnnge  42026  iooiinicc  42179  iooiinioc  42193  mccl  42240  sumnnodd  42272  wallispilem4  42710  wallispi2lem1  42713  wallispi2lem2  42714  stirlinglem8  42723  stirlinglem11  42726  stirlinglem12  42727  stirlinglem13  42728  fourierdlem31  42780  nnfoctbdjlem  43094  hoicvr  43187  hoicvrrex  43195  hoidmvlelem3  43236  ovnhoilem1  43240  ovnhoilem2  43241  ovnlecvr2  43249  ovnsubadd2lem  43284  iinhoiicclem  43312  vonicclem2  43323  iccpartlt  43941  257prm  44078  fmtnoprmfac2lem1  44083  fmtno4prmfac193  44090  fmtno4nprmfac193  44091  fmtno5nprm  44100  3ndvds4  44112  139prmALT  44113  31prm  44114  127prm  44116  3exp4mod41  44134  41prothprmlem2  44136  perfectALTVlem1  44239  perfectALTVlem2  44240  2exp340mod341  44251  341fppr2  44252  4fppr1  44253  nnsum3primesprm  44308  bgoldbtbndlem1  44323  tgblthelfgott  44333  nnsgrpmgm  44436  nnsgrpnmnd  44438  blennn0elnn  44991  blen1  44998  ackval42  45110