Theorem 1nn 9318

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 9309	. . . 4 ⊢ ℕ = ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)}
2	1	eleq2i 2305	. . 3 ⊢ (1 ∈ ℕ ↔ 1 ∈ ∩ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)})
3		1re 8326	. . . 4 ⊢ 1 ∈ ℝ
4		elintg 3978	. . . 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 2824	. . . 4 ⊢ 𝑧 ∈ V
8		eleq2 2302	. . . . 5 ⊢ (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9		eleq2 2302	. . . . . 6 ⊢ (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
10	9	raleqbi1dv 2761	. . . . 5 ⊢ (𝑥 = 𝑧 → (∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
11	8, 10	anbi12d 477	. . . 4 ⊢ (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧)))
12	7, 11	elab 2970	. . 3 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦 ∈ 𝑧 (𝑦 + 1) ∈ 𝑧))
13	12	simplbi 274	. 2 ⊢ (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦 ∈ 𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
14	6, 13	mprgbir 2608	1 ⊢ 1 ∈ ℕ

This proof depends on syntax axioms:   ∧ wa 104   ↔ wb 105   ∈ wcel 2209  {cab 2224  ∀wral 2528  ∩ cint 3970  (class class class)co 6085  ℝcr 8179  1c1 8181   + caddc 8183  ℕcn 9307

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-ext 2220  ax-1re 8274

This proof depends on definitions:  df-bi 117  df-tru 1405  df-nf 1514  df-sb 1816  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ral 2533  df-v 2823  df-int 3971  df-inn 9308

This theorem is used by:  nnind  9323  nn1suc  9326  2nn  9471  1nn0  9584  nn0p1nn  9607  1z  9675  neg1z  9681  elz2  9721  nneoor  9753  9p1e10  9784  11nn  9806  indstr  10003  elnn1uz2  10017  zq  10036  qreccl  10052  fz01or  10529  exp3vallem  10992  exp1  10997  nnexpcl  11004  expnbnd  11116  3dec  11168  fac1  11183  faccl  11189  faclbnd3  11197  fiubnn  11289  lsw0  11368  cats1un  11509  cats1fvn  11552  cats1fvnd  11553  resqrexlemf1  11790  resqrexlemcalc3  11798  resqrexlemnmsq  11799  resqrexlemnm  11800  resqrexlemcvg  11801  resqrexlemglsq  11804  resqrexlemga  11805  sumsnf  12195  cvgratnnlemnexp  12310  cvgratnnlemfm  12315  cvgratnnlemrate  12316  cvgratnn  12317  prodsnf  12378  fprodnncl  12396  eftlub  12476  eirraplem  12563  n2dvds1  12698  ndvdsp1  12718  5ndvds6  12721  gcd1  12783  bezoutr1  12829  ncoprmgcdne1b  12886  1nprm  12911  1idssfct  12912  isprm2lem  12913  qden1elz  13004  phicl2  13015  phi1  13020  phiprm  13024  eulerthlema  13031  pcpre1  13094  pczpre  13099  pcmptcl  13144  pcmpt  13145  infpnlem2  13162  mul4sq  13196  5prm  13246  7prm  13248  10nprm  13251  11prm  13252  13prm  13253  17prm  13254  19prm  13255  37prm  13258  43prm  13259  83prm  13260  139prm  13261  163prm  13262  317prm  13263  631prm  13264  1259lem4  13268  1259lem5  13269  1259prm  13270  ballotfilem4  13293  ballotfilemi1  13297  ballotfilemii  13298  ballotfilemic  13302  ballotfilem1c  13303  exmidunben  13369  nninfdc  13396  base0  13454  baseval  13457  baseid  13458  basendx  13459  basendxnn  13460  1strstrg  13523  2strstrg  13526  basendxnplusgndx  13532  basendxnmulrndx  13541  rngstrg  13542  lmodstrd  13571  topgrpstrd  13603  ocndx  13618  ocid  13619  basendxnocndx  13620  plendxnocndx  13621  basendxltdsndx  13626  dsndxnplusgndx  13628  dsndxnmulrndx  13629  slotsdnscsi  13630  dsndxntsetndx  13631  slotsdifdsndx  13632  basendxltunifndx  13636  unifndxntsetndx  13638  slotsdifunifndx  13639  mulg1  13985  mulg2  13987  mulgnndir  14007  setsmsdsg  15672  logfac  16090  log2ublog2  16185  efnnfsumcl  16200  efchtqdvds  16226  prmorcht  16243  perfectlem1  16260  perfectlem2  16261  bpos1  16271  bposlem5  16276  lgsdir2lem1  16313  lgsdir2lem4  16316  lgsdir2lem5  16317  lgsdir  16320  lgsne0  16323  lgs1  16329  lgsquad2lem2  16367  basendxltedgfndx  16417  clwwlkn1  16825  konigsberglem1  16895  trilpolemgt1  17255