Theorem acexmid 5852

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 7183 and df-exmid 4181 syntaxes, see exmidac 7186. (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 1521	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒))
2	1	sb8eu 2032	. . . . . . . . . . . . 13 ⊢ (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
3		eleq12 2235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = 𝑣 ∧ 𝑐 = 𝑧) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
4	3	ancoms 266	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
5	4	3adant3 1012	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
6		eleq12 2235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝑧 ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
7	6	3ad2antl1 1154	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
8		eleq12 2235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝑣 ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
9	8	3ad2antl2 1155	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
10	7, 9	anbi12d 470	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → ((𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
11		simpl3 997	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → 𝑏 = 𝑦)
12	10, 11	cbvrexdva2 2704	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	5, 12	anbi12d 470	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
14	13	3com23 1204	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦 ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
15	14	3expa 1198	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
16	15	sbiedv 1782	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → ([𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
17	16	eubidv 2027	. . . . . . . . . . . . 13 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
18	2, 17	syl5bb 191	. . . . . . . . . . . 12 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
19		df-reu 2455	. . . . . . . . . . . 12 ⊢ (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
20		df-reu 2455	. . . . . . . . . . . 12 ⊢ (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
21	18, 19, 20	3bitr4g 222	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
22	21	adantr 274	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
23		simpll 524	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → 𝑐 = 𝑧)
24	22, 23	cbvraldva2 2703	. . . . . . . . 9 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
25	24	ancoms 266	. . . . . . . 8 ⊢ ((𝑏 = 𝑦 ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
26	25	adantll 473	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
27		simpll 524	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → 𝑎 = 𝑥)
28	26, 27	cbvraldva2 2703	. . . . . 6 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
29	28	cbvexdva 1922	. . . . 5 ⊢ (𝑎 = 𝑥 → (∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
30	29	cbvalv 1910	. . . 4 ⊢ (∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
31		acexmid.choice	. . . 4 ⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)
32	30, 31	mpgbir 1446	. . 3 ⊢ ∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
33	32	spi 1529	. 2 ⊢ ∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
34	33	acexmidlemv 5851	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 103   ↔ wb 104   ∨ wo 703   ∧ w3a 973  ∀wal 1346  ∃wex 1485  [wsb 1755  ∃!weu 2019  ∀wral 2448  ∃wrex 2449  ∃!wreu 2450

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-nf 1454  df-sb 1756  df-eu 2022  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-pw 3568  df-sn 3589  df-pr 3590  df-uni 3797  df-tr 4088  df-iord 4351  df-on 4353  df-suc 4356  df-iota 5160  df-riota 5809

This theorem is referenced by: (None)