Theorem 1nn 11649

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 10637	. . . 4 ⊢ 1 ∈ V
2		fr0g 8071	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8070	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7601	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 6848	. . . 4 ⊢ (((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω ∧ ∅ ∈ ω) → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω))
7	4, 5, 6	mp2an 690	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
8	3, 7	eqeltrri 2910	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 11639	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5568	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2844	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2912	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1537   ∈ wcel 2114  Vcvv 3494  ∅c0 4291   ↦ cmpt 5146  ran crn 5556   ↾ cres 5557   “ cima 5558   Fn wfn 6350  ‘cfv 6355  (class class class)co 7156  ωcom 7580  reccrdg 8045  1c1 10538   + caddc 10540  ℕcn 11638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793  ax-sep 5203  ax-nul 5210  ax-pow 5266  ax-pr 5330  ax-un 7461  ax-1cn 10595

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1084  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-mo 2622  df-eu 2654  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-ne 3017  df-ral 3143  df-rex 3144  df-reu 3145  df-rab 3147  df-v 3496  df-sbc 3773  df-csb 3884  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-pss 3954  df-nul 4292  df-if 4468  df-pw 4541  df-sn 4568  df-pr 4570  df-tp 4572  df-op 4574  df-uni 4839  df-iun 4921  df-br 5067  df-opab 5129  df-mpt 5147  df-tr 5173  df-id 5460  df-eprel 5465  df-po 5474  df-so 5475  df-fr 5514  df-we 5516  df-xp 5561  df-rel 5562  df-cnv 5563  df-co 5564  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568  df-pred 6148  df-ord 6194  df-on 6195  df-lim 6196  df-suc 6197  df-iota 6314  df-fun 6357  df-fn 6358  df-f 6359  df-f1 6360  df-fo 6361  df-f1o 6362  df-fv 6363  df-om 7581  df-wrecs 7947  df-recs 8008  df-rdg 8046  df-nn 11639

This theorem is referenced by:  dfnn2  11651  dfnn3  11652  nnind  11656  nn1suc  11660  2nn  11711  nnunb  11894  1nn0  11914  nn0p1nn  11937  elz2  12000  1z  12013  neg1z  12019  nneo  12067  9p1e10  12101  elnn1uz2  12326  zq  12355  rpnnen1lem4  12380  rpnnen1lem5  12381  ser1const  13427  exp1  13436  nnexpcl  13443  expnbnd  13594  fac1  13638  faccl  13644  faclbnd3  13653  faclbnd4lem1  13654  faclbnd4lem2  13655  faclbnd4lem3  13656  faclbnd4lem4  13657  lsw0  13917  ccat2s1p1  13985  ccat2s1p1OLD  13987  cats1un  14083  revs1  14127  cats1fvn  14220  relexpsucnnl  14391  relexpaddg  14412  isercolllem2  15022  isercolllem3  15023  isercoll  15024  sumsnf  15099  climcndslem1  15204  climcndslem2  15205  fprodnncl  15309  prodsn  15316  prodsnf  15318  nnrisefaccl  15373  eftlub  15462  eirrlem  15557  rpnnen2lem5  15571  rpnnen2lem8  15574  rpnnen2lem12  15578  dvdsle  15660  n2dvds1OLD  15718  ndvdsp1  15762  gcd1  15876  bezoutr1  15913  1nprm  16023  1idssfct  16024  isprm2lem  16025  qden1elz  16097  phi1  16110  phiprm  16114  pcpre1  16179  pczpre  16184  pcmptcl  16227  pcmpt  16228  infpnlem2  16247  prmreclem1  16252  prmreclem6  16257  mul4sq  16290  vdwmc2  16315  vdwlem8  16324  vdwlem13  16329  vdwnnlem3  16333  prmocl  16370  prmop1  16374  fvprmselelfz  16380  fvprmselgcd1  16381  prmolefac  16382  prmodvdslcmf  16383  prmgapprmo  16398  5prm  16442  7prm  16444  11prm  16448  13prm  16449  17prm  16450  19prm  16451  37prm  16454  43prm  16455  83prm  16456  139prm  16457  163prm  16458  317prm  16459  631prm  16460  1259lem4  16467  1259lem5  16468  1259prm  16469  2503lem3  16472  2503prm  16473  4001lem1  16474  4001lem2  16475  4001lem3  16476  4001lem4  16477  4001prm  16478  baseid  16543  basendx  16547  basendxnn  16548  ressval3d  16561  1strstr  16598  2strstr  16602  basendxnplusgndx  16608  basendxnmulrndx  16618  rngstr  16619  lmodstr  16636  topgrpstr  16661  otpsstr  16668  ocndx  16673  ocid  16674  ressds  16686  resshom  16691  ressco  16692  slotsbhcdif  16693  oppcbas  16988  rescbas  17099  rescabs  17103  catstr  17227  estrreslem1  17387  ipostr  17763  mulgfval  18226  mulg1  18235  mulg2  18237  oppgbas  18479  symgvalstruct  18525  od1  18686  gex1  18716  efgsval2  18859  efgsp1  18863  torsubg  18974  pgpfaclem1  19203  mgpbas  19245  mgpds  19249  opprbas  19379  rmodislmod  19702  srabase  19950  srads  19958  opsrbas  20259  cnfldfun  20557  zlmbas  20665  znbas2  20686  thlbas  20840  thlle  20841  pmatcollpw3fi1lem2  21395  hauspwdom  22109  ressunif  22871  tuslem  22876  imasdsf1olem  22983  setsmsds  23086  tmslem  23092  tnglem  23249  tngbas  23250  tngds  23257  cphipval  23846  bcthlem4  23930  bcth3  23934  ovolmge0  24078  ovollb2  24090  ovolctb  24091  ovolunlem1a  24097  ovolunlem1  24098  ovoliunlem1  24103  ovoliun  24106  ovoliun2  24107  ovolicc1  24117  voliunlem1  24151  volsup  24157  ioombl1lem2  24160  ioombl1lem4  24162  uniioombllem1  24182  uniioombllem2  24184  uniioombllem6  24189  itg1climres  24315  itg2seq  24343  itg2monolem1  24351  itg2monolem2  24352  itg2monolem3  24353  itg2mono  24354  itg2i1fseq2  24357  itg2cnlem1  24362  aalioulem5  24925  aaliou2b  24930  aaliou3lem4  24935  aaliou3lem7  24938  log2ub  25527  emcllem6  25578  emcllem7  25579  lgam1  25641  gam1  25642  ftalem7  25656  efnnfsumcl  25680  vmaprm  25694  efvmacl  25697  efchtdvds  25736  vma1  25743  prmorcht  25755  sqff1o  25759  pclogsum  25791  perfectlem1  25805  perfectlem2  25806  bpos1  25859  bposlem5  25864  lgsdir  25908  lgs1  25917  lgsquad2lem2  25961  addsqn2reu  26017  addsqrexnreu  26018  dchrmusumlema  26069  dchrisum0lema  26090  trkgstr  26230  ttgbas  26663  ttgplusg  26664  ttgvsca  26666  eengstr  26766  baseltedgf  26779  usgrexmplef  27041  lfgrn1cycl  27583  clwwlkn1  27819  ipval2  28484  opsqrlem2  29918  ssnnssfz  30510  nnindf  30535  nn0min  30536  isarchi3  30816  resvbas  30905  rge0scvg  31192  zlmds  31205  qqh0  31225  qqh1  31226  esumfzf  31328  esumfsup  31329  esumpcvgval  31337  voliune  31488  eulerpartgbij  31630  eulerpartlemgs2  31638  fib2  31660  rrvsum  31712  ballotlem4  31756  ballotlemi1  31760  ballotlemii  31761  ballotlemic  31764  ballotlem1c  31765  hgt750lem  31922  hgt750leme  31929  0nn0m1nnn0  32351  faclimlem1  32975  nn0prpwlem  33670  nn0prpw  33671  bj-endbase  34600  poimirlem32  34939  ovoliunnfl  34949  voliunnfl  34951  volsupnfl  34952  incsequz  35038  bfplem1  35115  rrncmslem  35125  hlhilsbase  39090  nnmulcom  39185  3cubes  39307  jm2.23  39613  rmydioph  39631  rmxdioph  39633  expdiophlem2  39639  expdioph  39640  relexp2  40042  iunrelexpmin1  40073  iunrelexpmin2  40077  dftrcl3  40085  fvtrcllb1d  40087  cotrcltrcl  40090  corcltrcl  40104  cotrclrcl  40107  prmunb2  40663  sumsnd  41303  nnn0  41667  xrralrecnnge  41682  iooiinicc  41838  iooiinioc  41852  mccl  41899  sumnnodd  41931  wallispilem4  42373  wallispi2lem1  42376  wallispi2lem2  42377  stirlinglem8  42386  stirlinglem11  42389  stirlinglem12  42390  stirlinglem13  42391  fourierdlem31  42443  nnfoctbdjlem  42757  hoicvr  42850  hoicvrrex  42858  hoidmvlelem3  42899  ovnhoilem1  42903  ovnhoilem2  42904  ovnlecvr2  42912  ovnsubadd2lem  42947  iinhoiicclem  42975  vonicclem2  42986  iccpartlt  43604  257prm  43743  fmtnoprmfac2lem1  43748  fmtno4prmfac193  43755  fmtno4nprmfac193  43756  fmtno5nprm  43765  3ndvds4  43778  139prmALT  43779  31prm  43780  127prm  43783  3exp4mod41  43801  41prothprmlem2  43803  perfectALTVlem1  43906  perfectALTVlem2  43907  2exp340mod341  43918  341fppr2  43919  4fppr1  43920  nnsum3primesprm  43975  bgoldbtbndlem1  43990  tgblthelfgott  44000  nnsgrpmgm  44103  nnsgrpnmnd  44105  blennn0elnn  44657  blen1  44664