Theorem 1nn 12157

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 11130	. . . 4 ⊢ 1 ∈ V
2		fr0g 8365	. . . 4 ⊢ (1 ∈ V → ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1)
3	1, 2	ax-mp 5	. . 3 ⊢ ((rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω)‘∅) = 1
4		frfnom 8364	. . . 4 ⊢ (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) ↾ ω) Fn ω
5		peano1 7829	. . . 4 ⊢ ∅ ∈ ω
6		fnfvelrn 7018	. . . 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 12147	. . 3 ⊢ ℕ = (rec((𝑥 ∈ V ↦ (𝑥 + 1)), 1) “ ω)
10		df-ima 5636	. . 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 3438  ∅c0 4286   ↦ cmpt 5176  ran crn 5624   ↾ cres 5625   “ cima 5626   Fn wfn 6481  ‘cfv 6486  (class class class)co 7353  ωcom 7806  reccrdg 8338  1c1 11029   + caddc 11031  ℕcn 12146

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 5238  ax-nul 5248  ax-pr 5374  ax-un 7675  ax-1cn 11086

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 3346  df-rab 3397  df-v 3440  df-sbc 3745  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-pss 3925  df-nul 4287  df-if 4479  df-pw 4555  df-sn 4580  df-pr 4582  df-op 4586  df-uni 4862  df-iun 4946  df-br 5096  df-opab 5158  df-mpt 5177  df-tr 5203  df-id 5518  df-eprel 5523  df-po 5531  df-so 5532  df-fr 5576  df-we 5578  df-xp 5629  df-rel 5630  df-cnv 5631  df-co 5632  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636  df-pred 6253  df-ord 6314  df-on 6315  df-lim 6316  df-suc 6317  df-iota 6442  df-fun 6488  df-fn 6489  df-f 6490  df-f1 6491  df-fo 6492  df-f1o 6493  df-fv 6494  df-ov 7356  df-om 7807  df-2nd 7932  df-frecs 8221  df-wrecs 8252  df-recs 8301  df-rdg 8339  df-nn 12147

This theorem is referenced by:  dfnn2  12159  dfnn3  12160  nnind  12164  nn1suc  12168  2nn  12219  nnunb  12398  1nn0  12418  nn0p1nn  12441  elz2  12507  1z  12523  neg1z  12529  nneo  12578  9p1e10  12611  elnn1uz2  12844  zq  12873  rpnnen1lem4  12899  rpnnen1lem5  12900  1elfzo1  13635  ser1const  13983  exp1  13992  nnexpcl  13999  expnbnd  14157  fac1  14202  faccl  14208  faclbnd3  14217  faclbnd4lem1  14218  faclbnd4lem2  14219  faclbnd4lem3  14220  faclbnd4lem4  14221  lsw0  14490  ccat2s1p1  14554  cats1un  14645  revs1  14689  cats1fvn  14783  relexpsucnnl  14955  relexpaddg  14978  isercolllem2  15591  isercolllem3  15592  isercoll  15593  sumsnf  15668  climcndslem1  15774  climcndslem2  15775  fprodnncl  15880  prodsn  15887  prodsnf  15889  nnrisefaccl  15944  eftlub  16036  eirrlem  16131  rpnnen2lem5  16145  rpnnen2lem8  16148  rpnnen2lem12  16152  dvdsle  16239  ndvdsp1  16340  5ndvds6  16343  gcd1  16457  bezoutr1  16498  1nprm  16608  1idssfct  16609  isprm2lem  16610  qden1elz  16686  phi1  16702  phiprm  16706  pcpre1  16772  pczpre  16777  pcmptcl  16821  pcmpt  16822  infpnlem2  16841  prmreclem1  16846  prmreclem6  16851  mul4sq  16884  vdwmc2  16909  vdwlem8  16918  vdwlem13  16923  vdwnnlem3  16927  prmocl  16964  prmop1  16968  fvprmselelfz  16974  fvprmselgcd1  16975  prmolefac  16976  prmodvdslcmf  16977  prmgapprmo  16992  5prm  17038  7prm  17040  11prm  17044  13prm  17045  17prm  17046  19prm  17047  37prm  17050  43prm  17051  83prm  17052  139prm  17053  163prm  17054  317prm  17055  631prm  17056  1259lem4  17063  1259lem5  17064  1259prm  17065  2503lem3  17068  2503prm  17069  4001lem1  17070  4001lem2  17071  4001lem3  17072  4001lem4  17073  4001prm  17074  baseid  17141  basendx  17147  basendxnn  17148  rngstr  17220  lmodstr  17247  topgrpstr  17283  otpsstr  17298  ocndx  17303  ocid  17304  basendxnocndx  17305  plendxnocndx  17306  basendxltdsndx  17310  dsndxnplusgndx  17312  dsndxnmulrndx  17313  slotsdnscsi  17314  dsndxntsetndx  17315  slotsdifdsndx  17316  basendxltunifndx  17320  unifndxntsetndx  17322  slotsdifunifndx  17323  slotsbhcdif  17337  slotsdifocndx  17339  catstr  17885  ipostr  18453  mulgfval  18966  mulg1  18978  mulg2  18980  od1  19456  0subgALT  19465  gex1  19488  efgsval2  19630  efgsp1  19634  torsubg  19751  pgpfaclem1  19980  pmatcollpw3fi1lem2  22690  hauspwdom  23404  imasdsf1olem  24277  cphipval  25159  bcthlem4  25243  bcth3  25247  ovolmge0  25394  ovollb2  25406  ovolctb  25407  ovolunlem1a  25413  ovolunlem1  25414  ovoliunlem1  25419  ovoliun  25422  ovoliun2  25423  ovolicc1  25433  voliunlem1  25467  volsup  25473  ioombl1lem2  25476  ioombl1lem4  25478  uniioombllem1  25498  uniioombllem2  25500  uniioombllem6  25505  itg1climres  25631  itg2seq  25659  itg2monolem1  25667  itg2monolem2  25668  itg2monolem3  25669  itg2mono  25670  itg2i1fseq2  25673  itg2cnlem1  25678  aalioulem5  26260  aaliou2b  26265  aaliou3lem4  26270  aaliou3lem7  26273  log2ub  26875  emcllem6  26927  emcllem7  26928  lgam1  26990  gam1  26991  ftalem7  27005  efnnfsumcl  27029  vmaprm  27043  efvmacl  27046  efchtdvds  27085  vma1  27092  prmorcht  27104  sqff1o  27108  pclogsum  27142  perfectlem1  27156  perfectlem2  27157  bpos1  27210  bposlem5  27215  lgsdir  27259  lgs1  27268  lgsquad2lem2  27312  addsqn2reu  27368  addsqrexnreu  27369  dchrmusumlema  27420  dchrisum0lema  27441  slotsinbpsd  28404  slotslnbpsd  28405  trkgstr  28407  eengstr  28943  basendxltedgfndx  28957  usgrexmplef  29222  lfgrn1cycl  29768  clwwlkn1  30003  ipval2  30669  opsqrlem2  32103  ssnnssfz  32743  znumd  32770  zdend  32771  nnindf  32777  nn0min  32778  isarchi3  33142  eufndx  33242  eufid  33243  constrext2chnlem  33719  iconstr  33735  rge0scvg  33918  qqh0  33953  qqh1  33954  esumfzf  34038  esumfsup  34039  esumpcvgval  34047  voliune  34198  eulerpartgbij  34342  eulerpartlemgs2  34350  fib2  34372  rrvsum  34424  ballotlem4  34469  ballotlemi1  34473  ballotlemii  34474  ballotlemic  34477  ballotlem1c  34478  hgt750lem  34621  hgt750leme  34628  0nn0m1nnn0  35088  faclimlem1  35718  nn0prpwlem  36298  nn0prpw  36299  poimirlem32  37634  ovoliunnfl  37644  voliunnfl  37646  volsupnfl  37647  incsequz  37730  bfplem1  37804  rrncmslem  37814  60gcd7e1  41981  12lcm5e60  41984  60lcm7e420  41986  lcm1un  41989  lcmineqlem10  42014  3lexlogpow5ineq1  42030  3lexlogpow5ineq2  42031  3lexlogpow5ineq4  42032  aks4d1p1p7  42050  aks6d1c1p8  42091  sticksstones9  42130  sticksstones11  42132  aks6d1c7lem1  42156  nnmulcom  42248  3cubes  42666  jm2.23  42972  rmydioph  42990  rmxdioph  42992  expdiophlem2  42998  expdioph  42999  relexp2  43653  iunrelexpmin1  43684  iunrelexpmin2  43688  dftrcl3  43696  fvtrcllb1d  43698  cotrcltrcl  43701  corcltrcl  43715  cotrclrcl  43718  prmunb2  44287  sumsnd  45007  nnn0  45361  xrralrecnnge  45373  iooiinicc  45527  iooiinioc  45541  mccl  45583  sumnnodd  45615  wallispilem4  46053  wallispi2lem1  46056  wallispi2lem2  46057  stirlinglem8  46066  stirlinglem11  46069  stirlinglem12  46070  stirlinglem13  46071  fourierdlem31  46123  nnfoctbdjlem  46440  hoicvr  46533  hoicvrrex  46541  hoidmvlelem3  46582  ovnhoilem1  46586  ovnhoilem2  46587  ovnlecvr2  46595  ovnsubadd2lem  46630  iinhoiicclem  46658  vonicclem2  46669  1elfzo1ceilhalf1  47325  iccpartlt  47412  257prm  47549  fmtnoprmfac2lem1  47554  fmtno4prmfac193  47561  fmtno4nprmfac193  47562  fmtno5nprm  47571  3ndvds4  47583  139prmALT  47584  31prm  47585  127prm  47587  3exp4mod41  47604  41prothprmlem2  47606  perfectALTVlem1  47709  perfectALTVlem2  47710  2exp340mod341  47721  341fppr2  47722  4fppr1  47723  nnsum3primesprm  47778  bgoldbtbndlem1  47793  tgblthelfgott  47803  nnsgrpmgm  48164  nnsgrpnmnd  48166  blennn0elnn  48566  blen1  48573  ackval42  48685