Theorem 1nn 9020

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 9011	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2263	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8044	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3883	. . . 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 2766	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2260	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2260	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2705	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2908	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2555	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2167  {cab 2182  ∀wral 2475  ∩ cint 3875  (class class class)co 5925  ℝcr 7897  1c1 7899   + caddc 7901  ℕcn 9009

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-ext 2178  ax-1re 7992

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1475  df-sb 1777  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ral 2480  df-v 2765  df-int 3876  df-inn 9010

This theorem is referenced by:  nnind  9025  nn1suc  9028  2nn  9171  1nn0  9284  nn0p1nn  9307  1z  9371  neg1z  9377  elz2  9416  nneoor  9447  9p1e10  9478  indstr  9686  elnn1uz2  9700  zq  9719  qreccl  9735  fz01or  10205  exp3vallem  10651  exp1  10656  nnexpcl  10663  expnbnd  10774  3dec  10825  fac1  10840  faccl  10846  faclbnd3  10854  fiubnn  10941  resqrexlemf1  11192  resqrexlemcalc3  11200  resqrexlemnmsq  11201  resqrexlemnm  11202  resqrexlemcvg  11203  resqrexlemglsq  11206  resqrexlemga  11207  sumsnf  11593  cvgratnnlemnexp  11708  cvgratnnlemfm  11713  cvgratnnlemrate  11714  cvgratnn  11715  prodsnf  11776  fprodnncl  11794  eftlub  11874  eirraplem  11961  n2dvds1  12096  ndvdsp1  12116  5ndvds6  12119  gcd1  12181  bezoutr1  12227  ncoprmgcdne1b  12284  1nprm  12309  1idssfct  12310  isprm2lem  12311  qden1elz  12400  phicl2  12409  phi1  12414  phiprm  12418  eulerthlema  12425  pcpre1  12488  pczpre  12493  pcmptcl  12538  pcmpt  12539  infpnlem2  12556  mul4sq  12590  exmidunben  12670  nninfdc  12697  base0  12755  baseval  12758  baseid  12759  basendx  12760  basendxnn  12761  1strstrg  12821  2strstrg  12823  basendxnplusgndx  12829  basendxnmulrndx  12838  rngstrg  12839  lmodstrd  12868  topgrpstrd  12900  ocndx  12915  ocid  12916  basendxnocndx  12917  plendxnocndx  12918  basendxltdsndx  12923  dsndxnplusgndx  12925  dsndxnmulrndx  12926  slotsdnscsi  12927  dsndxntsetndx  12928  slotsdifdsndx  12929  basendxltunifndx  12933  unifndxntsetndx  12935  slotsdifunifndx  12936  mulg1  13337  mulg2  13339  mulgnndir  13359  setsmsdsg  14824  perfectlem1  15343  perfectlem2  15344  lgsdir2lem1  15377  lgsdir2lem4  15380  lgsdir2lem5  15381  lgsdir  15384  lgsne0  15387  lgs1  15393  lgsquad2lem2  15431  trilpolemgt1  15796