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

Theorem nnsucelsuc 6182
Description: Membership is inherited by successors. The reverse direction holds for all ordinals, as seen at onsucelsucr 4287, but the forward direction, for all ordinals, implies excluded middle as seen as onsucelsucexmid 4308. (Contributed by Jim Kingdon, 25-Aug-2019.)
Assertion
Ref Expression
nnsucelsuc (𝐵 ∈ ω → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))

Proof of Theorem nnsucelsuc
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eleq2 2146 . . . 4 (𝑥 = ∅ → (𝐴𝑥𝐴 ∈ ∅))
2 suceq 4192 . . . . 5 (𝑥 = ∅ → suc 𝑥 = suc ∅)
32eleq2d 2152 . . . 4 (𝑥 = ∅ → (suc 𝐴 ∈ suc 𝑥 ↔ suc 𝐴 ∈ suc ∅))
41, 3imbi12d 232 . . 3 (𝑥 = ∅ → ((𝐴𝑥 → suc 𝐴 ∈ suc 𝑥) ↔ (𝐴 ∈ ∅ → suc 𝐴 ∈ suc ∅)))
5 eleq2 2146 . . . 4 (𝑥 = 𝑦 → (𝐴𝑥𝐴𝑦))
6 suceq 4192 . . . . 5 (𝑥 = 𝑦 → suc 𝑥 = suc 𝑦)
76eleq2d 2152 . . . 4 (𝑥 = 𝑦 → (suc 𝐴 ∈ suc 𝑥 ↔ suc 𝐴 ∈ suc 𝑦))
85, 7imbi12d 232 . . 3 (𝑥 = 𝑦 → ((𝐴𝑥 → suc 𝐴 ∈ suc 𝑥) ↔ (𝐴𝑦 → suc 𝐴 ∈ suc 𝑦)))
9 eleq2 2146 . . . 4 (𝑥 = suc 𝑦 → (𝐴𝑥𝐴 ∈ suc 𝑦))
10 suceq 4192 . . . . 5 (𝑥 = suc 𝑦 → suc 𝑥 = suc suc 𝑦)
1110eleq2d 2152 . . . 4 (𝑥 = suc 𝑦 → (suc 𝐴 ∈ suc 𝑥 ↔ suc 𝐴 ∈ suc suc 𝑦))
129, 11imbi12d 232 . . 3 (𝑥 = suc 𝑦 → ((𝐴𝑥 → suc 𝐴 ∈ suc 𝑥) ↔ (𝐴 ∈ suc 𝑦 → suc 𝐴 ∈ suc suc 𝑦)))
13 eleq2 2146 . . . 4 (𝑥 = 𝐵 → (𝐴𝑥𝐴𝐵))
14 suceq 4192 . . . . 5 (𝑥 = 𝐵 → suc 𝑥 = suc 𝐵)
1514eleq2d 2152 . . . 4 (𝑥 = 𝐵 → (suc 𝐴 ∈ suc 𝑥 ↔ suc 𝐴 ∈ suc 𝐵))
1613, 15imbi12d 232 . . 3 (𝑥 = 𝐵 → ((𝐴𝑥 → suc 𝐴 ∈ suc 𝑥) ↔ (𝐴𝐵 → suc 𝐴 ∈ suc 𝐵)))
17 noel 3273 . . . 4 ¬ 𝐴 ∈ ∅
1817pm2.21i 608 . . 3 (𝐴 ∈ ∅ → suc 𝐴 ∈ suc ∅)
19 elsuci 4193 . . . . . . . 8 (𝐴 ∈ suc 𝑦 → (𝐴𝑦𝐴 = 𝑦))
2019adantl 271 . . . . . . 7 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → (𝐴𝑦𝐴 = 𝑦))
21 simpl 107 . . . . . . . 8 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → (𝐴𝑦 → suc 𝐴 ∈ suc 𝑦))
22 suceq 4192 . . . . . . . . 9 (𝐴 = 𝑦 → suc 𝐴 = suc 𝑦)
2322a1i 9 . . . . . . . 8 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → (𝐴 = 𝑦 → suc 𝐴 = suc 𝑦))
2421, 23orim12d 733 . . . . . . 7 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → ((𝐴𝑦𝐴 = 𝑦) → (suc 𝐴 ∈ suc 𝑦 ∨ suc 𝐴 = suc 𝑦)))
2520, 24mpd 13 . . . . . 6 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → (suc 𝐴 ∈ suc 𝑦 ∨ suc 𝐴 = suc 𝑦))
26 vex 2615 . . . . . . . 8 𝑦 ∈ V
2726sucex 4278 . . . . . . 7 suc 𝑦 ∈ V
2827elsuc2 4197 . . . . . 6 (suc 𝐴 ∈ suc suc 𝑦 ↔ (suc 𝐴 ∈ suc 𝑦 ∨ suc 𝐴 = suc 𝑦))
2925, 28sylibr 132 . . . . 5 (((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) ∧ 𝐴 ∈ suc 𝑦) → suc 𝐴 ∈ suc suc 𝑦)
3029ex 113 . . . 4 ((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) → (𝐴 ∈ suc 𝑦 → suc 𝐴 ∈ suc suc 𝑦))
3130a1i 9 . . 3 (𝑦 ∈ ω → ((𝐴𝑦 → suc 𝐴 ∈ suc 𝑦) → (𝐴 ∈ suc 𝑦 → suc 𝐴 ∈ suc suc 𝑦)))
324, 8, 12, 16, 18, 31finds 4377 . 2 (𝐵 ∈ ω → (𝐴𝐵 → suc 𝐴 ∈ suc 𝐵))
33 nnon 4386 . . 3 (𝐵 ∈ ω → 𝐵 ∈ On)
34 onsucelsucr 4287 . . 3 (𝐵 ∈ On → (suc 𝐴 ∈ suc 𝐵𝐴𝐵))
3533, 34syl 14 . 2 (𝐵 ∈ ω → (suc 𝐴 ∈ suc 𝐵𝐴𝐵))
3632, 35impbid 127 1 (𝐵 ∈ ω → (𝐴𝐵 ↔ suc 𝐴 ∈ suc 𝐵))
Colors of variables: wff set class
Syntax hints:  wi 4  wa 102  wb 103  wo 662   = wceq 1285  wcel 1434  c0 3269  Oncon0 4153  suc csuc 4155  ωcom 4367
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 577  ax-in2 578  ax-io 663  ax-5 1377  ax-7 1378  ax-gen 1379  ax-ie1 1423  ax-ie2 1424  ax-8 1436  ax-10 1437  ax-11 1438  ax-i12 1439  ax-bndl 1440  ax-4 1441  ax-13 1445  ax-14 1446  ax-17 1460  ax-i9 1464  ax-ial 1468  ax-i5r 1469  ax-ext 2065  ax-sep 3922  ax-nul 3930  ax-pow 3974  ax-pr 3999  ax-un 4223  ax-iinf 4365
This theorem depends on definitions:  df-bi 115  df-3an 922  df-tru 1288  df-nf 1391  df-sb 1688  df-clab 2070  df-cleq 2076  df-clel 2079  df-nfc 2212  df-ral 2358  df-rex 2359  df-v 2614  df-dif 2986  df-un 2988  df-in 2990  df-ss 2997  df-nul 3270  df-pw 3408  df-sn 3428  df-pr 3429  df-uni 3628  df-int 3663  df-tr 3902  df-iord 4156  df-on 4158  df-suc 4161  df-iom 4368
This theorem is referenced by:  nnsucsssuc  6183  nntri3or  6184  nnsucuniel  6186  nnaordi  6195
  Copyright terms: Public domain W3C validator