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

Theorem exmidexmid 4090
Description: EXMID implies that an arbitrary proposition is decidable. That is, EXMID captures the usual meaning of excluded middle when stated in terms of propositions.

To get other propositional statements which are equivalent to excluded middle, combine this with notnotrdc 813, peircedc 884, or condc 823.

(Contributed by Jim Kingdon, 18-Jun-2022.)

Assertion
Ref Expression
exmidexmid (EXMIDDECID 𝜑)

Proof of Theorem exmidexmid
Dummy variables 𝑥 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ssrab2 3152 . . 3 {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}
2 df-exmid 4089 . . . 4 (EXMID ↔ ∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥))
3 p0ex 4082 . . . . . 6 {∅} ∈ V
43rabex 4042 . . . . 5 {𝑧 ∈ {∅} ∣ 𝜑} ∈ V
5 sseq1 3090 . . . . . 6 (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (𝑥 ⊆ {∅} ↔ {𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅}))
6 eleq2 2181 . . . . . . 7 (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (∅ ∈ 𝑥 ↔ ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))
76dcbid 808 . . . . . 6 (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → (DECID ∅ ∈ 𝑥DECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))
85, 7imbi12d 233 . . . . 5 (𝑥 = {𝑧 ∈ {∅} ∣ 𝜑} → ((𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥) ↔ ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} → DECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})))
94, 8spcv 2753 . . . 4 (∀𝑥(𝑥 ⊆ {∅} → DECID ∅ ∈ 𝑥) → ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} → DECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))
102, 9sylbi 120 . . 3 (EXMID → ({𝑧 ∈ {∅} ∣ 𝜑} ⊆ {∅} → DECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑}))
111, 10mpi 15 . 2 (EXMIDDECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑})
12 0ex 4025 . . . . 5 ∅ ∈ V
1312snid 3526 . . . 4 ∅ ∈ {∅}
14 biidd 171 . . . . 5 (𝑧 = ∅ → (𝜑𝜑))
1514elrab 2813 . . . 4 (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ (∅ ∈ {∅} ∧ 𝜑))
1613, 15mpbiran 909 . . 3 (∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ 𝜑)
1716dcbii 810 . 2 (DECID ∅ ∈ {𝑧 ∈ {∅} ∣ 𝜑} ↔ DECID 𝜑)
1811, 17sylib 121 1 (EXMIDDECID 𝜑)
Colors of variables: wff set class
Syntax hints:  wi 4  DECID wdc 804  wal 1314   = wceq 1316  wcel 1465  {crab 2397  wss 3041  c0 3333  {csn 3497  EXMIDwem 4088
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 588  ax-in2 589  ax-io 683  ax-5 1408  ax-7 1409  ax-gen 1410  ax-ie1 1454  ax-ie2 1455  ax-8 1467  ax-10 1468  ax-11 1469  ax-i12 1470  ax-bndl 1471  ax-4 1472  ax-14 1477  ax-17 1491  ax-i9 1495  ax-ial 1499  ax-i5r 1500  ax-ext 2099  ax-sep 4016  ax-nul 4024  ax-pow 4068
This theorem depends on definitions:  df-bi 116  df-dc 805  df-tru 1319  df-nf 1422  df-sb 1721  df-clab 2104  df-cleq 2110  df-clel 2113  df-nfc 2247  df-rab 2402  df-v 2662  df-dif 3043  df-in 3047  df-ss 3054  df-nul 3334  df-pw 3482  df-sn 3503  df-exmid 4089
This theorem is referenced by:  exmidn0m  4094  exmid0el  4097  exmidel  4098  exmidundif  4099  exmidundifim  4100  sbthlemi3  6815  sbthlemi5  6817  sbthlemi6  6818  exmidomniim  6981  exmidfodomrlemim  7025
  Copyright terms: Public domain W3C validator