Theorem 1nn 9315

Description: Peano postulate: 1 is a positive integer. (Contributed by NM, 11-Jan-1997.)

Assertion

Ref	Expression
1nn	⊢ 1 ∈ ℕ

Proof of Theorem 1nn

Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		dfnn2 9306	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2305	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8325	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3978	. . . 4 ⊢ (1 ∈ ℝ → (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
5	3, 4	ax-mp 5	. . 3 ⊢ (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
6	2, 5	bitri 184	. 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7		vex 2824	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2302	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2302	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2761	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 477	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2970	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2608	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  {cab 2224  ∀wral 2528  ∩ cint 3970  (class class class)co 6085  ℝcr 8178  1c1 8180   + caddc 8182  ℕcn 9304

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8273

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-int 3971  df-inn 9305

This theorem is used by:  nnind  9320  nn1suc  9323  2nn  9466  1nn0  9579  nn0p1nn  9602  1z  9670  neg1z  9676  elz2  9716  nneoor  9748  9p1e10  9779  indstr  9993  elnn1uz2  10007  zq  10026  qreccl  10042  fz01or  10518  exp3vallem  10977  exp1  10982  nnexpcl  10989  expnbnd  11101  3dec  11152  fac1  11167  faccl  11173  faclbnd3  11181  fiubnn  11273  lsw0  11352  cats1un  11493  cats1fvn  11536  cats1fvnd  11537  resqrexlemf1  11774  resqrexlemcalc3  11782  resqrexlemnmsq  11783  resqrexlemnm  11784  resqrexlemcvg  11785  resqrexlemglsq  11788  resqrexlemga  11789  sumsnf  12176  cvgratnnlemnexp  12291  cvgratnnlemfm  12296  cvgratnnlemrate  12297  cvgratnn  12298  prodsnf  12359  fprodnncl  12377  eftlub  12457  eirraplem  12544  n2dvds1  12679  ndvdsp1  12699  5ndvds6  12702  gcd1  12764  bezoutr1  12810  ncoprmgcdne1b  12867  1nprm  12892  1idssfct  12893  isprm2lem  12894  qden1elz  12983  phicl2  12992  phi1  12997  phiprm  13001  eulerthlema  13008  pcpre1  13071  pczpre  13076  pcmptcl  13121  pcmpt  13122  infpnlem2  13139  mul4sq  13173  ballotfilem4  13241  ballotfilemi1  13245  ballotfilemii  13246  ballotfilemic  13250  ballotfilem1c  13251  exmidunben  13317  nninfdc  13344  base0  13402  baseval  13405  baseid  13406  basendx  13407  basendxnn  13408  1strstrg  13470  2strstrg  13473  basendxnplusgndx  13479  basendxnmulrndx  13488  rngstrg  13489  lmodstrd  13518  topgrpstrd  13550  ocndx  13565  ocid  13566  basendxnocndx  13567  plendxnocndx  13568  basendxltdsndx  13573  dsndxnplusgndx  13575  dsndxnmulrndx  13576  slotsdnscsi  13577  dsndxntsetndx  13578  slotsdifdsndx  13579  basendxltunifndx  13583  unifndxntsetndx  13585  slotsdifunifndx  13586  mulg1  13932  mulg2  13934  mulgnndir  13954  setsmsdsg  15581  logfac  15995  log2ublog2  16086  perfectlem1  16113  perfectlem2  16114  lgsdir2lem1  16147  lgsdir2lem4  16150  lgsdir2lem5  16151  lgsdir  16154  lgsne0  16157  lgs1  16163  lgsquad2lem2  16201  basendxltedgfndx  16251  clwwlkn1  16659  konigsberglem1  16729  trilpolemgt1  17088