Theorem acexmid 5511

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 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	⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)

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 1421	. . . . . . . . . . . . . 14 ⊢ Ⅎ𝑣(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒))
2	1	sb8eu 1913	. . . . . . . . . . . . 13 ⊢ (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
3		eleq12 2102	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 = 𝑣 ∧ 𝑐 = 𝑧) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
4	3	ancoms 255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
5	4	3adant3 924	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (𝑓 ∈ 𝑐 ↔ 𝑣 ∈ 𝑧))
6		eleq12 2102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = 𝑧 ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
7	6	3ad2antl1 1066	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑐 ∈ 𝑒 ↔ 𝑧 ∈ 𝑢))
8		eleq12 2102	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 = 𝑣 ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
9	8	3ad2antl2 1067	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → (𝑓 ∈ 𝑒 ↔ 𝑣 ∈ 𝑢))
10	7, 9	anbi12d 442	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → ((𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
11		simpl3 909	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) ∧ 𝑒 = 𝑢) → 𝑏 = 𝑦)
12	10, 11	cbvrexdva2 2538	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → (∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
13	5, 12	anbi12d 442	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = 𝑧 ∧ 𝑓 = 𝑣 ∧ 𝑏 = 𝑦) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
14	13	3com23 1110	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦 ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
15	14	3expa 1104	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑓 = 𝑣) → ((𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
16	15	sbiedv 1672	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → ([𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ (𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
17	16	eubidv 1908	. . . . . . . . . . . . 13 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑣[𝑣 / 𝑓](𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
18	2, 17	syl5bb 181	. . . . . . . . . . . 12 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))))
19		df-reu 2313	. . . . . . . . . . . 12 ⊢ (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑓(𝑓 ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)))
20		df-reu 2313	. . . . . . . . . . . 12 ⊢ (∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢) ↔ ∃!𝑣(𝑣 ∈ 𝑧 ∧ ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
21	18, 19, 20	3bitr4g 212	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
22	21	adantr 261	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → (∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
23		simpll 481	. . . . . . . . . 10 ⊢ (((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) ∧ 𝑑 = 𝑤) → 𝑐 = 𝑧)
24	22, 23	cbvraldva2 2537	. . . . . . . . 9 ⊢ ((𝑐 = 𝑧 ∧ 𝑏 = 𝑦) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
25	24	ancoms 255	. . . . . . . 8 ⊢ ((𝑏 = 𝑦 ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
26	25	adantll 445	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → (∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
27		simpll 481	. . . . . . 7 ⊢ (((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) ∧ 𝑐 = 𝑧) → 𝑎 = 𝑥)
28	26, 27	cbvraldva2 2537	. . . . . 6 ⊢ ((𝑎 = 𝑥 ∧ 𝑏 = 𝑦) → (∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
29	28	cbvexdva 1804	. . . . 5 ⊢ (𝑎 = 𝑥 → (∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)))
30	29	cbvalv 1794	. . . 4 ⊢ (∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒) ↔ ∀𝑥∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢))
31		acexmid.choice	. . . 4 ⊢ ∃𝑦∀𝑧 ∈ 𝑥 ∀𝑤 ∈ 𝑧 ∃!𝑣 ∈ 𝑧 ∃𝑢 ∈ 𝑦 (𝑧 ∈ 𝑢 ∧ 𝑣 ∈ 𝑢)
32	30, 31	mpgbir 1342	. . 3 ⊢ ∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
33	32	spi 1429	. 2 ⊢ ∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!𝑓 ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ 𝑓 ∈ 𝑒)
34	33	acexmidlemv 5510	1 ⊢ (𝜑 ∨ ¬ 𝜑)

Syntax hints:  ¬ wn 3   ∧ wa 97   ↔ wb 98   ∨ wo 629   ∧ w3a 885  ∀wal 1241  ∃wex 1381  [wsb 1645  ∃!weu 1900  ∀wral 2306  ∃wrex 2307  ∃!wreu 2308

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 3875  ax-nul 3883  ax-pow 3927  ax-pr 3944

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 2311  df-rex 2312  df-reu 2313  df-rab 2315  df-v 2559  df-sbc 2765  df-dif 2920  df-un 2922  df-in 2924  df-ss 2931  df-nul 3225  df-pw 3361  df-sn 3381  df-pr 3382  df-uni 3581  df-tr 3855  df-iord 4103  df-on 4105  df-suc 4108  df-iota 4867  df-riota 5468

This theorem is referenced by: (None)