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

Theorem peano2 4216
Description: The successor of any natural number is a natural number. One of Peano's 5 postulates for arithmetic. Proposition 7.30(2) of [TakeutiZaring] p. 42. (Contributed by NM, 3-Sep-2003.)
Assertion
Ref Expression
peano2 (A 𝜔 → suc A 𝜔)

Proof of Theorem peano2
Dummy variables x y z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elex 2540 . 2 (A 𝜔 → A V)
2 ax-ia1 99 . . . . . 6 ((A V z {y ∣ (∅ y x y suc x y)}) → A V)
3 eleq1 2081 . . . . . . . 8 (x = A → (x zA z))
4 suceq 4059 . . . . . . . . 9 (x = A → suc x = suc A)
54eleq1d 2087 . . . . . . . 8 (x = A → (suc x z ↔ suc A z))
63, 5imbi12d 223 . . . . . . 7 (x = A → ((x z → suc x z) ↔ (A z → suc A z)))
76adantl 262 . . . . . 6 (((A V z {y ∣ (∅ y x y suc x y)}) x = A) → ((x z → suc x z) ↔ (A z → suc A z)))
8 df-clab 2008 . . . . . . . . 9 (z {y ∣ (∅ y x y suc x y)} ↔ [z / y](∅ y x y suc x y))
9 ax-ia2 100 . . . . . . . . . . . 12 ((∅ y x y suc x y) → x y suc x y)
10 df-ral 2286 . . . . . . . . . . . 12 (x y suc x yx(x y → suc x y))
119, 10sylib 127 . . . . . . . . . . 11 ((∅ y x y suc x y) → x(x y → suc x y))
1211sbimi 1630 . . . . . . . . . 10 ([z / y](∅ y x y suc x y) → [z / y]x(x y → suc x y))
13 sbim 1808 . . . . . . . . . . . 12 ([z / y](x y → suc x y) ↔ ([z / y]x y → [z / y]suc x y))
14 elsb4 1834 . . . . . . . . . . . . 13 ([z / y]x yx z)
15 clelsb4 2124 . . . . . . . . . . . . 13 ([z / y]suc x y ↔ suc x z)
1614, 15imbi12i 228 . . . . . . . . . . . 12 (([z / y]x y → [z / y]suc x y) ↔ (x z → suc x z))
1713, 16bitri 173 . . . . . . . . . . 11 ([z / y](x y → suc x y) ↔ (x z → suc x z))
1817sbalv 1862 . . . . . . . . . 10 ([z / y]x(x y → suc x y) ↔ x(x z → suc x z))
1912, 18sylib 127 . . . . . . . . 9 ([z / y](∅ y x y suc x y) → x(x z → suc x z))
208, 19sylbi 114 . . . . . . . 8 (z {y ∣ (∅ y x y suc x y)} → x(x z → suc x z))
212019.21bi 1435 . . . . . . 7 (z {y ∣ (∅ y x y suc x y)} → (x z → suc x z))
2221adantl 262 . . . . . 6 ((A V z {y ∣ (∅ y x y suc x y)}) → (x z → suc x z))
23 nfv 1404 . . . . . . 7 x A V
24 nfv 1404 . . . . . . . . 9 x y
25 nfra1 2330 . . . . . . . . 9 xx y suc x y
2624, 25nfan 1442 . . . . . . . 8 x(∅ y x y suc x y)
2726nfsab 2013 . . . . . . 7 x z {y ∣ (∅ y x y suc x y)}
2823, 27nfan 1442 . . . . . 6 x(A V z {y ∣ (∅ y x y suc x y)})
29 nfcvd 2160 . . . . . 6 ((A V z {y ∣ (∅ y x y suc x y)}) → xA)
30 nfvd 1405 . . . . . 6 ((A V z {y ∣ (∅ y x y suc x y)}) → Ⅎx(A z → suc A z))
312, 7, 22, 28, 29, 30vtocldf 2579 . . . . 5 ((A V z {y ∣ (∅ y x y suc x y)}) → (A z → suc A z))
3231ralrimiva 2367 . . . 4 (A V → z {y ∣ (∅ y x y suc x y)} (A z → suc A z))
33 ralim 2355 . . . . 5 (z {y ∣ (∅ y x y suc x y)} (A z → suc A z) → (z {y ∣ (∅ y x y suc x y)}A zz {y ∣ (∅ y x y suc x y)}suc A z))
34 elintg 3570 . . . . . 6 (A V → (A {y ∣ (∅ y x y suc x y)} ↔ z {y ∣ (∅ y x y suc x y)}A z))
35 sucexg 4145 . . . . . . 7 (A V → suc A V)
36 elintg 3570 . . . . . . 7 (suc A V → (suc A {y ∣ (∅ y x y suc x y)} ↔ z {y ∣ (∅ y x y suc x y)}suc A z))
3735, 36syl 14 . . . . . 6 (A V → (suc A {y ∣ (∅ y x y suc x y)} ↔ z {y ∣ (∅ y x y suc x y)}suc A z))
3834, 37imbi12d 223 . . . . 5 (A V → ((A {y ∣ (∅ y x y suc x y)} → suc A {y ∣ (∅ y x y suc x y)}) ↔ (z {y ∣ (∅ y x y suc x y)}A zz {y ∣ (∅ y x y suc x y)}suc A z)))
3933, 38syl5ibr 145 . . . 4 (A V → (z {y ∣ (∅ y x y suc x y)} (A z → suc A z) → (A {y ∣ (∅ y x y suc x y)} → suc A {y ∣ (∅ y x y suc x y)})))
4032, 39mpd 13 . . 3 (A V → (A {y ∣ (∅ y x y suc x y)} → suc A {y ∣ (∅ y x y suc x y)}))
41 dfom3 4213 . . . 4 𝜔 = {y ∣ (∅ y x y suc x y)}
4241eleq2i 2085 . . 3 (A 𝜔 ↔ A {y ∣ (∅ y x y suc x y)})
4341eleq2i 2085 . . 3 (suc A 𝜔 ↔ suc A {y ∣ (∅ y x y suc x y)})
4440, 42, 433imtr4g 194 . 2 (A V → (A 𝜔 → suc A 𝜔))
451, 44mpcom 32 1 (A 𝜔 → suc A 𝜔)
Colors of variables: wff set class
Syntax hints:  wi 4   wa 97  wb 98  wal 1228   = wceq 1230   wcel 1376  [wsb 1628  {cab 2007  wral 2281  Vcvv 2532  c0 3198   cint 3562  suc csuc 4023  𝜔com 4211
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 617  ax-5 1318  ax-7 1319  ax-gen 1320  ax-ie1 1365  ax-ie2 1366  ax-8 1378  ax-10 1379  ax-11 1380  ax-i12 1381  ax-bnd 1382  ax-4 1383  ax-13 1387  ax-14 1388  ax-17 1402  ax-i9 1406  ax-ial 1411  ax-i5r 1412  ax-ext 2003  ax-sep 3822  ax-pow 3874  ax-pr 3891  ax-un 4091
This theorem depends on definitions:  df-bi 110  df-3an 877  df-tru 1233  df-nf 1332  df-sb 1629  df-clab 2008  df-cleq 2014  df-clel 2017  df-nfc 2148  df-ral 2286  df-rex 2287  df-v 2534  df-un 2896  df-in 2898  df-ss 2905  df-pw 3309  df-sn 3329  df-pr 3330  df-uni 3528  df-int 3563  df-suc 4028  df-iom 4212
This theorem is referenced by:  peano5  4219  limom  4234  peano2b  4235  nnregexmid  4240  frecsuclem1  5871  frecsuclem3  5874  frecrdg  5876  nnacl  5942  nnacom  5946  nnmsucr  5950  nnsucsssuc  5953  nnaword  5962  1onn  5971  2onn  5972  3onn  5973  4onn  5974  nnaordex  5978
  Copyright terms: Public domain W3C validator