Theorem acexmid 5813

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).

For this theorem stated using the df-ac 7120 and df-exmid 4151 syntaxes, see exmidac 7123. (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.

Step	Hyp	Ref	Expression
1		nfv 1505	. . . . . . . . . . . . . 14 |- F/ v ( f e. c /\ E. e e. b ( c e. e /\ f e. e ) )
2	1	sb8eu 2016	. . . . . . . . . . . . 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 2219	. . . . . . . . . . . . . . . . . . . 20 |- ( ( f = v /\ c = z ) -> ( f e. c <-> v e. z ) )
4	3	ancoms 266	. . . . . . . . . . . . . . . . . . 19 |- ( ( c = z /\ f = v ) -> ( f e. c <-> v e. z ) )
5	4	3adant3 1002	. . . . . . . . . . . . . . . . . 18 |- ( ( c = z /\ f = v /\ b = y ) -> ( f e. c <-> v e. z ) )
6		eleq12 2219	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( c = z /\ e = u ) -> ( c e. e <-> z e. u ) )
7	6	3ad2antl1 1144	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( c = z /\ f = v /\ b = y ) /\ e = u ) -> ( c e. e <-> z e. u ) )
8		eleq12 2219	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( f = v /\ e = u ) -> ( f e. e <-> v e. u ) )
9	8	3ad2antl2 1145	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( c = z /\ f = v /\ b = y ) /\ e = u ) -> ( f e. e <-> v e. u ) )
10	7, 9	anbi12d 465	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( c = z /\ f = v /\ b = y ) /\ e = u ) -> ( ( c e. e /\ f e. e ) <-> ( z e. u /\ v e. u ) ) )
11		simpl3 987	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( c = z /\ f = v /\ b = y ) /\ e = u ) -> b = y )
12	10, 11	cbvrexdva2 2685	. . . . . . . . . . . . . . . . . 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 ) ) )
13	5, 12	anbi12d 465	. . . . . . . . . . . . . . . . 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 ) ) ) )
14	13	3com23 1188	. . . . . . . . . . . . . . . 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 ) ) ) )
15	14	3expa 1182	. . . . . . . . . . . . . . 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 ) ) ) )
16	15	sbiedv 1766	. . . . . . . . . . . . . 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 ) ) ) )
17	16	eubidv 2011	. . . . . . . . . . . . 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 ) ) ) )
18	2, 17	syl5bb 191	. . . . . . . . . . . 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 2439	. . . . . . . . . . . 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 2439	. . . . . . . . . . . 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 ) ) )
21	18, 19, 20	3bitr4g 222	. . . . . . . . . . 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 ) ) )
22	21	adantr 274	. . . . . . . . . 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 519	. . . . . . . . . 10 |- ( ( ( c = z /\ b = y ) /\ d = w ) -> c = z )
24	22, 23	cbvraldva2 2684	. . . . . . . . 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 ) ) )
25	24	ancoms 266	. . . . . . . 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 ) ) )
26	25	adantll 468	. . . . . . 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 519	. . . . . . 7 |- ( ( ( a = x /\ b = y ) /\ c = z ) -> a = x )
28	26, 27	cbvraldva2 2684	. . . . . 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 ) ) )
29	28	cbvexdva 1906	. . . . 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 ) ) )
30	29	cbvalv 1894	. . . 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 )
32	30, 31	mpgbir 1430	. . 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 )
33	32	spi 1513	. 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 )
34	33	acexmidlemv 5812	1 |- ( ph \/ -. ph )

Syntax hints:   -. wn 3   /\ wa 103   <-> wb 104   \/ wo 698   /\ w3a 963   A.wal 1330   E.wex 1469   [wsb 1739   E!weu 2003   A.wral 2432   E.wrex 2433   E!wreu 2434

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 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1481  ax-10 1482  ax-11 1483  ax-i12 1484  ax-bndl 1486  ax-4 1487  ax-17 1503  ax-i9 1507  ax-ial 1511  ax-i5r 1512  ax-14 2128  ax-ext 2136  ax-sep 4078  ax-nul 4086  ax-pow 4130  ax-pr 4164

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1335  df-nf 1438  df-sb 1740  df-eu 2006  df-clab 2141  df-cleq 2147  df-clel 2150  df-nfc 2285  df-ral 2437  df-rex 2438  df-reu 2439  df-rab 2441  df-v 2711  df-sbc 2934  df-dif 3100  df-un 3102  df-in 3104  df-ss 3111  df-nul 3391  df-pw 3541  df-sn 3562  df-pr 3563  df-uni 3769  df-tr 4059  df-iord 4321  df-on 4323  df-suc 4326  df-iota 5128  df-riota 5770

This theorem is referenced by: (None)