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

Theorem onsucelsucexmid 4514
Description: The converse of onsucelsucr 4492 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 4492 does hold, as seen at nnsucelsuc 6470. (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 4512 . . . 4 ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
2 0elon 4377 . . . . . 6 ∅ ∈ On
3 onsucelsucexmidlem 4513 . . . . . 6 {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On
42, 3pm3.2i 270 . . . . 5 (∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On)
5 onsucelsucexmid.1 . . . . 5 𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)
6 eleq1 2233 . . . . . . 7 (𝑥 = ∅ → (𝑥𝑦 ↔ ∅ ∈ 𝑦))
7 suceq 4387 . . . . . . . 8 (𝑥 = ∅ → suc 𝑥 = suc ∅)
87eleq1d 2239 . . . . . . 7 (𝑥 = ∅ → (suc 𝑥 ∈ suc 𝑦 ↔ suc ∅ ∈ suc 𝑦))
96, 8imbi12d 233 . . . . . 6 (𝑥 = ∅ → ((𝑥𝑦 → suc 𝑥 ∈ suc 𝑦) ↔ (∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦)))
10 eleq2 2234 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (∅ ∈ 𝑦 ↔ ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
11 suceq 4387 . . . . . . . 8 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc 𝑦 = suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
1211eleq2d 2240 . . . . . . 7 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ suc 𝑦 ↔ suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1310, 12imbi12d 233 . . . . . 6 (𝑦 = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ((∅ ∈ 𝑦 → suc ∅ ∈ suc 𝑦) ↔ (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})))
149, 13rspc2va 2848 . . . . 5 (((∅ ∈ On ∧ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∈ On) ∧ ∀𝑥 ∈ On ∀𝑦 ∈ On (𝑥𝑦 → suc 𝑥 ∈ suc 𝑦)) → (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
154, 5, 14mp2an 424 . . . 4 (∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
161, 15ax-mp 5 . . 3 suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}
17 elsuci 4388 . . 3 (suc ∅ ∈ suc {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
1816, 17ax-mp 5 . 2 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ∨ suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
19 suc0 4396 . . . . . 6 suc ∅ = {∅}
20 p0ex 4174 . . . . . . 7 {∅} ∈ V
2120prid2 3690 . . . . . 6 {∅} ∈ {∅, {∅}}
2219, 21eqeltri 2243 . . . . 5 suc ∅ ∈ {∅, {∅}}
23 eqeq1 2177 . . . . . . 7 (𝑧 = suc ∅ → (𝑧 = ∅ ↔ suc ∅ = ∅))
2423orbi1d 786 . . . . . 6 (𝑧 = suc ∅ → ((𝑧 = ∅ ∨ 𝜑) ↔ (suc ∅ = ∅ ∨ 𝜑)))
2524elrab3 2887 . . . . 5 (suc ∅ ∈ {∅, {∅}} → (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑)))
2622, 25ax-mp 5 . . . 4 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ (suc ∅ = ∅ ∨ 𝜑))
27 0ex 4116 . . . . . . 7 ∅ ∈ V
28 nsuceq0g 4403 . . . . . . 7 (∅ ∈ V → suc ∅ ≠ ∅)
2927, 28ax-mp 5 . . . . . 6 suc ∅ ≠ ∅
30 df-ne 2341 . . . . . 6 (suc ∅ ≠ ∅ ↔ ¬ suc ∅ = ∅)
3129, 30mpbi 144 . . . . 5 ¬ suc ∅ = ∅
32 pm2.53 717 . . . . 5 ((suc ∅ = ∅ ∨ 𝜑) → (¬ suc ∅ = ∅ → 𝜑))
3331, 32mpi 15 . . . 4 ((suc ∅ = ∅ ∨ 𝜑) → 𝜑)
3426, 33sylbi 120 . . 3 (suc ∅ ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → 𝜑)
3519eqeq1i 2178 . . . . 5 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ {∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
3619eqeq1i 2178 . . . . . . . 8 (suc ∅ = ∅ ↔ {∅} = ∅)
3731, 36mtbi 665 . . . . . . 7 ¬ {∅} = ∅
3820elsn 3599 . . . . . . 7 ({∅} ∈ {∅} ↔ {∅} = ∅)
3937, 38mtbir 666 . . . . . 6 ¬ {∅} ∈ {∅}
40 eleq2 2234 . . . . . 6 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ({∅} ∈ {∅} ↔ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)}))
4139, 40mtbii 669 . . . . 5 ({∅} = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4235, 41sylbi 120 . . . 4 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
43 olc 706 . . . . 5 (𝜑 → ({∅} = ∅ ∨ 𝜑))
44 eqeq1 2177 . . . . . . . 8 (𝑧 = {∅} → (𝑧 = ∅ ↔ {∅} = ∅))
4544orbi1d 786 . . . . . . 7 (𝑧 = {∅} → ((𝑧 = ∅ ∨ 𝜑) ↔ ({∅} = ∅ ∨ 𝜑)))
4645elrab3 2887 . . . . . 6 ({∅} ∈ {∅, {∅}} → ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑)))
4721, 46ax-mp 5 . . . . 5 ({∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} ↔ ({∅} = ∅ ∨ 𝜑))
4843, 47sylibr 133 . . . 4 (𝜑 → {∅} ∈ {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)})
4942, 48nsyl 623 . . 3 (suc ∅ = {𝑧 ∈ {∅, {∅}} ∣ (𝑧 = ∅ ∨ 𝜑)} → ¬ 𝜑)
5034, 49orim12i 754 . 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 703   = wceq 1348  wcel 2141  wne 2340  wral 2448  {crab 2452  Vcvv 2730  c0 3414  {csn 3583  {cpr 3584  Oncon0 4348  suc csuc 4350
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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160
This theorem depends on definitions:  df-bi 116  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-rab 2457  df-v 2732  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-uni 3797  df-tr 4088  df-iord 4351  df-on 4353  df-suc 4356
This theorem is referenced by:  ordsucunielexmid  4515
  Copyright terms: Public domain W3C validator