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

Theorem onsucelsucexmid 4374
Description: The converse of onsucelsucr 4353 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 4353 does hold, as seen at nnsucelsuc 6292. (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 4372 . . . 4 ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
2 0elon 4243 . . . . . 6 ∅ ∈ On
3 onsucelsucexmidlem 4373 . . . . . 6 {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On
42, 3pm3.2i 267 . . . . 5 (∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On)
5 onsucelsucexmid.1 . . . . 5 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
6 eleq1 2157 . . . . . . 7 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
7 suceq 4253 . . . . . . . 8 (𝑥 = ∅ → suc 𝑥 = suc ∅)
87eleq1d 2163 . . . . . . 7 (𝑥 = ∅ → (suc 𝑥 ∈ suc 𝑦 ↔ suc ∅ ∈ suc 𝑦))
96, 8imbi12d 233 . . . . . 6 (𝑥 = ∅ → ((𝑥𝑦 → suc 𝑥 ∈ suc 𝑦) ↔ (∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦)))
10 eleq2 2158 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (∅ ∈ 𝑦 ↔ ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
11 suceq 4253 . . . . . . . 8 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc 𝑦 = suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
1211eleq2d 2164 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ suc 𝑦 ↔ suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1310, 12imbi12d 233 . . . . . 6 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ((∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦) ↔ (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})))
149, 13rspc2va 2749 . . . . 5 (((∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)) → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
154, 5, 14mp2an 418 . . . 4 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
161, 15ax-mp 7 . . 3 suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
17 elsuci 4254 . . 3 (suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1816, 17ax-mp 7 . 2 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
19 suc0 4262 . . . . . 6 suc ∅ = {∅}
20 p0ex 4044 . . . . . . 7 {∅} ∈ V
2120prid2 3569 . . . . . 6 {∅} ∈ {∅, {∅}}
2219, 21eqeltri 2167 . . . . 5 suc ∅ ∈ {∅, {∅}}
23 eqeq1 2101 . . . . . . 7 (𝑧 = suc ∅ → (𝑧 = ∅ ↔ suc ∅ = ∅))
2423orbi1d 743 . . . . . 6 (𝑧 = suc ∅ → ((𝑧 = ∅ ∨ 𝜑) ↔ (suc ∅ = ∅ ∨ 𝜑)))
2524elrab3 2786 . . . . 5 (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑)))
2622, 25ax-mp 7 . . . 4 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑))
27 0ex 3987 . . . . . . 7 ∅ ∈ V
28 nsuceq0g 4269 . . . . . . 7 (∅ ∈ V → suc ∅ ≠ ∅)
2927, 28ax-mp 7 . . . . . 6 suc ∅ ≠ ∅
30 df-ne 2263 . . . . . 6 (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
3129, 30mpbi 144 . . . . 5 ¬ suc ∅ = ∅
32 pm2.53 679 . . . . 5 ((suc ∅ = ∅ ∨ 𝜑) → (¬ suc ∅ = ∅ → 𝜑))
3331, 32mpi 15 . . . 4 ((suc ∅ = ∅ ∨ 𝜑) → 𝜑)
3426, 33sylbi 120 . . 3 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → 𝜑)
3519eqeq1i 2102 . . . . 5 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ {∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
3619eqeq1i 2102 . . . . . . . 8 (suc ∅ = ∅ ↔ {∅} = ∅)
3731, 36mtbi 633 . . . . . . 7 ¬ {∅} = ∅
3820elsn 3482 . . . . . . 7 ({∅} ∈ {∅} ↔ {∅} = ∅)
3937, 38mtbir 634 . . . . . 6 ¬ {∅} ∈ {∅}
40 eleq2 2158 . . . . . 6 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ({∅} ∈ {∅} ↔ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
4139, 40mtbii 637 . . . . 5 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4235, 41sylbi 120 . . . 4 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
43 olc 670 . . . . 5 (𝜑 → ({∅} = ∅ ∨ 𝜑))
44 eqeq1 2101 . . . . . . . 8 (𝑧 = {∅} → (𝑧 = ∅ ↔ {∅} = ∅))
4544orbi1d 743 . . . . . . 7 (𝑧 = {∅} → ((𝑧 = ∅ ∨ 𝜑) ↔ ({∅} = ∅ ∨ 𝜑)))
4645elrab3 2786 . . . . . 6 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑)))
4721, 46ax-mp 7 . . . . 5 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑))
4843, 47sylibr 133 . . . 4 (𝜑 → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4942, 48nsyl 596 . . 3 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ 𝜑)
5034, 49orim12i 714 . 2 ((suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}) → (𝜑 ∨ ¬ 𝜑))
5118, 50ax-mp 7 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 103  wb 104  wo 667   = wceq 1296  wcel 1445  wne 2262  wral 2370  {crab 2374  Vcvv 2633  c0 3302  {csn 3466  {cpr 3467  Oncon0 4214  suc csuc 4216
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-nul 3986  ax-pow 4030
This theorem depends on definitions:  df-bi 116  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ne 2263  df-ral 2375  df-rex 2376  df-rab 2379  df-v 2635  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-uni 3676  df-tr 3959  df-iord 4217  df-on 4219  df-suc 4222
This theorem is referenced by:  ordsucunielexmid  4375
  Copyright terms: Public domain W3C validator