Theorem 1nn 9265

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 9256	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2301	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8289	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3962	. . . 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 2818	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2298	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2298	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2755	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 473	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2964	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2602	1 ⊢ 1 ∈ ℕ

Syntax hints:   ∧ wa 104   ↔ wb 105   ∈ wcel 2205  {cab 2220  ∀wral 2522  ∩ cint 3954  (class class class)co 6058  ℝcr 8142  1c1 8144   + caddc 8146  ℕcn 9254

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2216  ax-1re 8237

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2221  df-cleq 2227  df-clel 2230  df-nfc 2375  df-ral 2527  df-v 2817  df-int 3955  df-inn 9255

This theorem is referenced by:  nnind  9270  nn1suc  9273  2nn  9416  1nn0  9529  nn0p1nn  9552  1z  9620  neg1z  9626  elz2  9666  nneoor  9698  9p1e10  9729  indstr  9943  elnn1uz2  9957  zq  9976  qreccl  9992  fz01or  10467  exp3vallem  10926  exp1  10931  nnexpcl  10938  expnbnd  11050  3dec  11101  fac1  11116  faccl  11122  faclbnd3  11130  fiubnn  11222  lsw0  11297  cats1un  11438  cats1fvn  11481  cats1fvnd  11482  resqrexlemf1  11718  resqrexlemcalc3  11726  resqrexlemnmsq  11727  resqrexlemnm  11728  resqrexlemcvg  11729  resqrexlemglsq  11732  resqrexlemga  11733  sumsnf  12120  cvgratnnlemnexp  12235  cvgratnnlemfm  12240  cvgratnnlemrate  12241  cvgratnn  12242  prodsnf  12303  fprodnncl  12321  eftlub  12401  eirraplem  12488  n2dvds1  12623  ndvdsp1  12643  5ndvds6  12646  gcd1  12708  bezoutr1  12754  ncoprmgcdne1b  12811  1nprm  12836  1idssfct  12837  isprm2lem  12838  qden1elz  12927  phicl2  12936  phi1  12941  phiprm  12945  eulerthlema  12952  pcpre1  13015  pczpre  13020  pcmptcl  13065  pcmpt  13066  infpnlem2  13083  mul4sq  13117  ballotfilem4  13185  ballotfilemi1  13189  ballotfilemii  13190  ballotfilemic  13194  ballotfilem1c  13195  exmidunben  13261  nninfdc  13288  base0  13346  baseval  13349  baseid  13350  basendx  13351  basendxnn  13352  1strstrg  13413  2strstrg  13416  basendxnplusgndx  13422  basendxnmulrndx  13431  rngstrg  13432  lmodstrd  13461  topgrpstrd  13493  ocndx  13508  ocid  13509  basendxnocndx  13510  plendxnocndx  13511  basendxltdsndx  13516  dsndxnplusgndx  13518  dsndxnmulrndx  13519  slotsdnscsi  13520  dsndxntsetndx  13521  slotsdifdsndx  13522  basendxltunifndx  13526  unifndxntsetndx  13528  slotsdifunifndx  13529  mulg1  13882  mulg2  13884  mulgnndir  13904  setsmsdsg  15471  perfectlem1  15993  perfectlem2  15994  lgsdir2lem1  16027  lgsdir2lem4  16030  lgsdir2lem5  16031  lgsdir  16034  lgsne0  16037  lgs1  16043  lgsquad2lem2  16081  basendxltedgfndx  16131  clwwlkn1  16539  konigsberglem1  16609  trilpolemgt1  16949