Theorem 1nn 9132

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 9123	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2296	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8156	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3931	. . . 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 2802	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2293	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2293	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2740	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2947	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2588	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2200  {cab 2215  ∀wral 2508  ∩ cint 3923  (class class class)co 6007  ℝcr 8009  1c1 8011   + caddc 8013  ℕcn 9121

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 714  ax-5 1493  ax-7 1494  ax-gen 1495  ax-ie1 1539  ax-ie2 1540  ax-8 1550  ax-10 1551  ax-11 1552  ax-i12 1553  ax-bndl 1555  ax-4 1556  ax-17 1572  ax-i9 1576  ax-ial 1580  ax-i5r 1581  ax-ext 2211  ax-1re 8104

This theorem depends on definitions:  df-bi 117  df-tru 1398  df-nf 1507  df-sb 1809  df-clab 2216  df-cleq 2222  df-clel 2225  df-nfc 2361  df-ral 2513  df-v 2801  df-int 3924  df-inn 9122

This theorem is referenced by:  nnind  9137  nn1suc  9140  2nn  9283  1nn0  9396  nn0p1nn  9419  1z  9483  neg1z  9489  elz2  9529  nneoor  9560  9p1e10  9591  indstr  9800  elnn1uz2  9814  zq  9833  qreccl  9849  fz01or  10319  exp3vallem  10774  exp1  10779  nnexpcl  10786  expnbnd  10897  3dec  10948  fac1  10963  faccl  10969  faclbnd3  10977  fiubnn  11065  lsw0  11132  cats1un  11268  cats1fvn  11311  cats1fvnd  11312  resqrexlemf1  11534  resqrexlemcalc3  11542  resqrexlemnmsq  11543  resqrexlemnm  11544  resqrexlemcvg  11545  resqrexlemglsq  11548  resqrexlemga  11549  sumsnf  11935  cvgratnnlemnexp  12050  cvgratnnlemfm  12055  cvgratnnlemrate  12056  cvgratnn  12057  prodsnf  12118  fprodnncl  12136  eftlub  12216  eirraplem  12303  n2dvds1  12438  ndvdsp1  12458  5ndvds6  12461  gcd1  12523  bezoutr1  12569  ncoprmgcdne1b  12626  1nprm  12651  1idssfct  12652  isprm2lem  12653  qden1elz  12742  phicl2  12751  phi1  12756  phiprm  12760  eulerthlema  12767  pcpre1  12830  pczpre  12835  pcmptcl  12880  pcmpt  12881  infpnlem2  12898  mul4sq  12932  exmidunben  13012  nninfdc  13039  base0  13097  baseval  13100  baseid  13101  basendx  13102  basendxnn  13103  1strstrg  13164  2strstrg  13167  basendxnplusgndx  13173  basendxnmulrndx  13182  rngstrg  13183  lmodstrd  13212  topgrpstrd  13244  ocndx  13259  ocid  13260  basendxnocndx  13261  plendxnocndx  13262  basendxltdsndx  13267  dsndxnplusgndx  13269  dsndxnmulrndx  13270  slotsdnscsi  13271  dsndxntsetndx  13272  slotsdifdsndx  13273  basendxltunifndx  13277  unifndxntsetndx  13279  slotsdifunifndx  13280  mulg1  13681  mulg2  13683  mulgnndir  13703  setsmsdsg  15169  perfectlem1  15688  perfectlem2  15689  lgsdir2lem1  15722  lgsdir2lem4  15725  lgsdir2lem5  15726  lgsdir  15729  lgsne0  15732  lgs1  15738  lgsquad2lem2  15776  basendxltedgfndx  15826  trilpolemgt1  16467