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

Theorem onsucelsucexmid 4255
Description: The converse of onsucelsucr 4234 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 4234 does hold, as seen at nnsucelsuc 6070. (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 4253 . . . 4 ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
2 0elon 4129 . . . . . 6 ∅ ∈ On
3 onsucelsucexmidlem 4254 . . . . . 6 {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On
42, 3pm3.2i 257 . . . . 5 (∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On)
5 onsucelsucexmid.1 . . . . 5 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
6 eleq1 2100 . . . . . . 7 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
7 suceq 4139 . . . . . . . 8 (𝑥 = ∅ → suc 𝑥 = suc ∅)
87eleq1d 2106 . . . . . . 7 (𝑥 = ∅ → (suc 𝑥 ∈ suc 𝑦 ↔ suc ∅ ∈ suc 𝑦))
96, 8imbi12d 223 . . . . . 6 (𝑥 = ∅ → ((𝑥𝑦 → suc 𝑥 ∈ suc 𝑦) ↔ (∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦)))
10 eleq2 2101 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (∅ ∈ 𝑦 ↔ ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
11 suceq 4139 . . . . . . . 8 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc 𝑦 = suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
1211eleq2d 2107 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ suc 𝑦 ↔ suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1310, 12imbi12d 223 . . . . . 6 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ((∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦) ↔ (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})))
149, 13rspc2va 2663 . . . . 5 (((∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)) → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
154, 5, 14mp2an 402 . . . 4 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
161, 15ax-mp 7 . . 3 suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
17 elsuci 4140 . . 3 (suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1816, 17ax-mp 7 . 2 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
19 suc0 4148 . . . . . 6 suc ∅ = {∅}
20 p0ex 3939 . . . . . . 7 {∅} ∈ V
2120prid2 3477 . . . . . 6 {∅} ∈ {∅, {∅}}
2219, 21eqeltri 2110 . . . . 5 suc ∅ ∈ {∅, {∅}}
23 eqeq1 2046 . . . . . . 7 (𝑧 = suc ∅ → (𝑧 = ∅ ↔ suc ∅ = ∅))
2423orbi1d 705 . . . . . 6 (𝑧 = suc ∅ → ((𝑧 = ∅ ∨ 𝜑) ↔ (suc ∅ = ∅ ∨ 𝜑)))
2524elrab3 2699 . . . . 5 (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑)))
2622, 25ax-mp 7 . . . 4 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑))
27 0ex 3884 . . . . . . 7 ∅ ∈ V
28 nsuceq0g 4155 . . . . . . 7 (∅ ∈ V → suc ∅ ≠ ∅)
2927, 28ax-mp 7 . . . . . 6 suc ∅ ≠ ∅
30 df-ne 2206 . . . . . 6 (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
3129, 30mpbi 133 . . . . 5 ¬ suc ∅ = ∅
32 pm2.53 641 . . . . 5 ((suc ∅ = ∅ ∨ 𝜑) → (¬ suc ∅ = ∅ → 𝜑))
3331, 32mpi 15 . . . 4 ((suc ∅ = ∅ ∨ 𝜑) → 𝜑)
3426, 33sylbi 114 . . 3 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → 𝜑)
3519eqeq1i 2047 . . . . 5 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ {∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
3619eqeq1i 2047 . . . . . . . 8 (suc ∅ = ∅ ↔ {∅} = ∅)
3731, 36mtbi 595 . . . . . . 7 ¬ {∅} = ∅
3820elsn 3391 . . . . . . 7 ({∅} ∈ {∅} ↔ {∅} = ∅)
3937, 38mtbir 596 . . . . . 6 ¬ {∅} ∈ {∅}
40 eleq2 2101 . . . . . 6 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ({∅} ∈ {∅} ↔ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
4139, 40mtbii 599 . . . . 5 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4235, 41sylbi 114 . . . 4 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
43 olc 632 . . . . 5 (𝜑 → ({∅} = ∅ ∨ 𝜑))
44 eqeq1 2046 . . . . . . . 8 (𝑧 = {∅} → (𝑧 = ∅ ↔ {∅} = ∅))
4544orbi1d 705 . . . . . . 7 (𝑧 = {∅} → ((𝑧 = ∅ ∨ 𝜑) ↔ ({∅} = ∅ ∨ 𝜑)))
4645elrab3 2699 . . . . . 6 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑)))
4721, 46ax-mp 7 . . . . 5 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑))
4843, 47sylibr 137 . . . 4 (𝜑 → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4942, 48nsyl 558 . . 3 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ 𝜑)
5034, 49orim12i 676 . 2 ((suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}) → (𝜑 ∨ ¬ 𝜑))
5118, 50ax-mp 7 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 97  wb 98  wo 629   = wceq 1243  wcel 1393  wne 2204  wral 2306  {crab 2310  Vcvv 2557  c0 3224  {csn 3375  {cpr 3376  Oncon0 4100  suc csuc 4102
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-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3875  ax-nul 3883  ax-pow 3927
This theorem depends on definitions:  df-bi 110  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ne 2206  df-ral 2311  df-rex 2312  df-rab 2315  df-v 2559  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-uni 3581  df-tr 3855  df-iord 4103  df-on 4105  df-suc 4108
This theorem is referenced by:  ordsucunielexmid  4256
  Copyright terms: Public domain W3C validator