Theorem 1nn 8589

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 8580	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2166	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 7637	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3726	. . . 4 ⊢ (1 ∈ ℝ → (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
5	3, 4	ax-mp 7	. . 3 ⊢ (1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
6	2, 5	bitri 183	. 2 ⊢ (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7		vex 2644	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2163	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2163	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2592	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 460	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2782	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 270	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2449	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 103   ↔ wb 104   ∈ wcel 1448  {cab 2086  ∀wral 2375  ∩ cint 3718  (class class class)co 5706  ℝcr 7499  1c1 7501   + caddc 7503  ℕcn 8578

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 671  ax-5 1391  ax-7 1392  ax-gen 1393  ax-ie1 1437  ax-ie2 1438  ax-8 1450  ax-10 1451  ax-11 1452  ax-i12 1453  ax-bndl 1454  ax-4 1455  ax-17 1474  ax-i9 1478  ax-ial 1482  ax-i5r 1483  ax-ext 2082  ax-1re 7589

This theorem depends on definitions:  df-bi 116  df-tru 1302  df-nf 1405  df-sb 1704  df-clab 2087  df-cleq 2093  df-clel 2096  df-nfc 2229  df-ral 2380  df-v 2643  df-int 3719  df-inn 8579

This theorem is referenced by:  nnind  8594  nn1suc  8597  2nn  8733  1nn0  8845  nn0p1nn  8868  1z  8932  neg1z  8938  elz2  8974  nneoor  9005  9p1e10  9036  indstr  9238  elnn1uz2  9251  zq  9268  qreccl  9284  fz01or  9732  exp3vallem  10135  exp1  10140  nnexpcl  10147  expnbnd  10256  3dec  10302  fac1  10316  faccl  10322  faclbnd3  10330  resqrexlemf1  10620  resqrexlemcalc3  10628  resqrexlemnmsq  10629  resqrexlemnm  10630  resqrexlemcvg  10631  resqrexlemglsq  10634  resqrexlemga  10635  sumsnf  11017  cvgratnnlemnexp  11132  cvgratnnlemfm  11137  cvgratnnlemrate  11138  cvgratnn  11139  eftlub  11194  eirraplem  11278  n2dvds1  11404  ndvdsp1  11424  gcd1  11470  bezoutr1  11514  ncoprmgcdne1b  11563  1nprm  11588  1idssfct  11589  isprm2lem  11590  qden1elz  11675  phicl2  11682  phi1  11687  phiprm  11691  exmidunben  11731  base0  11790  baseval  11793  baseid  11794  basendx  11795  basendxnn  11796  1strstrg  11839  2strstrg  11841  basendxnplusgndx  11847  basendxnmulrndx  11855  rngstrg  11856  lmodstrd  11874  topgrpstrd  11892  setsmsdsg  12408  trilpolemgt1  12816