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

Theorem acexmid 5457
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 y provides a value when z is inhabited (as opposed to non-empty 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 yz x w z ∃!v z u y (z u v u)
Assertion
Ref Expression
acexmid (φ ¬ φ)
Distinct variable group:   x,y,z,w,v,u
Allowed substitution hints:   φ(x,y,z,w,v,u)

Proof of Theorem acexmid
Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1421 . . . . . . . . . . . . . 14 v(f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒))
21sb8eu 1913 . . . . . . . . . . . . 13 (∃!f(f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ ∃!v[v / f](f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)))
3 eleq12 2102 . . . . . . . . . . . . . . . . . . . 20 ((f = v 𝑐 = z) → (f 𝑐v z))
43ancoms 255 . . . . . . . . . . . . . . . . . . 19 ((𝑐 = z f = v) → (f 𝑐v z))
543adant3 924 . . . . . . . . . . . . . . . . . 18 ((𝑐 = z f = v 𝑏 = y) → (f 𝑐v z))
6 eleq12 2102 . . . . . . . . . . . . . . . . . . . . 21 ((𝑐 = z 𝑒 = u) → (𝑐 𝑒z u))
763ad2antl1 1066 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = z f = v 𝑏 = y) 𝑒 = u) → (𝑐 𝑒z u))
8 eleq12 2102 . . . . . . . . . . . . . . . . . . . . 21 ((f = v 𝑒 = u) → (f 𝑒v u))
983ad2antl2 1067 . . . . . . . . . . . . . . . . . . . 20 (((𝑐 = z f = v 𝑏 = y) 𝑒 = u) → (f 𝑒v u))
107, 9anbi12d 442 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = z f = v 𝑏 = y) 𝑒 = u) → ((𝑐 𝑒 f 𝑒) ↔ (z u v u)))
11 simpl3 909 . . . . . . . . . . . . . . . . . . 19 (((𝑐 = z f = v 𝑏 = y) 𝑒 = u) → 𝑏 = y)
1210, 11cbvrexdva2 2535 . . . . . . . . . . . . . . . . . 18 ((𝑐 = z f = v 𝑏 = y) → (𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ u y (z u v u)))
135, 12anbi12d 442 . . . . . . . . . . . . . . . . 17 ((𝑐 = z f = v 𝑏 = y) → ((f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ (v z u y (z u v u))))
14133com23 1110 . . . . . . . . . . . . . . . 16 ((𝑐 = z 𝑏 = y f = v) → ((f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ (v z u y (z u v u))))
15143expa 1104 . . . . . . . . . . . . . . 15 (((𝑐 = z 𝑏 = y) f = v) → ((f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ (v z u y (z u v u))))
1615sbiedv 1672 . . . . . . . . . . . . . 14 ((𝑐 = z 𝑏 = y) → ([v / f](f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ (v z u y (z u v u))))
1716eubidv 1908 . . . . . . . . . . . . 13 ((𝑐 = z 𝑏 = y) → (∃!v[v / f](f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ ∃!v(v z u y (z u v u))))
182, 17syl5bb 181 . . . . . . . . . . . 12 ((𝑐 = z 𝑏 = y) → (∃!f(f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)) ↔ ∃!v(v z u y (z u v u))))
19 df-reu 2310 . . . . . . . . . . . 12 (∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ ∃!f(f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)))
20 df-reu 2310 . . . . . . . . . . . 12 (∃!v z u y (z u v u) ↔ ∃!v(v z u y (z u v u)))
2118, 19, 203bitr4g 212 . . . . . . . . . . 11 ((𝑐 = z 𝑏 = y) → (∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ ∃!v z u y (z u v u)))
2221adantr 261 . . . . . . . . . 10 (((𝑐 = z 𝑏 = y) 𝑑 = w) → (∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ ∃!v z u y (z u v u)))
23 simpll 481 . . . . . . . . . 10 (((𝑐 = z 𝑏 = y) 𝑑 = w) → 𝑐 = z)
2422, 23cbvraldva2 2534 . . . . . . . . 9 ((𝑐 = z 𝑏 = y) → (𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ w z ∃!v z u y (z u v u)))
2524ancoms 255 . . . . . . . 8 ((𝑏 = y 𝑐 = z) → (𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ w z ∃!v z u y (z u v u)))
2625adantll 445 . . . . . . 7 (((𝑎 = x 𝑏 = y) 𝑐 = z) → (𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ w z ∃!v z u y (z u v u)))
27 simpll 481 . . . . . . 7 (((𝑎 = x 𝑏 = y) 𝑐 = z) → 𝑎 = x)
2826, 27cbvraldva2 2534 . . . . . 6 ((𝑎 = x 𝑏 = y) → (𝑐 𝑎 𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ z x w z ∃!v z u y (z u v u)))
2928cbvexdva 1804 . . . . 5 (𝑎 = x → (𝑏𝑐 𝑎 𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ yz x w z ∃!v z u y (z u v u)))
3029cbvalv 1794 . . . 4 (𝑎𝑏𝑐 𝑎 𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒) ↔ xyz x w z ∃!v z u y (z u v u))
31 acexmid.choice . . . 4 yz x w z ∃!v z u y (z u v u)
3230, 31mpgbir 1342 . . 3 𝑎𝑏𝑐 𝑎 𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)
3332spi 1429 . 2 𝑏𝑐 𝑎 𝑑 𝑐 ∃!f 𝑐 𝑒 𝑏 (𝑐 𝑒 f 𝑒)
3433acexmidlemv 5456 1 (φ ¬ φ)
Colors of variables: wff set class
Syntax hints:  ¬ wn 3   wa 97  wb 98   wo 629   w3a 885  wal 1241  wex 1381  [wsb 1645  ∃!weu 1900  wral 2303  wrex 2304  ∃!wreu 2305
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101  ax-in1 544  ax-in2 545  ax-io 630  ax-5 1336  ax-7 1337  ax-gen 1338  ax-ie1 1382  ax-ie2 1383  ax-8 1395  ax-10 1396  ax-11 1397  ax-i12 1398  ax-bndl 1399  ax-4 1400  ax-14 1405  ax-17 1419  ax-i9 1423  ax-ial 1427  ax-i5r 1428  ax-ext 2022  ax-sep 3869  ax-nul 3877  ax-pow 3921  ax-pr 3938
This theorem depends on definitions:  df-bi 110  df-3or 886  df-3an 887  df-tru 1246  df-nf 1350  df-sb 1646  df-eu 1903  df-clab 2027  df-cleq 2033  df-clel 2036  df-nfc 2167  df-ral 2308  df-rex 2309  df-reu 2310  df-rab 2312  df-v 2556  df-sbc 2762  df-dif 2917  df-un 2919  df-in 2921  df-ss 2928  df-nul 3222  df-pw 3356  df-sn 3376  df-pr 3377  df-uni 3575  df-tr 3849  df-iord 4072  df-on 4074  df-suc 4077  df-iota 4813  df-riota 5414
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator