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

Theorem acexmid 5887
Description: The axiom of choice implies excluded middle. Theorem 1.3 in [Bauer] p. 483.

The statement of the axiom of choice given here is ac2 in the Metamath Proof Explorer (version of 3-Aug-2019). In particular, note that the choice function 𝑦 provides a value when 𝑧 is inhabited (as opposed to nonempty as in some statements of the axiom of choice).

Essentially the same proof can also be found at "The axiom of choice implies instances of EM", [Crosilla], p. "Set-theoretic principles incompatible with intuitionistic logic".

Often referred to as Diaconescu's theorem, or Diaconescu-Goodman-Myhill theorem, after Radu Diaconescu who discovered it in 1975 in the framework of topos theory and N. D. Goodman and John Myhill in 1978 in the framework of set theory (although it already appeared as an exercise in Errett Bishop's book Foundations of Constructive Analysis from 1967).

For this theorem stated using the df-ac 7219 and df-exmid 4207 syntaxes, see exmidac 7222. (Contributed by Jim Kingdon, 4-Aug-2019.)

Hypothesis
Ref Expression
acexmid.choice 𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)
Assertion
Ref Expression
acexmid (𝜑 ∨ ¬ 𝜑)
Distinct variable group:   𝑥,𝑦,𝑧,𝑤,𝑣,𝑢
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤,𝑣,𝑢)

Proof of Theorem acexmid
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1538 . . . . . . . . . . . . . 14 𝑣(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒))
21sb8eu 2049 . . . . . . . . . . . . 13 (∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣[𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)))
3 eleq12 2252 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = 𝑣𝑐 = 𝑧) → (𝑓𝑐𝑣𝑧))
43ancoms 268 . . . . . . . . . . . . . . . . . . 19 ((𝑐 = 𝑧𝑓 = 𝑣) → (𝑓𝑐𝑣𝑧))
543adant3 1018 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → (𝑓𝑐𝑣𝑧))
6 eleq12 2252 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = 𝑧𝑒 = 𝑢) → (𝑐𝑒𝑧𝑢))
763ad2antl1 1160 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑐𝑒𝑧𝑢))
8 eleq12 2252 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = 𝑣𝑒 = 𝑢) → (𝑓𝑒𝑣𝑢))
983ad2antl2 1161 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑓𝑒𝑣𝑢))
107, 9anbi12d 473 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → ((𝑐𝑒𝑓𝑒) ↔ (𝑧𝑢𝑣𝑢)))
11 simpl3 1003 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → 𝑏 = 𝑦)
1210, 11cbvrexdva2 2723 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → (∃𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢)))
135, 12anbi12d 473 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
14133com23 1210 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝑧𝑏 = 𝑦𝑓 = 𝑣) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
15143expa 1204 . . . . . . . . . . . . . . 15 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑓 = 𝑣) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
1615sbiedv 1799 . . . . . . . . . . . . . 14 ((𝑐 = 𝑧𝑏 = 𝑦) → ([𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
1716eubidv 2044 . . . . . . . . . . . . 13 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑣[𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
182, 17bitrid 192 . . . . . . . . . . . 12 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
19 df-reu 2472 . . . . . . . . . . . 12 (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)))
20 df-reu 2472 . . . . . . . . . . . 12 (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2118, 19, 203bitr4g 223 . . . . . . . . . . 11 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2221adantr 276 . . . . . . . . . 10 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
23 simpll 527 . . . . . . . . . 10 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → 𝑐 = 𝑧)
2422, 23cbvraldva2 2722 . . . . . . . . 9 ((𝑐 = 𝑧𝑏 = 𝑦) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2524ancoms 268 . . . . . . . 8 ((𝑏 = 𝑦𝑐 = 𝑧) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2625adantll 476 . . . . . . 7 (((𝑎 = 𝑥𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
27 simpll 527 . . . . . . 7 (((𝑎 = 𝑥𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → 𝑎 = 𝑥)
2826, 27cbvraldva2 2722 . . . . . 6 ((𝑎 = 𝑥𝑏 = 𝑦) → (∀𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2928cbvexdva 1939 . . . . 5 (𝑎 = 𝑥 → (∃𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
3029cbvalv 1927 . . . 4 (∀𝑎𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑥𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢))
31 acexmid.choice . . . 4 𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)
3230, 31mpgbir 1463 . . 3 𝑎𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒)
3332spi 1546 . 2 𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒)
3433acexmidlemv 5886 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 104  wb 105  wo 709  w3a 979  wal 1361  wex 1502  [wsb 1772  ∃!weu 2036  wral 2465  wrex 2466  ∃!wreu 2467
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 615  ax-in2 616  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-14 2161  ax-ext 2169  ax-sep 4133  ax-nul 4141  ax-pow 4186  ax-pr 4221
This theorem depends on definitions:  df-bi 117  df-3or 980  df-3an 981  df-tru 1366  df-nf 1471  df-sb 1773  df-eu 2039  df-clab 2174  df-cleq 2180  df-clel 2183  df-nfc 2318  df-ral 2470  df-rex 2471  df-reu 2472  df-rab 2474  df-v 2751  df-sbc 2975  df-dif 3143  df-un 3145  df-in 3147  df-ss 3154  df-nul 3435  df-pw 3589  df-sn 3610  df-pr 3611  df-uni 3822  df-tr 4114  df-iord 4378  df-on 4380  df-suc 4383  df-iota 5190  df-riota 5844
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator