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

Theorem peano2nn 8930
Description: Peano postulate: a successor of a positive integer is a positive integer. (Contributed by NM, 11-Jan-1997.) (Revised by Mario Carneiro, 17-Nov-2014.)
Assertion
Ref Expression
peano2nn (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)

Proof of Theorem peano2nn
Dummy variables 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 dfnn2 8920 . . . . . 6 ℕ = {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}
21eleq2i 2244 . . . . 5 (𝐴 ∈ ℕ ↔ 𝐴 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
3 elintg 3852 . . . . 5 (𝐴 ∈ ℕ → (𝐴 {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴𝑧))
42, 3bitrid 192 . . . 4 (𝐴 ∈ ℕ → (𝐴 ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴𝑧))
54ibi 176 . . 3 (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴𝑧)
6 vex 2740 . . . . . . . 8 𝑧 ∈ V
7 eleq2 2241 . . . . . . . . 9 (𝑥 = 𝑧 → (1 ∈ 𝑥 ↔ 1 ∈ 𝑧))
8 eleq2 2241 . . . . . . . . . 10 (𝑥 = 𝑧 → ((𝑦 + 1) ∈ 𝑥 ↔ (𝑦 + 1) ∈ 𝑧))
98raleqbi1dv 2680 . . . . . . . . 9 (𝑥 = 𝑧 → (∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥 ↔ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
107, 9anbi12d 473 . . . . . . . 8 (𝑥 = 𝑧 → ((1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥) ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧)))
116, 10elab 2881 . . . . . . 7 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ (1 ∈ 𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧))
1211simprbi 275 . . . . . 6 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} → ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧)
13 oveq1 5881 . . . . . . . 8 (𝑦 = 𝐴 → (𝑦 + 1) = (𝐴 + 1))
1413eleq1d 2246 . . . . . . 7 (𝑦 = 𝐴 → ((𝑦 + 1) ∈ 𝑧 ↔ (𝐴 + 1) ∈ 𝑧))
1514rspcva 2839 . . . . . 6 ((𝐴𝑧 ∧ ∀𝑦𝑧 (𝑦 + 1) ∈ 𝑧) → (𝐴 + 1) ∈ 𝑧)
1612, 15sylan2 286 . . . . 5 ((𝐴𝑧𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}) → (𝐴 + 1) ∈ 𝑧)
1716expcom 116 . . . 4 (𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} → (𝐴𝑧 → (𝐴 + 1) ∈ 𝑧))
1817ralimia 2538 . . 3 (∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)}𝐴𝑧 → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
195, 18syl 14 . 2 (𝐴 ∈ ℕ → ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧)
20 nnre 8925 . . . 4 (𝐴 ∈ ℕ → 𝐴 ∈ ℝ)
21 1red 7971 . . . 4 (𝐴 ∈ ℕ → 1 ∈ ℝ)
2220, 21readdcld 7986 . . 3 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℝ)
231eleq2i 2244 . . . 4 ((𝐴 + 1) ∈ ℕ ↔ (𝐴 + 1) ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)})
24 elintg 3852 . . . 4 ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
2523, 24bitrid 192 . . 3 ((𝐴 + 1) ∈ ℝ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
2622, 25syl 14 . 2 (𝐴 ∈ ℕ → ((𝐴 + 1) ∈ ℕ ↔ ∀𝑧 ∈ {𝑥 ∣ (1 ∈ 𝑥 ∧ ∀𝑦𝑥 (𝑦 + 1) ∈ 𝑥)} (𝐴 + 1) ∈ 𝑧))
2719, 26mpbird 167 1 (𝐴 ∈ ℕ → (𝐴 + 1) ∈ ℕ)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104  wb 105   = wceq 1353  wcel 2148  {cab 2163  wral 2455   cint 3844  (class class class)co 5874  cr 7809  1c1 7811   + caddc 7813  cn 8918
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 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-ext 2159  ax-sep 4121  ax-cnex 7901  ax-resscn 7902  ax-1re 7904  ax-addrcl 7907
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-nf 1461  df-sb 1763  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ral 2460  df-rex 2461  df-v 2739  df-un 3133  df-in 3135  df-ss 3142  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-int 3845  df-br 4004  df-iota 5178  df-fv 5224  df-ov 5877  df-inn 8919
This theorem is referenced by:  peano2nnd  8933  nnind  8934  nnaddcl  8938  2nn  9079  3nn  9080  4nn  9081  5nn  9082  6nn  9083  7nn  9084  8nn  9085  9nn  9086  nneoor  9354  10nn  9398  nnsplit  10136  fzonn0p1p1  10212  expp1  10526  facp1  10709  resqrexlemfp1  11017  resqrexlemcalc3  11024  trireciplem  11507  trirecip  11508  cvgratnnlemnexp  11531  cvgratz  11539  nno  11910  nnoddm1d2  11914  rplpwr  12027  prmind2  12119  sqrt2irr  12161  pcmpt  12340  pockthi  12355  mulgnnp1  12990  2sqlem10  14442
  Copyright terms: Public domain W3C validator