Theorem 1nn 8903

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 8894	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2242	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 7931	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3848	. . . 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 2738	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2239	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2239	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2678	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2879	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2533	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2146  {cab 2161  ∀wral 2453  ∩ cint 3840  (class class class)co 5865  ℝcr 7785  1c1 7787   + caddc 7789  ℕcn 8892

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 709  ax-5 1445  ax-7 1446  ax-gen 1447  ax-ie1 1491  ax-ie2 1492  ax-8 1502  ax-10 1503  ax-11 1504  ax-i12 1505  ax-bndl 1507  ax-4 1508  ax-17 1524  ax-i9 1528  ax-ial 1532  ax-i5r 1533  ax-ext 2157  ax-1re 7880

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1459  df-sb 1761  df-clab 2162  df-cleq 2168  df-clel 2171  df-nfc 2306  df-ral 2458  df-v 2737  df-int 3841  df-inn 8893

This theorem is referenced by:  nnind  8908  nn1suc  8911  2nn  9053  1nn0  9165  nn0p1nn  9188  1z  9252  neg1z  9258  elz2  9297  nneoor  9328  9p1e10  9359  indstr  9566  elnn1uz2  9580  zq  9599  qreccl  9615  fz01or  10081  exp3vallem  10491  exp1  10496  nnexpcl  10503  expnbnd  10613  3dec  10662  fac1  10677  faccl  10683  faclbnd3  10691  fiubnn  10778  resqrexlemf1  10985  resqrexlemcalc3  10993  resqrexlemnmsq  10994  resqrexlemnm  10995  resqrexlemcvg  10996  resqrexlemglsq  10999  resqrexlemga  11000  sumsnf  11385  cvgratnnlemnexp  11500  cvgratnnlemfm  11505  cvgratnnlemrate  11506  cvgratnn  11507  prodsnf  11568  fprodnncl  11586  eftlub  11666  eirraplem  11752  n2dvds1  11884  ndvdsp1  11904  gcd1  11955  bezoutr1  12001  ncoprmgcdne1b  12056  1nprm  12081  1idssfct  12082  isprm2lem  12083  qden1elz  12172  phicl2  12181  phi1  12186  phiprm  12190  eulerthlema  12197  pcpre1  12259  pczpre  12264  pcmptcl  12307  pcmpt  12308  infpnlem2  12325  mul4sq  12359  exmidunben  12394  nninfdc  12421  base0  12478  baseval  12481  baseid  12482  basendx  12483  basendxnn  12484  1strstrg  12529  2strstrg  12531  basendxnplusgndx  12537  basendxnmulrndx  12545  rngstrg  12546  lmodstrd  12567  topgrpstrd  12592  basendxltdsndx  12603  dsndxnplusgndx  12605  dsndxnmulrndx  12606  slotsdnscsi  12607  dsndxntsetndx  12608  slotsdifdsndx  12609  mulg1  12851  mulg2  12853  mulgnndir  12872  setsmsdsg  13551  lgsdir2lem1  14000  lgsdir2lem4  14003  lgsdir2lem5  14004  lgsdir  14007  lgsne0  14010  lgs1  14016  trilpolemgt1  14348