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

Theorem 1nn 7971
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 7962 . . . 4 ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
21eleq2i 2118 . . 3 (1 ∈ ℕ ↔ 1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
3 1re 7054 . . . 4 1 ∈ ℝ
4 elintg 3648 . . . 4 (1 ∈ ℝ → (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
53, 4ax-mp 7 . . 3 (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
62, 5bitri 177 . 2 (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7 vex 2575 . . . 4 𝑧 ∈ V
8 eleq2 2115 . . . . 5 (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9 eleq2 2115 . . . . . 6 (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
109raleqbi1dv 2528 . . . . 5 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
118, 10anbi12d 450 . . . 4 (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧)))
127, 11elab 2707 . . 3 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
1312simplbi 263 . 2 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
146, 13mprgbir 2394 1 1 ∈ ℕ
Colors of variables: wff set class
Syntax hints:  wa 101  wb 102  wcel 1407  {cab 2040  wral 2321   cint 3640  (class class class)co 5537  cr 6916  1c1 6918   + caddc 6920  cn 7960
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 103  ax-ia2 104  ax-ia3 105  ax-io 638  ax-5 1350  ax-7 1351  ax-gen 1352  ax-ie1 1396  ax-ie2 1397  ax-8 1409  ax-10 1410  ax-11 1411  ax-i12 1412  ax-bndl 1413  ax-4 1414  ax-17 1433  ax-i9 1437  ax-ial 1441  ax-i5r 1442  ax-ext 2036  ax-1re 7006
This theorem depends on definitions:  df-bi 114  df-tru 1260  df-nf 1364  df-sb 1660  df-clab 2041  df-cleq 2047  df-clel 2050  df-nfc 2181  df-ral 2326  df-v 2574  df-int 3641  df-inn 7961
This theorem is referenced by:  nnind  7976  nn1suc  7979  2nn  8114  1nn0  8225  nn0p1nn  8248  1z  8298  neg1z  8304  elz2  8340  nneoor  8369  9p1e10  8399  indstr  8602  elnn1uz2  8611  zq  8628  qreccl  8644  expivallem  9386  exp1  9391  nnexpcl  9398  expnbnd  9504  3dec  9550  fac1  9561  faccl  9567  faclbnd3  9575  resqrexlemf1  9798  resqrexlemcalc3  9806  resqrexlemnmsq  9807  resqrexlemnm  9808  resqrexlemcvg  9809  resqrexlemglsq  9812  resqrexlemga  9813  fz01or  10153  n2dvds1  10187
  Copyright terms: Public domain W3C validator