Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  1nn GIF version

Theorem 1nn 8754
 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.
StepHypRef Expression
1 dfnn2 8745 . . . 4 ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
21eleq2i 2207 . . 3 (1 ∈ ℕ ↔ 1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
3 1re 7788 . . . 4 1 ∈ ℝ
4 elintg 3786 . . . 4 (1 ∈ ℝ → (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
53, 4ax-mp 5 . . 3 (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
62, 5bitri 183 . 2 (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7 vex 2692 . . . 4 𝑧 ∈ V
8 eleq2 2204 . . . . 5 (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9 eleq2 2204 . . . . . 6 (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
109raleqbi1dv 2637 . . . . 5 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
118, 10anbi12d 465 . . . 4 (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧)))
127, 11elab 2831 . . 3 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
1312simplbi 272 . 2 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
146, 13mprgbir 2493 1 1 ∈ ℕ
 Colors of variables: wff set class Syntax hints:   ∧ wa 103   ↔ wb 104   ∈ wcel 1481  {cab 2126  ∀wral 2417  ∩ cint 3778  (class class class)co 5781  ℝcr 7642  1c1 7644   + caddc 7646  ℕcn 8743 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-1re 7737 This theorem depends on definitions:  df-bi 116  df-tru 1335  df-nf 1438  df-sb 1737  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ral 2422  df-v 2691  df-int 3779  df-inn 8744 This theorem is referenced by:  nnind  8759  nn1suc  8762  2nn  8904  1nn0  9016  nn0p1nn  9039  1z  9103  neg1z  9109  elz2  9145  nneoor  9176  9p1e10  9207  indstr  9414  elnn1uz2  9427  zq  9444  qreccl  9460  fz01or  9921  exp3vallem  10324  exp1  10329  nnexpcl  10336  expnbnd  10445  3dec  10491  fac1  10506  faccl  10512  faclbnd3  10520  resqrexlemf1  10811  resqrexlemcalc3  10819  resqrexlemnmsq  10820  resqrexlemnm  10821  resqrexlemcvg  10822  resqrexlemglsq  10825  resqrexlemga  10826  sumsnf  11209  cvgratnnlemnexp  11324  cvgratnnlemfm  11329  cvgratnnlemrate  11330  cvgratnn  11331  eftlub  11431  eirraplem  11517  n2dvds1  11643  ndvdsp1  11663  gcd1  11709  bezoutr1  11755  ncoprmgcdne1b  11804  1nprm  11829  1idssfct  11830  isprm2lem  11831  qden1elz  11917  phicl2  11924  phi1  11929  phiprm  11933  exmidunben  11973  base0  12045  baseval  12048  baseid  12049  basendx  12050  basendxnn  12051  1strstrg  12094  2strstrg  12096  basendxnplusgndx  12102  basendxnmulrndx  12110  rngstrg  12111  lmodstrd  12129  topgrpstrd  12147  setsmsdsg  12686  trilpolemgt1  13405
 Copyright terms: Public domain W3C validator