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

Theorem acexmid 5633
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 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  |-  E. y A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)
Assertion
Ref Expression
acexmid  |-  ( ph  \/  -.  ph )
Distinct variable group:    x, y, z, w, v, u
Allowed substitution hints:    ph( x, y, z, w, v, u)

Proof of Theorem acexmid
Dummy variables  a  b  c  d  e  f are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 nfv 1466 . . . . . . . . . . . . . 14  |-  F/ v ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )
21sb8eu 1961 . . . . . . . . . . . . 13  |-  ( E! f ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )  <->  E! v [ v  /  f ] ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) ) )
3 eleq12 2152 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( f  =  v  /\  c  =  z )  ->  ( f  e.  c  <-> 
v  e.  z ) )
43ancoms 264 . . . . . . . . . . . . . . . . . . 19  |-  ( ( c  =  z  /\  f  =  v )  ->  ( f  e.  c  <-> 
v  e.  z ) )
543adant3 963 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  z  /\  f  =  v  /\  b  =  y )  ->  ( f  e.  c  <-> 
v  e.  z ) )
6 eleq12 2152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( c  =  z  /\  e  =  u )  ->  ( c  e.  e  <-> 
z  e.  u ) )
763ad2antl1 1105 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( c  =  z  /\  f  =  v  /\  b  =  y )  /\  e  =  u )  ->  (
c  e.  e  <->  z  e.  u ) )
8 eleq12 2152 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( f  =  v  /\  e  =  u )  ->  ( f  e.  e  <-> 
v  e.  u ) )
983ad2antl2 1106 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( c  =  z  /\  f  =  v  /\  b  =  y )  /\  e  =  u )  ->  (
f  e.  e  <->  v  e.  u ) )
107, 9anbi12d 457 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( c  =  z  /\  f  =  v  /\  b  =  y )  /\  e  =  u )  ->  (
( c  e.  e  /\  f  e.  e )  <->  ( z  e.  u  /\  v  e.  u ) ) )
11 simpl3 948 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( c  =  z  /\  f  =  v  /\  b  =  y )  /\  e  =  u )  ->  b  =  y )
1210, 11cbvrexdva2 2595 . . . . . . . . . . . . . . . . . 18  |-  ( ( c  =  z  /\  f  =  v  /\  b  =  y )  ->  ( E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
135, 12anbi12d 457 . . . . . . . . . . . . . . . . 17  |-  ( ( c  =  z  /\  f  =  v  /\  b  =  y )  ->  ( ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )  <->  ( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) ) )
14133com23 1149 . . . . . . . . . . . . . . . 16  |-  ( ( c  =  z  /\  b  =  y  /\  f  =  v )  ->  ( ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )  <->  ( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) ) )
15143expa 1143 . . . . . . . . . . . . . . 15  |-  ( ( ( c  =  z  /\  b  =  y )  /\  f  =  v )  ->  (
( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )  <->  ( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) ) )
1615sbiedv 1719 . . . . . . . . . . . . . 14  |-  ( ( c  =  z  /\  b  =  y )  ->  ( [ v  / 
f ] ( f  e.  c  /\  E. e  e.  b  (
c  e.  e  /\  f  e.  e )
)  <->  ( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) ) )
1716eubidv 1956 . . . . . . . . . . . . 13  |-  ( ( c  =  z  /\  b  =  y )  ->  ( E! v [ v  /  f ] ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) )  <->  E! v
( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) ) )
182, 17syl5bb 190 . . . . . . . . . . . 12  |-  ( ( c  =  z  /\  b  =  y )  ->  ( E! f ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e )
)  <->  E! v ( v  e.  z  /\  E. u  e.  y  (
z  e.  u  /\  v  e.  u )
) ) )
19 df-reu 2366 . . . . . . . . . . . 12  |-  ( E! f  e.  c  E. e  e.  b  (
c  e.  e  /\  f  e.  e )  <->  E! f ( f  e.  c  /\  E. e  e.  b  ( c  e.  e  /\  f  e.  e ) ) )
20 df-reu 2366 . . . . . . . . . . . 12  |-  ( E! v  e.  z  E. u  e.  y  (
z  e.  u  /\  v  e.  u )  <->  E! v ( v  e.  z  /\  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
2118, 19, 203bitr4g 221 . . . . . . . . . . 11  |-  ( ( c  =  z  /\  b  =  y )  ->  ( E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
2221adantr 270 . . . . . . . . . 10  |-  ( ( ( c  =  z  /\  b  =  y )  /\  d  =  w )  ->  ( E! f  e.  c  E. e  e.  b 
( c  e.  e  /\  f  e.  e )  <->  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u
) ) )
23 simpll 496 . . . . . . . . . 10  |-  ( ( ( c  =  z  /\  b  =  y )  /\  d  =  w )  ->  c  =  z )
2422, 23cbvraldva2 2594 . . . . . . . . 9  |-  ( ( c  =  z  /\  b  =  y )  ->  ( A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  A. w  e.  z  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
2524ancoms 264 . . . . . . . 8  |-  ( ( b  =  y  /\  c  =  z )  ->  ( A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  A. w  e.  z  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
2625adantll 460 . . . . . . 7  |-  ( ( ( a  =  x  /\  b  =  y )  /\  c  =  z )  ->  ( A. d  e.  c  E! f  e.  c  E. e  e.  b 
( c  e.  e  /\  f  e.  e )  <->  A. w  e.  z  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u
) ) )
27 simpll 496 . . . . . . 7  |-  ( ( ( a  =  x  /\  b  =  y )  /\  c  =  z )  ->  a  =  x )
2826, 27cbvraldva2 2594 . . . . . 6  |-  ( ( a  =  x  /\  b  =  y )  ->  ( A. c  e.  a  A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) ) )
2928cbvexdva 1852 . . . . 5  |-  ( a  =  x  ->  ( E. b A. c  e.  a  A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  E. y A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
) ) )
3029cbvalv 1842 . . . 4  |-  ( A. a E. b A. c  e.  a  A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )  <->  A. x E. y A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y  ( z  e.  u  /\  v  e.  u ) )
31 acexmid.choice . . . 4  |-  E. y A. z  e.  x  A. w  e.  z  E! v  e.  z  E. u  e.  y 
( z  e.  u  /\  v  e.  u
)
3230, 31mpgbir 1387 . . 3  |-  A. a E. b A. c  e.  a  A. d  e.  c  E! f  e.  c  E. e  e.  b  ( c  e.  e  /\  f  e.  e )
3332spi 1474 . 2  |-  E. b A. c  e.  a  A. d  e.  c  E! f  e.  c  E. e  e.  b 
( c  e.  e  /\  f  e.  e )
3433acexmidlemv 5632 1  |-  ( ph  \/  -.  ph )
Colors of variables: wff set class
Syntax hints:   -. wn 3    /\ wa 102    <-> wb 103    \/ wo 664    /\ w3a 924   A.wal 1287   E.wex 1426   [wsb 1692   E!weu 1948   A.wral 2359   E.wrex 2360   E!wreu 2361
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-in1 579  ax-in2 580  ax-io 665  ax-5 1381  ax-7 1382  ax-gen 1383  ax-ie1 1427  ax-ie2 1428  ax-8 1440  ax-10 1441  ax-11 1442  ax-i12 1443  ax-bndl 1444  ax-4 1445  ax-14 1450  ax-17 1464  ax-i9 1468  ax-ial 1472  ax-i5r 1473  ax-ext 2070  ax-sep 3949  ax-nul 3957  ax-pow 4001  ax-pr 4027
This theorem depends on definitions:  df-bi 115  df-3or 925  df-3an 926  df-tru 1292  df-nf 1395  df-sb 1693  df-eu 1951  df-clab 2075  df-cleq 2081  df-clel 2084  df-nfc 2217  df-ral 2364  df-rex 2365  df-reu 2366  df-rab 2368  df-v 2621  df-sbc 2839  df-dif 2999  df-un 3001  df-in 3003  df-ss 3010  df-nul 3285  df-pw 3427  df-sn 3447  df-pr 3448  df-uni 3649  df-tr 3929  df-iord 4184  df-on 4186  df-suc 4189  df-iota 4967  df-riota 5590
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator