Theorem 1nn 8961

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 8952	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2256	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 7987	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3867	. . . 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 2755	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2253	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2253	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2694	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2896	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2548	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2160  {cab 2175  ∀wral 2468  ∩ cint 3859  (class class class)co 5897  ℝcr 7841  1c1 7843   + caddc 7845  ℕcn 8950

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 1458  ax-7 1459  ax-gen 1460  ax-ie1 1504  ax-ie2 1505  ax-8 1515  ax-10 1516  ax-11 1517  ax-i12 1518  ax-bndl 1520  ax-4 1521  ax-17 1537  ax-i9 1541  ax-ial 1545  ax-i5r 1546  ax-ext 2171  ax-1re 7936

This theorem depends on definitions:  df-bi 117  df-tru 1367  df-nf 1472  df-sb 1774  df-clab 2176  df-cleq 2182  df-clel 2185  df-nfc 2321  df-ral 2473  df-v 2754  df-int 3860  df-inn 8951

This theorem is referenced by:  nnind  8966  nn1suc  8969  2nn  9111  1nn0  9223  nn0p1nn  9246  1z  9310  neg1z  9316  elz2  9355  nneoor  9386  9p1e10  9417  indstr  9625  elnn1uz2  9639  zq  9658  qreccl  9674  fz01or  10143  exp3vallem  10555  exp1  10560  nnexpcl  10567  expnbnd  10678  3dec  10729  fac1  10744  faccl  10750  faclbnd3  10758  fiubnn  10845  resqrexlemf1  11052  resqrexlemcalc3  11060  resqrexlemnmsq  11061  resqrexlemnm  11062  resqrexlemcvg  11063  resqrexlemglsq  11066  resqrexlemga  11067  sumsnf  11452  cvgratnnlemnexp  11567  cvgratnnlemfm  11572  cvgratnnlemrate  11573  cvgratnn  11574  prodsnf  11635  fprodnncl  11653  eftlub  11733  eirraplem  11819  n2dvds1  11952  ndvdsp1  11972  gcd1  12023  bezoutr1  12069  ncoprmgcdne1b  12124  1nprm  12149  1idssfct  12150  isprm2lem  12151  qden1elz  12240  phicl2  12249  phi1  12254  phiprm  12258  eulerthlema  12265  pcpre1  12327  pczpre  12332  pcmptcl  12377  pcmpt  12378  infpnlem2  12395  mul4sq  12429  exmidunben  12480  nninfdc  12507  base0  12565  baseval  12568  baseid  12569  basendx  12570  basendxnn  12571  1strstrg  12631  2strstrg  12633  basendxnplusgndx  12639  basendxnmulrndx  12648  rngstrg  12649  lmodstrd  12678  topgrpstrd  12710  basendxltdsndx  12729  dsndxnplusgndx  12731  dsndxnmulrndx  12732  slotsdnscsi  12733  dsndxntsetndx  12734  slotsdifdsndx  12735  basendxltunifndx  12739  unifndxntsetndx  12741  slotsdifunifndx  12742  mulg1  13086  mulg2  13088  mulgnndir  13108  cnfldstr  13883  setsmsdsg  14457  lgsdir2lem1  14907  lgsdir2lem4  14910  lgsdir2lem5  14911  lgsdir  14914  lgsne0  14917  lgs1  14923  trilpolemgt1  15266