Theorem 1nn 8930

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 8921	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2244	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 7956	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3853	. . . 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 2741	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2241	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2241	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2681	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2882	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2535	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2148  {cab 2163  ∀wral 2455  ∩ cint 3845  (class class class)co 5875  ℝcr 7810  1c1 7812   + caddc 7814  ℕcn 8919

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 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-1re 7905

This theorem depends on definitions:  df-bi 117  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-v 2740  df-int 3846  df-inn 8920

This theorem is referenced by:  nnind  8935  nn1suc  8938  2nn  9080  1nn0  9192  nn0p1nn  9215  1z  9279  neg1z  9285  elz2  9324  nneoor  9355  9p1e10  9386  indstr  9593  elnn1uz2  9607  zq  9626  qreccl  9642  fz01or  10111  exp3vallem  10521  exp1  10526  nnexpcl  10533  expnbnd  10644  3dec  10694  fac1  10709  faccl  10715  faclbnd3  10723  fiubnn  10810  resqrexlemf1  11017  resqrexlemcalc3  11025  resqrexlemnmsq  11026  resqrexlemnm  11027  resqrexlemcvg  11028  resqrexlemglsq  11031  resqrexlemga  11032  sumsnf  11417  cvgratnnlemnexp  11532  cvgratnnlemfm  11537  cvgratnnlemrate  11538  cvgratnn  11539  prodsnf  11600  fprodnncl  11618  eftlub  11698  eirraplem  11784  n2dvds1  11917  ndvdsp1  11937  gcd1  11988  bezoutr1  12034  ncoprmgcdne1b  12089  1nprm  12114  1idssfct  12115  isprm2lem  12116  qden1elz  12205  phicl2  12214  phi1  12219  phiprm  12223  eulerthlema  12230  pcpre1  12292  pczpre  12297  pcmptcl  12340  pcmpt  12341  infpnlem2  12358  mul4sq  12392  exmidunben  12427  nninfdc  12454  base0  12512  baseval  12515  baseid  12516  basendx  12517  basendxnn  12518  1strstrg  12575  2strstrg  12577  basendxnplusgndx  12583  basendxnmulrndx  12592  rngstrg  12593  lmodstrd  12622  topgrpstrd  12651  basendxltdsndx  12670  dsndxnplusgndx  12672  dsndxnmulrndx  12673  slotsdnscsi  12674  dsndxntsetndx  12675  slotsdifdsndx  12676  basendxltunifndx  12680  unifndxntsetndx  12682  slotsdifunifndx  12683  mulg1  12990  mulg2  12992  mulgnndir  13012  cnfldstr  13460  setsmsdsg  13983  lgsdir2lem1  14432  lgsdir2lem4  14435  lgsdir2lem5  14436  lgsdir  14439  lgsne0  14442  lgs1  14448  trilpolemgt1  14790