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

Theorem 1nn 7925
 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 7916 . . . 4 ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
21eleq2i 2104 . . 3 (1 ∈ ℕ ↔ 1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
3 1re 7026 . . . 4 1 ∈ ℝ
4 elintg 3623 . . . 4 (1 ∈ ℝ → (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧))
53, 4ax-mp 7 . . 3 (1 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
62, 5bitri 173 . 2 (1 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}1 ∈ 𝑧)
7 vex 2560 . . . 4 𝑧 ∈ V
8 eleq2 2101 . . . . 5 (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
9 eleq2 2101 . . . . . 6 (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
109raleqbi1dv 2513 . . . . 5 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
118, 10anbi12d 442 . . . 4 (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧)))
127, 11elab 2687 . . 3 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
1312simplbi 259 . 2 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} → 1 ∈ 𝑧)
146, 13mprgbir 2379 1 1 ∈ ℕ
 Colors of variables: wff set class Syntax hints:   ∧ wa 97   ↔ wb 98   ∈ wcel 1393  {cab 2026  ∀wral 2306  ∩ cint 3615  (class class class)co 5512  ℝcr 6888  1c1 6890   + caddc 6892  ℕcn 7914 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-1re 6978 This theorem depends on definitions:  df-bi 110  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2311  df-v 2559  df-int 3616  df-inn 7915 This theorem is referenced by:  nnind  7930  nn1suc  7933  2nn  8077  1nn0  8197  nn0p1nn  8221  1z  8271  neg1z  8277  elz2  8312  nneoor  8340  indstr  8536  elnn1uz2  8544  zq  8561  qreccl  8576  expivallem  9256  exp1  9261  nnexpcl  9268  expnbnd  9372  resqrexlemf1  9606  resqrexlemcalc3  9614  resqrexlemnmsq  9615  resqrexlemnm  9616  resqrexlemcvg  9617  resqrexlemglsq  9620  resqrexlemga  9621
 Copyright terms: Public domain W3C validator