Theorem acexmid 5404

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

(Contributed by Jim Kingdon, 4-Aug-2019.)

Hypothesis

Ref	Expression
acexmid.choice	⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)

Assertion

Ref	Expression
acexmid	⊢ (φ ∨ ¬ φ)

Distinct variable group:   x,y,z,w,v,u

Allowed substitution hints:   φ(x,y,z,w,v,u)

Proof of Theorem acexmid

Dummy variables 𝑎 𝑏 𝑐 𝑑 𝑒 f are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfv 1403	. . . . . . . . . . . . . 14 ⊢ Ⅎv(f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒))
2	1	sb8eu 1894	. . . . . . . . . . . . 13 ⊢ (∃!f(f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ ∃!v[v / f](f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)))
3		eleq12 2084	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((f = v ∧ 𝑐 = z) → (f ∈ 𝑐 ↔ v ∈ z))
4	3	ancoms 255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑐 = z ∧ f = v) → (f ∈ 𝑐 ↔ v ∈ z))
5	4	3adant3 914	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = z ∧ f = v ∧ 𝑏 = y) → (f ∈ 𝑐 ↔ v ∈ z))
6		eleq12 2084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑐 = z ∧ 𝑒 = u) → (𝑐 ∈ 𝑒 ↔ z ∈ u))
7	6	3ad2antl1 1056	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = z ∧ f = v ∧ 𝑏 = y) ∧ 𝑒 = u) → (𝑐 ∈ 𝑒 ↔ z ∈ u))
8		eleq12 2084	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((f = v ∧ 𝑒 = u) → (f ∈ 𝑒 ↔ v ∈ u))
9	8	3ad2antl2 1057	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((𝑐 = z ∧ f = v ∧ 𝑏 = y) ∧ 𝑒 = u) → (f ∈ 𝑒 ↔ v ∈ u))
10	7, 9	anbi12d 445	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = z ∧ f = v ∧ 𝑏 = y) ∧ 𝑒 = u) → ((𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ (z ∈ u ∧ v ∈ u)))
11		simpl3 899	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑐 = z ∧ f = v ∧ 𝑏 = y) ∧ 𝑒 = u) → 𝑏 = y)
12	10, 11	cbvrexdva2 2514	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑐 = z ∧ f = v ∧ 𝑏 = y) → (∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∃u ∈ y (z ∈ u ∧ v ∈ u)))
13	5, 12	anbi12d 445	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑐 = z ∧ f = v ∧ 𝑏 = y) → ((f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
14	13	3com23 1098	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = z ∧ 𝑏 = y ∧ f = v) → ((f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
15	14	3expa 1092	. . . . . . . . . . . . . . 15 ⊢ (((𝑐 = z ∧ 𝑏 = y) ∧ f = v) → ((f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
16	15	sbiedv 1654	. . . . . . . . . . . . . 14 ⊢ ((𝑐 = z ∧ 𝑏 = y) → ([v / f](f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ (v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
17	16	eubidv 1889	. . . . . . . . . . . . 13 ⊢ ((𝑐 = z ∧ 𝑏 = y) → (∃!v[v / f](f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
18	2, 17	syl5bb 181	. . . . . . . . . . . 12 ⊢ ((𝑐 = z ∧ 𝑏 = y) → (∃!f(f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u))))
19		df-reu 2289	. . . . . . . . . . . 12 ⊢ (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∃!f(f ∈ 𝑐 ∧ ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)))
20		df-reu 2289	. . . . . . . . . . . 12 ⊢ (∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u) ↔ ∃!v(v ∈ z ∧ ∃u ∈ y (z ∈ u ∧ v ∈ u)))
21	18, 19, 20	3bitr4g 212	. . . . . . . . . . 11 ⊢ ((𝑐 = z ∧ 𝑏 = y) → (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
22	21	adantr 261	. . . . . . . . . 10 ⊢ (((𝑐 = z ∧ 𝑏 = y) ∧ 𝑑 = w) → (∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
23		simpll 469	. . . . . . . . . 10 ⊢ (((𝑐 = z ∧ 𝑏 = y) ∧ 𝑑 = w) → 𝑐 = z)
24	22, 23	cbvraldva2 2513	. . . . . . . . 9 ⊢ ((𝑐 = z ∧ 𝑏 = y) → (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
25	24	ancoms 255	. . . . . . . 8 ⊢ ((𝑏 = y ∧ 𝑐 = z) → (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
26	25	adantll 448	. . . . . . 7 ⊢ (((𝑎 = x ∧ 𝑏 = y) ∧ 𝑐 = z) → (∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
27		simpll 469	. . . . . . 7 ⊢ (((𝑎 = x ∧ 𝑏 = y) ∧ 𝑐 = z) → 𝑎 = x)
28	26, 27	cbvraldva2 2513	. . . . . 6 ⊢ ((𝑎 = x ∧ 𝑏 = y) → (∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
29	28	cbvexdva 1786	. . . . 5 ⊢ (𝑎 = x → (∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)))
30	29	cbvalv 1776	. . . 4 ⊢ (∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒) ↔ ∀x∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u))
31		acexmid.choice	. . . 4 ⊢ ∃y∀z ∈ x ∀w ∈ z ∃!v ∈ z ∃u ∈ y (z ∈ u ∧ v ∈ u)
32	30, 31	mpgbir 1321	. . 3 ⊢ ∀𝑎∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)
33	32	spi 1412	. 2 ⊢ ∃𝑏∀𝑐 ∈ 𝑎 ∀𝑑 ∈ 𝑐 ∃!f ∈ 𝑐 ∃𝑒 ∈ 𝑏 (𝑐 ∈ 𝑒 ∧ f ∈ 𝑒)
34	33	acexmidlemv 5403	1 ⊢ (φ ∨ ¬ φ)

Syntax hints:  ¬ wn 3   ∧ wa 97   ↔ wb 98   ∨ wo 616   ∧ w3a 875  ∀wal 1314  ∃wex 1361  [wsb 1627  ∃!weu 1881  ∀wral 2282  ∃wrex 2283  ∃!wreu 2284

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 532  ax-in2 533  ax-io 617  ax-5 1315  ax-7 1316  ax-gen 1317  ax-ie1 1362  ax-ie2 1363  ax-8 1377  ax-10 1378  ax-11 1379  ax-i12 1380  ax-bnd 1381  ax-4 1382  ax-14 1387  ax-17 1401  ax-i9 1405  ax-ial 1410  ax-i5r 1411  ax-ext 2004  ax-sep 3827  ax-nul 3835  ax-pow 3879  ax-pr 3896

This theorem depends on definitions:  df-bi 110  df-3or 876  df-3an 877  df-tru 1231  df-nf 1329  df-sb 1628  df-eu 1884  df-clab 2009  df-cleq 2015  df-clel 2018  df-nfc 2149  df-ral 2287  df-rex 2288  df-reu 2289  df-rab 2291  df-v 2535  df-sbc 2740  df-dif 2898  df-un 2900  df-in 2902  df-ss 2909  df-nul 3203  df-pw 3313  df-sn 3333  df-pr 3334  df-uni 3533  df-tr 3807  df-iord 4027  df-on 4028  df-suc 4031  df-iota 4761  df-riota 5360

This theorem is referenced by: (None)