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

Theorem onsucelsucexmid 4445
 Description: The converse of onsucelsucr 4424 implies excluded middle. On the other hand, if 𝑦 is constrained to be a natural number, instead of an arbitrary ordinal, then the converse of onsucelsucr 4424 does hold, as seen at nnsucelsuc 6387. (Contributed by Jim Kingdon, 2-Aug-2019.)
Hypothesis
Ref Expression
onsucelsucexmid.1 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
Assertion
Ref Expression
onsucelsucexmid (𝜑 ∨ ¬ 𝜑)
Distinct variable group:   𝜑,𝑥,𝑦

Proof of Theorem onsucelsucexmid
Dummy variable 𝑧 is distinct from all other variables.
StepHypRef Expression
1 onsucelsucexmidlem1 4443 . . . 4 ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
2 0elon 4314 . . . . . 6 ∅ ∈ On
3 onsucelsucexmidlem 4444 . . . . . 6 {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On
42, 3pm3.2i 270 . . . . 5 (∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On)
5 onsucelsucexmid.1 . . . . 5 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
6 eleq1 2202 . . . . . . 7 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
7 suceq 4324 . . . . . . . 8 (𝑥 = ∅ → suc 𝑥 = suc ∅)
87eleq1d 2208 . . . . . . 7 (𝑥 = ∅ → (suc 𝑥 ∈ suc 𝑦 ↔ suc ∅ ∈ suc 𝑦))
96, 8imbi12d 233 . . . . . 6 (𝑥 = ∅ → ((𝑥𝑦 → suc 𝑥 ∈ suc 𝑦) ↔ (∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦)))
10 eleq2 2203 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (∅ ∈ 𝑦 ↔ ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
11 suceq 4324 . . . . . . . 8 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc 𝑦 = suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
1211eleq2d 2209 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ suc 𝑦 ↔ suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1310, 12imbi12d 233 . . . . . 6 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ((∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦) ↔ (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})))
149, 13rspc2va 2803 . . . . 5 (((∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)) → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
154, 5, 14mp2an 422 . . . 4 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
161, 15ax-mp 5 . . 3 suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
17 elsuci 4325 . . 3 (suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1816, 17ax-mp 5 . 2 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
19 suc0 4333 . . . . . 6 suc ∅ = {∅}
20 p0ex 4112 . . . . . . 7 {∅} ∈ V
2120prid2 3630 . . . . . 6 {∅} ∈ {∅, {∅}}
2219, 21eqeltri 2212 . . . . 5 suc ∅ ∈ {∅, {∅}}
23 eqeq1 2146 . . . . . . 7 (𝑧 = suc ∅ → (𝑧 = ∅ ↔ suc ∅ = ∅))
2423orbi1d 780 . . . . . 6 (𝑧 = suc ∅ → ((𝑧 = ∅ ∨ 𝜑) ↔ (suc ∅ = ∅ ∨ 𝜑)))
2524elrab3 2841 . . . . 5 (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑)))
2622, 25ax-mp 5 . . . 4 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑))
27 0ex 4055 . . . . . . 7 ∅ ∈ V
28 nsuceq0g 4340 . . . . . . 7 (∅ ∈ V → suc ∅ ≠ ∅)
2927, 28ax-mp 5 . . . . . 6 suc ∅ ≠ ∅
30 df-ne 2309 . . . . . 6 (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
3129, 30mpbi 144 . . . . 5 ¬ suc ∅ = ∅
32 pm2.53 711 . . . . 5 ((suc ∅ = ∅ ∨ 𝜑) → (¬ suc ∅ = ∅ → 𝜑))
3331, 32mpi 15 . . . 4 ((suc ∅ = ∅ ∨ 𝜑) → 𝜑)
3426, 33sylbi 120 . . 3 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → 𝜑)
3519eqeq1i 2147 . . . . 5 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ {∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
3619eqeq1i 2147 . . . . . . . 8 (suc ∅ = ∅ ↔ {∅} = ∅)
3731, 36mtbi 659 . . . . . . 7 ¬ {∅} = ∅
3820elsn 3543 . . . . . . 7 ({∅} ∈ {∅} ↔ {∅} = ∅)
3937, 38mtbir 660 . . . . . 6 ¬ {∅} ∈ {∅}
40 eleq2 2203 . . . . . 6 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ({∅} ∈ {∅} ↔ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
4139, 40mtbii 663 . . . . 5 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4235, 41sylbi 120 . . . 4 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
43 olc 700 . . . . 5 (𝜑 → ({∅} = ∅ ∨ 𝜑))
44 eqeq1 2146 . . . . . . . 8 (𝑧 = {∅} → (𝑧 = ∅ ↔ {∅} = ∅))
4544orbi1d 780 . . . . . . 7 (𝑧 = {∅} → ((𝑧 = ∅ ∨ 𝜑) ↔ ({∅} = ∅ ∨ 𝜑)))
4645elrab3 2841 . . . . . 6 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑)))
4721, 46ax-mp 5 . . . . 5 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑))
4843, 47sylibr 133 . . . 4 (𝜑 → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4942, 48nsyl 617 . . 3 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ 𝜑)
5034, 49orim12i 748 . 2 ((suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}) → (𝜑 ∨ ¬ 𝜑))
5118, 50ax-mp 5 1 (𝜑 ∨ ¬ 𝜑)
 Colors of variables: wff set class Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   = wceq 1331   ∈ wcel 1480   ≠ wne 2308  ∀wral 2416  {crab 2420  Vcvv 2686  ∅c0 3363  {csn 3527  {cpr 3528  Oncon0 4285  suc csuc 4287 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-nul 4054  ax-pow 4098 This theorem depends on definitions:  df-bi 116  df-3an 964  df-tru 1334  df-nf 1437  df-sb 1736  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-rab 2425  df-v 2688  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-pw 3512  df-sn 3533  df-pr 3534  df-uni 3737  df-tr 4027  df-iord 4288  df-on 4290  df-suc 4293 This theorem is referenced by:  ordsucunielexmid  4446
 Copyright terms: Public domain W3C validator