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

Theorem onsucelsucexmid 4312
Description: The converse of onsucelsucr 4291 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 4291 does hold, as seen at nnsucelsuc 6187. (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 4310 . . . 4 ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
2 0elon 4186 . . . . . 6 ∅ ∈ On
3 onsucelsucexmidlem 4311 . . . . . 6 {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On
42, 3pm3.2i 266 . . . . 5 (∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On)
5 onsucelsucexmid.1 . . . . 5 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
6 eleq1 2147 . . . . . . 7 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
7 suceq 4196 . . . . . . . 8 (𝑥 = ∅ → suc 𝑥 = suc ∅)
87eleq1d 2153 . . . . . . 7 (𝑥 = ∅ → (suc 𝑥 ∈ suc 𝑦 ↔ suc ∅ ∈ suc 𝑦))
96, 8imbi12d 232 . . . . . 6 (𝑥 = ∅ → ((𝑥𝑦 → suc 𝑥 ∈ suc 𝑦) ↔ (∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦)))
10 eleq2 2148 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (∅ ∈ 𝑦 ↔ ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
11 suceq 4196 . . . . . . . 8 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc 𝑦 = suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
1211eleq2d 2154 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ suc 𝑦 ↔ suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1310, 12imbi12d 232 . . . . . 6 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ((∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦) ↔ (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})))
149, 13rspc2va 2726 . . . . 5 (((∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)) → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
154, 5, 14mp2an 417 . . . 4 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
161, 15ax-mp 7 . . 3 suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
17 elsuci 4197 . . 3 (suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1816, 17ax-mp 7 . 2 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
19 suc0 4205 . . . . . 6 suc ∅ = {∅}
20 p0ex 3990 . . . . . . 7 {∅} ∈ V
2120prid2 3526 . . . . . 6 {∅} ∈ {∅, {∅}}
2219, 21eqeltri 2157 . . . . 5 suc ∅ ∈ {∅, {∅}}
23 eqeq1 2091 . . . . . . 7 (𝑧 = suc ∅ → (𝑧 = ∅ ↔ suc ∅ = ∅))
2423orbi1d 738 . . . . . 6 (𝑧 = suc ∅ → ((𝑧 = ∅ ∨ 𝜑) ↔ (suc ∅ = ∅ ∨ 𝜑)))
2524elrab3 2762 . . . . 5 (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑)))
2622, 25ax-mp 7 . . . 4 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑))
27 0ex 3934 . . . . . . 7 ∅ ∈ V
28 nsuceq0g 4212 . . . . . . 7 (∅ ∈ V → suc ∅ ≠ ∅)
2927, 28ax-mp 7 . . . . . 6 suc ∅ ≠ ∅
30 df-ne 2252 . . . . . 6 (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
3129, 30mpbi 143 . . . . 5 ¬ suc ∅ = ∅
32 pm2.53 674 . . . . 5 ((suc ∅ = ∅ ∨ 𝜑) → (¬ suc ∅ = ∅ → 𝜑))
3331, 32mpi 15 . . . 4 ((suc ∅ = ∅ ∨ 𝜑) → 𝜑)
3426, 33sylbi 119 . . 3 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → 𝜑)
3519eqeq1i 2092 . . . . 5 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ {∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
3619eqeq1i 2092 . . . . . . . 8 (suc ∅ = ∅ ↔ {∅} = ∅)
3731, 36mtbi 628 . . . . . . 7 ¬ {∅} = ∅
3820elsn 3441 . . . . . . 7 ({∅} ∈ {∅} ↔ {∅} = ∅)
3937, 38mtbir 629 . . . . . 6 ¬ {∅} ∈ {∅}
40 eleq2 2148 . . . . . 6 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ({∅} ∈ {∅} ↔ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
4139, 40mtbii 632 . . . . 5 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4235, 41sylbi 119 . . . 4 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
43 olc 665 . . . . 5 (𝜑 → ({∅} = ∅ ∨ 𝜑))
44 eqeq1 2091 . . . . . . . 8 (𝑧 = {∅} → (𝑧 = ∅ ↔ {∅} = ∅))
4544orbi1d 738 . . . . . . 7 (𝑧 = {∅} → ((𝑧 = ∅ ∨ 𝜑) ↔ ({∅} = ∅ ∨ 𝜑)))
4645elrab3 2762 . . . . . 6 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑)))
4721, 46ax-mp 7 . . . . 5 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑))
4843, 47sylibr 132 . . . 4 (𝜑 → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4942, 48nsyl 591 . . 3 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ 𝜑)
5034, 49orim12i 709 . 2 ((suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}) → (𝜑 ∨ ¬ 𝜑))
5118, 50ax-mp 7 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wi 4  wa 102  wb 103  wo 662   = wceq 1287  wcel 1436  wne 2251  wral 2355  {crab 2359  Vcvv 2614  c0 3272  {csn 3425  {cpr 3426  Oncon0 4157  suc csuc 4159
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 1379  ax-7 1380  ax-gen 1381  ax-ie1 1425  ax-ie2 1426  ax-8 1438  ax-10 1439  ax-11 1440  ax-i12 1441  ax-bndl 1442  ax-4 1443  ax-14 1448  ax-17 1462  ax-i9 1466  ax-ial 1470  ax-i5r 1471  ax-ext 2067  ax-sep 3925  ax-nul 3933  ax-pow 3977
This theorem depends on definitions:  df-bi 115  df-3an 924  df-tru 1290  df-nf 1393  df-sb 1690  df-clab 2072  df-cleq 2078  df-clel 2081  df-nfc 2214  df-ne 2252  df-ral 2360  df-rex 2361  df-rab 2364  df-v 2616  df-dif 2988  df-un 2990  df-in 2992  df-ss 2999  df-nul 3273  df-pw 3411  df-sn 3431  df-pr 3432  df-uni 3631  df-tr 3905  df-iord 4160  df-on 4162  df-suc 4165
This theorem is referenced by:  ordsucunielexmid  4313
  Copyright terms: Public domain W3C validator