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

Theorem acexmid 5689
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).

(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 1473 . . . . . . . . . . . . . 14 𝑣(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒))
21sb8eu 1968 . . . . . . . . . . . . 13 (∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣[𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)))
3 eleq12 2159 . . . . . . . . . . . . . . . . . . . 20 ((𝑓 = 𝑣𝑐 = 𝑧) → (𝑓𝑐𝑣𝑧))
43ancoms 265 . . . . . . . . . . . . . . . . . . 19 ((𝑐 = 𝑧𝑓 = 𝑣) → (𝑓𝑐𝑣𝑧))
543adant3 966 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → (𝑓𝑐𝑣𝑧))
6 eleq12 2159 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = 𝑧𝑒 = 𝑢) → (𝑐𝑒𝑧𝑢))
763ad2antl1 1108 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑐𝑒𝑧𝑢))
8 eleq12 2159 . . . . . . . . . . . . . . . . . . . . 21 ((𝑓 = 𝑣𝑒 = 𝑢) → (𝑓𝑒𝑣𝑢))
983ad2antl2 1109 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑓𝑒𝑣𝑢))
107, 9anbi12d 458 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → ((𝑐𝑒𝑓𝑒) ↔ (𝑧𝑢𝑣𝑢)))
11 simpl3 951 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → 𝑏 = 𝑦)
1210, 11cbvrexdva2 2609 . . . . . . . . . . . . . . . . . 18 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → (∃𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢)))
135, 12anbi12d 458 . . . . . . . . . . . . . . . . 17 ((𝑐 = 𝑧𝑓 = 𝑣𝑏 = 𝑦) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
14133com23 1152 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝑧𝑏 = 𝑦𝑓 = 𝑣) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
15143expa 1146 . . . . . . . . . . . . . . 15 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑓 = 𝑣) → ((𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
1615sbiedv 1726 . . . . . . . . . . . . . 14 ((𝑐 = 𝑧𝑏 = 𝑦) → ([𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ (𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
1716eubidv 1963 . . . . . . . . . . . . 13 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑣[𝑣 / 𝑓](𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
182, 17syl5bb 191 . . . . . . . . . . . 12 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢))))
19 df-reu 2377 . . . . . . . . . . . 12 (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑓(𝑓𝑐 ∧ ∃𝑒𝑏 (𝑐𝑒𝑓𝑒)))
20 df-reu 2377 . . . . . . . . . . . 12 (∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢) ↔ ∃!𝑣(𝑣𝑧 ∧ ∃𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2118, 19, 203bitr4g 222 . . . . . . . . . . 11 ((𝑐 = 𝑧𝑏 = 𝑦) → (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2221adantr 271 . . . . . . . . . 10 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → (∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
23 simpll 497 . . . . . . . . . 10 (((𝑐 = 𝑧𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → 𝑐 = 𝑧)
2422, 23cbvraldva2 2608 . . . . . . . . 9 ((𝑐 = 𝑧𝑏 = 𝑦) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2524ancoms 265 . . . . . . . 8 ((𝑏 = 𝑦𝑐 = 𝑧) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2625adantll 461 . . . . . . 7 (((𝑎 = 𝑥𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → (∀𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
27 simpll 497 . . . . . . 7 (((𝑎 = 𝑥𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → 𝑎 = 𝑥)
2826, 27cbvraldva2 2608 . . . . . 6 ((𝑎 = 𝑥𝑏 = 𝑦) → (∀𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
2928cbvexdva 1859 . . . . 5 (𝑎 = 𝑥 → (∃𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∃𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)))
3029cbvalv 1849 . . . 4 (∀𝑎𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒) ↔ ∀𝑥𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢))
31 acexmid.choice . . . 4 𝑦𝑧𝑥𝑤𝑧 ∃!𝑣𝑧𝑢𝑦 (𝑧𝑢𝑣𝑢)
3230, 31mpgbir 1394 . . 3 𝑎𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒)
3332spi 1481 . 2 𝑏𝑐𝑎𝑑𝑐 ∃!𝑓𝑐𝑒𝑏 (𝑐𝑒𝑓𝑒)
3433acexmidlemv 5688 1 (𝜑 ∨ ¬ 𝜑)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3  wa 103  wb 104  wo 667  w3a 927  wal 1294  wex 1433  [wsb 1699  ∃!weu 1955  wral 2370  wrex 2371  ∃!wreu 2372
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 582  ax-in2 583  ax-io 668  ax-5 1388  ax-7 1389  ax-gen 1390  ax-ie1 1434  ax-ie2 1435  ax-8 1447  ax-10 1448  ax-11 1449  ax-i12 1450  ax-bndl 1451  ax-4 1452  ax-14 1457  ax-17 1471  ax-i9 1475  ax-ial 1479  ax-i5r 1480  ax-ext 2077  ax-sep 3978  ax-nul 3986  ax-pow 4030  ax-pr 4060
This theorem depends on definitions:  df-bi 116  df-3or 928  df-3an 929  df-tru 1299  df-nf 1402  df-sb 1700  df-eu 1958  df-clab 2082  df-cleq 2088  df-clel 2091  df-nfc 2224  df-ral 2375  df-rex 2376  df-reu 2377  df-rab 2379  df-v 2635  df-sbc 2855  df-dif 3015  df-un 3017  df-in 3019  df-ss 3026  df-nul 3303  df-pw 3451  df-sn 3472  df-pr 3473  df-uni 3676  df-tr 3959  df-iord 4217  df-on 4219  df-suc 4222  df-iota 5014  df-riota 5646
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator