Theorem acexmid 6027

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 7464 and df-exmid 4291 syntaxes, see exmidac 7467. (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.

Step	Hyp	Ref	Expression
1		nfv 1577	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒))
2	1	sb8eu 2092	. . . . . . . . . . . . 13 ⊢ (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
3		eleq12 2296	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = 𝑣 ∧ 𝑐 = 𝑧) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
4	3	ancoms 268	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
5	4	3adant3 1044	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
6		eleq12 2296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝑧 ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
7	6	3ad2antl1 1186	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
8		eleq12 2296	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝑣 ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
9	8	3ad2antl2 1187	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
10	7, 9	anbi12d 473	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → ((𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
11		simpl3 1029	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → 𝑏 = 𝑦)
12	10, 11	cbvrexdva2 2776	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	5, 12	anbi12d 473	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
14	13	3com23 1236	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦 ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
15	14	3expa 1230	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
16	15	sbiedv 1837	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → ([𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
17	16	eubidv 2087	. . . . . . . . . . . . 13 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
18	2, 17	bitrid 192	. . . . . . . . . . . 12 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
19		df-reu 2518	. . . . . . . . . . . 12 ⊢ (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
20		df-reu 2518	. . . . . . . . . . . 12 ⊢ (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
21	18, 19, 20	3bitr4g 223	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
22	21	adantr 276	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
23		simpll 527	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → 𝑐 = 𝑧)
24	22, 23	cbvraldva2 2775	. . . . . . . . 9 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
25	24	ancoms 268	. . . . . . . 8 ⊢ ((𝑏 = 𝑦 ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
26	25	adantll 476	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
27		simpll 527	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → 𝑎 = 𝑥)
28	26, 27	cbvraldva2 2775	. . . . . 6 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
29	28	cbvexdva 1978	. . . . 5 ⊢ (𝑎 = 𝑥 → (∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
30	29	cbvalv 1966	. . . 4 ⊢ (∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
31		acexmid.choice	. . . 4 ⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)
32	30, 31	mpgbir 1502	. . 3 ⊢ ∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
33	32	spi 1585	. 2 ⊢ ∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
34	33	acexmidlemv 6026	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 104   ↔ wb 105   ∨ wo 716   ∧ w3a 1005  ∀wal 1396  ∃wex 1541  [wsb 1810  ∃!weu 2079  ∀wral 2511  ∃wrex 2512  ∃!wreu 2513

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 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-14 2205  ax-ext 2213  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305

This theorem depends on definitions:  df-bi 117  df-3or 1006  df-3an 1007  df-tru 1401  df-nf 1510  df-sb 1811  df-eu 2082  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-pw 3658  df-sn 3679  df-pr 3680  df-uni 3899  df-tr 4193  df-iord 4469  df-on 4471  df-suc 4474  df-iota 5293  df-riota 5981

This theorem is referenced by: (None)