Theorem 1nn 12164

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 11151	. . . 4 ⊢ 1 ∈ V
2		fr0g 8382	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8381	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7825	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7031	. . . 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 2835	. 2 ⊢ 1 ∈ ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
9		df-nn 12154	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5646	. . 3 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω) = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
11	9, 10	eqtri 2764	. 2 ⊢ ℕ = ran (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)
12	8, 11	eleqtrri 2837	1 ⊢ 1 ∈ ℕ

Syntax hints:   = wceq 1541   ∈ wcel 2106  Vcvv 3445  ∅c0 4282   ↦ cmpt 5188  ran crn 5634   ↾ cres 5635   “ cima 5636   Fn wfn 6491  ‘cfv 6496  (class class class)co 7357  ωcom 7802  reccrdg 8355  1c1 11052   + caddc 11054  ℕcn 12153

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2707  ax-sep 5256  ax-nul 5263  ax-pr 5384  ax-un 7672  ax-1cn 11109

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3or 1088  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-mo 2538  df-eu 2567  df-clab 2714  df-cleq 2728  df-clel 2814  df-nfc 2889  df-ne 2944  df-ral 3065  df-rex 3074  df-reu 3354  df-rab 3408  df-v 3447  df-sbc 3740  df-csb 3856  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-pss 3929  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-iun 4956  df-br 5106  df-opab 5168  df-mpt 5189  df-tr 5223  df-id 5531  df-eprel 5537  df-po 5545  df-so 5546  df-fr 5588  df-we 5590  df-xp 5639  df-rel 5640  df-cnv 5641  df-co 5642  df-dm 5643  df-rn 5644  df-res 5645  df-ima 5646  df-pred 6253  df-ord 6320  df-on 6321  df-lim 6322  df-suc 6323  df-iota 6448  df-fun 6498  df-fn 6499  df-f 6500  df-f1 6501  df-fo 6502  df-f1o 6503  df-fv 6504  df-ov 7360  df-om 7803  df-2nd 7922  df-frecs 8212  df-wrecs 8243  df-recs 8317  df-rdg 8356  df-nn 12154

This theorem is referenced by:  dfnn2  12166  dfnn3  12167  nnind  12171  nn1suc  12175  2nn  12226  nnunb  12409  1nn0  12429  nn0p1nn  12452  elz2  12517  1z  12533  neg1z  12539  nneo  12587  9p1e10  12620  elnn1uz2  12850  zq  12879  rpnnen1lem4  12905  rpnnen1lem5  12906  ser1const  13964  exp1  13973  nnexpcl  13980  expnbnd  14135  fac1  14177  faccl  14183  faclbnd3  14192  faclbnd4lem1  14193  faclbnd4lem2  14194  faclbnd4lem3  14195  faclbnd4lem4  14196  lsw0  14453  ccat2s1p1  14517  cats1un  14609  revs1  14653  cats1fvn  14747  relexpsucnnl  14915  relexpaddg  14938  isercolllem2  15550  isercolllem3  15551  isercoll  15552  sumsnf  15628  climcndslem1  15734  climcndslem2  15735  fprodnncl  15838  prodsn  15845  prodsnf  15847  nnrisefaccl  15902  eftlub  15991  eirrlem  16086  rpnnen2lem5  16100  rpnnen2lem8  16103  rpnnen2lem12  16107  dvdsle  16192  ndvdsp1  16293  gcd1  16408  bezoutr1  16445  1nprm  16555  1idssfct  16556  isprm2lem  16557  qden1elz  16632  phi1  16645  phiprm  16649  pcpre1  16714  pczpre  16719  pcmptcl  16763  pcmpt  16764  infpnlem2  16783  prmreclem1  16788  prmreclem6  16793  mul4sq  16826  vdwmc2  16851  vdwlem8  16860  vdwlem13  16865  vdwnnlem3  16869  prmocl  16906  prmop1  16910  fvprmselelfz  16916  fvprmselgcd1  16917  prmolefac  16918  prmodvdslcmf  16919  prmgapprmo  16934  5prm  16981  7prm  16983  11prm  16987  13prm  16988  17prm  16989  19prm  16990  37prm  16993  43prm  16994  83prm  16995  139prm  16996  163prm  16997  317prm  16998  631prm  16999  1259lem4  17006  1259lem5  17007  1259prm  17008  2503lem3  17011  2503prm  17012  4001lem1  17013  4001lem2  17014  4001lem3  17015  4001lem4  17016  4001prm  17017  baseid  17086  basendx  17092  basendxnn  17093  basendxnnOLD  17094  1strstr  17098  2strstr  17105  ressval3dOLD  17128  basendxnplusgndxOLD  17164  basendxnmulrndxOLD  17177  rngstr  17179  lmodstr  17206  topgrpstr  17242  otpsstr  17257  ocndx  17262  ocid  17263  basendxnocndx  17264  plendxnocndx  17265  basendxltdsndx  17269  dsndxnplusgndx  17271  dsndxnmulrndx  17272  slotsdnscsi  17273  dsndxntsetndx  17274  slotsdifdsndx  17275  basendxltunifndx  17279  unifndxntsetndx  17281  slotsdifunifndx  17282  slotsbhcdif  17296  slotsbhcdifOLD  17297  slotsdifocndx  17299  oppcbasOLD  17600  rescbasOLD  17713  rescabsOLD  17719  catstr  17845  estrreslem1OLD  18025  ipostr  18418  mulgfval  18874  mulg1  18883  mulg2  18885  oppgbasOLD  19131  symgvalstructOLD  19179  od1  19341  0subgALT  19350  gex1  19373  efgsval2  19515  efgsp1  19519  torsubg  19632  pgpfaclem1  19860  mgpbasOLD  19903  mgpdsOLD  19910  opprbasOLD  20057  rmodislmodOLD  20391  srabaseOLD  20641  sradsOLD  20655  cnfldfunALTOLD  20810  zlmbasOLD  20920  znbas2OLD  20944  thlbasOLD  21101  thlleOLD  21103  opsrbasOLD  21453  pmatcollpw3fi1lem2  22136  hauspwdom  22852  tuslemOLD  23619  imasdsf1olem  23726  setsmsdsOLD  23831  tmslemOLD  23838  tnglemOLD  23997  tngbasOLD  23999  tngdsOLD  24012  cphipval  24607  bcthlem4  24691  bcth3  24695  ovolmge0  24841  ovollb2  24853  ovolctb  24854  ovolunlem1a  24860  ovolunlem1  24861  ovoliunlem1  24866  ovoliun  24869  ovoliun2  24870  ovolicc1  24880  voliunlem1  24914  volsup  24920  ioombl1lem2  24923  ioombl1lem4  24925  uniioombllem1  24945  uniioombllem2  24947  uniioombllem6  24952  itg1climres  25079  itg2seq  25107  itg2monolem1  25115  itg2monolem2  25116  itg2monolem3  25117  itg2mono  25118  itg2i1fseq2  25121  itg2cnlem1  25126  aalioulem5  25696  aaliou2b  25701  aaliou3lem4  25706  aaliou3lem7  25709  log2ub  26299  emcllem6  26350  emcllem7  26351  lgam1  26413  gam1  26414  ftalem7  26428  efnnfsumcl  26452  vmaprm  26466  efvmacl  26469  efchtdvds  26508  vma1  26515  prmorcht  26527  sqff1o  26531  pclogsum  26563  perfectlem1  26577  perfectlem2  26578  bpos1  26631  bposlem5  26636  lgsdir  26680  lgs1  26689  lgsquad2lem2  26733  addsqn2reu  26789  addsqrexnreu  26790  dchrmusumlema  26841  dchrisum0lema  26862  slotsinbpsd  27383  slotslnbpsd  27384  trkgstr  27386  ttgbasOLD  27822  ttgplusgOLD  27824  ttgvscaOLD  27827  eengstr  27929  basendxltedgfndx  27944  baseltedgfOLD  27945  usgrexmplef  28207  lfgrn1cycl  28750  clwwlkn1  28985  ipval2  29649  opsqrlem2  31083  ssnnssfz  31690  nnindf  31715  nn0min  31716  isarchi3  32023  resvbasOLD  32125  rge0scvg  32530  zlmdsOLD  32544  qqh0  32565  qqh1  32566  esumfzf  32668  esumfsup  32669  esumpcvgval  32677  voliune  32828  eulerpartgbij  32972  eulerpartlemgs2  32980  fib2  33002  rrvsum  33054  ballotlem4  33098  ballotlemi1  33102  ballotlemii  33103  ballotlemic  33106  ballotlem1c  33107  hgt750lem  33264  hgt750leme  33271  0nn0m1nnn0  33703  faclimlem1  34316  nn0prpwlem  34794  nn0prpw  34795  poimirlem32  36110  ovoliunnfl  36120  voliunnfl  36122  volsupnfl  36123  incsequz  36207  bfplem1  36281  rrncmslem  36291  hlhilsbaseOLD  40404  60gcd7e1  40462  12lcm5e60  40465  60lcm7e420  40467  lcm1un  40470  lcmineqlem10  40495  3lexlogpow5ineq1  40511  3lexlogpow5ineq2  40512  3lexlogpow5ineq4  40513  aks4d1p1p7  40531  sticksstones9  40562  sticksstones11  40564  nnmulcom  40774  3cubes  40999  jm2.23  41306  rmydioph  41324  rmxdioph  41326  expdiophlem2  41332  expdioph  41333  relexp2  41939  iunrelexpmin1  41970  iunrelexpmin2  41974  dftrcl3  41982  fvtrcllb1d  41984  cotrcltrcl  41987  corcltrcl  42001  cotrclrcl  42004  mnringbasedOLD  42482  prmunb2  42581  sumsnd  43221  nnn0  43602  xrralrecnnge  43615  iooiinicc  43770  iooiinioc  43784  mccl  43829  sumnnodd  43861  wallispilem4  44299  wallispi2lem1  44302  wallispi2lem2  44303  stirlinglem8  44312  stirlinglem11  44315  stirlinglem12  44316  stirlinglem13  44317  fourierdlem31  44369  nnfoctbdjlem  44686  hoicvr  44779  hoicvrrex  44787  hoidmvlelem3  44828  ovnhoilem1  44832  ovnhoilem2  44833  ovnlecvr2  44841  ovnsubadd2lem  44876  iinhoiicclem  44904  vonicclem2  44915  iccpartlt  45606  257prm  45743  fmtnoprmfac2lem1  45748  fmtno4prmfac193  45755  fmtno4nprmfac193  45756  fmtno5nprm  45765  3ndvds4  45777  139prmALT  45778  31prm  45779  127prm  45781  3exp4mod41  45798  41prothprmlem2  45800  perfectALTVlem1  45903  perfectALTVlem2  45904  2exp340mod341  45915  341fppr2  45916  4fppr1  45917  nnsum3primesprm  45972  bgoldbtbndlem1  45987  tgblthelfgott  45997  nnsgrpmgm  46100  nnsgrpnmnd  46102  blennn0elnn  46653  blen1  46660  ackval42  46772