Theorem exmid 199

Description: Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice. (Contributed by Mario Carneiro, 10-Oct-2014.)

Hypothesis

Ref	Expression
exmid.1	⊢ A:∗

Assertion

Ref	Expression
exmid	⊢ ⊤⊧[A ∨ (¬ A)]

Proof of Theorem exmid

Dummy variables x y are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wat 193	. . 3 ⊢ ε:((∗ → ∗) → ∗)
2		wor 140	. . . . 5 ⊢ ∨ :(∗ → (∗ → ∗))
3		wv 64	. . . . 5 ⊢ x:∗:∗
4		exmid.1	. . . . 5 ⊢ A:∗
5	2, 3, 4	wov 72	. . . 4 ⊢ [x:∗ ∨ A]:∗
6	5	wl 66	. . 3 ⊢ λx:∗ [x:∗ ∨ A]:(∗ → ∗)
7	1, 6	wc 50	. 2 ⊢ (ελx:∗ [x:∗ ∨ A]):∗
8		wnot 138	. . . 4 ⊢ ¬ :(∗ → ∗)
9	8, 4	wc 50	. . 3 ⊢ (¬ A):∗
10	2, 4, 9	wov 72	. 2 ⊢ [A ∨ (¬ A)]:∗
11		wtru 43	. . . . . 6 ⊢ ⊤:∗
12	11, 4	orc 165	. . . . 5 ⊢ ⊤⊧[⊤ ∨ A]
13	3, 11	weqi 76	. . . . . . . 8 ⊢ [x:∗ = ⊤]:∗
14	13	id 25	. . . . . . 7 ⊢ [x:∗ = ⊤]⊧[x:∗ = ⊤]
15	2, 3, 4, 14	oveq1 99	. . . . . 6 ⊢ [x:∗ = ⊤]⊧[[x:∗ ∨ A] = [⊤ ∨ A]]
16	5, 11, 15	cl 116	. . . . 5 ⊢ ⊤⊧[(λx:∗ [x:∗ ∨ A]⊤) = [⊤ ∨ A]]
17	12, 16	mpbir 87	. . . 4 ⊢ ⊤⊧(λx:∗ [x:∗ ∨ A]⊤)
18	6, 11	ac 197	. . . 4 ⊢ (λx:∗ [x:∗ ∨ A]⊤)⊧(λx:∗ [x:∗ ∨ A](ελx:∗ [x:∗ ∨ A]))
19	17, 18	syl 16	. . 3 ⊢ ⊤⊧(λx:∗ [x:∗ ∨ A](ελx:∗ [x:∗ ∨ A]))
20	3, 7	weqi 76	. . . . . 6 ⊢ [x:∗ = (ελx:∗ [x:∗ ∨ A])]:∗
21	20	id 25	. . . . 5 ⊢ [x:∗ = (ελx:∗ [x:∗ ∨ A])]⊧[x:∗ = (ελx:∗ [x:∗ ∨ A])]
22	2, 3, 4, 21	oveq1 99	. . . 4 ⊢ [x:∗ = (ελx:∗ [x:∗ ∨ A])]⊧[[x:∗ ∨ A] = [(ελx:∗ [x:∗ ∨ A]) ∨ A]]
23		wv 64	. . . . 5 ⊢ y:∗:∗
24	2, 23	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:∗ ∨ y:∗) = ∨ ]
25	1, 23	ax-17 105	. . . . . 6 ⊢ ⊤⊧[(λx:∗ εy:∗) = ε]
26	5, 23	ax-hbl1 103	. . . . . 6 ⊢ ⊤⊧[(λx:∗ λx:∗ [x:∗ ∨ A]y:∗) = λx:∗ [x:∗ ∨ A]]
27	1, 6, 23, 25, 26	hbc 110	. . . . 5 ⊢ ⊤⊧[(λx:∗ (ελx:∗ [x:∗ ∨ A])y:∗) = (ελx:∗ [x:∗ ∨ A])]
28	4, 23	ax-17 105	. . . . 5 ⊢ ⊤⊧[(λx:∗ Ay:∗) = A]
29	2, 7, 23, 4, 24, 27, 28	hbov 111	. . . 4 ⊢ ⊤⊧[(λx:∗ [(ελx:∗ [x:∗ ∨ A]) ∨ A]y:∗) = [(ελx:∗ [x:∗ ∨ A]) ∨ A]]
30	5, 7, 22, 29, 27	clf 115	. . 3 ⊢ ⊤⊧[(λx:∗ [x:∗ ∨ A](ελx:∗ [x:∗ ∨ A])) = [(ελx:∗ [x:∗ ∨ A]) ∨ A]]
31	19, 30	mpbi 82	. 2 ⊢ ⊤⊧[(ελx:∗ [x:∗ ∨ A]) ∨ A]
32	8, 3	wc 50	. . . . . . . 8 ⊢ (¬ x:∗):∗
33	2, 32, 4	wov 72	. . . . . . 7 ⊢ [(¬ x:∗) ∨ A]:∗
34	33	wl 66	. . . . . 6 ⊢ λx:∗ [(¬ x:∗) ∨ A]:(∗ → ∗)
35	1, 34	wc 50	. . . . 5 ⊢ (ελx:∗ [(¬ x:∗) ∨ A]):∗
36	8, 35	wc 50	. . . 4 ⊢ (¬ (ελx:∗ [(¬ x:∗) ∨ A])):∗
37		wfal 135	. . . . . . . . 9 ⊢ ⊥:∗
38	3, 37	weqi 76	. . . . . . . . . . . . 13 ⊢ [x:∗ = ⊥]:∗
39	38	id 25	. . . . . . . . . . . 12 ⊢ [x:∗ = ⊥]⊧[x:∗ = ⊥]
40	8, 3, 39	ceq2 90	. . . . . . . . . . 11 ⊢ [x:∗ = ⊥]⊧[(¬ x:∗) = (¬ ⊥)]
41	11, 37	simpr 23	. . . . . . . . . . . . . . . 16 ⊢ (⊤, ⊥)⊧⊥
42	41	ex 158	. . . . . . . . . . . . . . 15 ⊢ ⊤⊧[⊥ ⇒ ⊥]
43	37	notval 145	. . . . . . . . . . . . . . 15 ⊢ ⊤⊧[(¬ ⊥) = [⊥ ⇒ ⊥]]
44	42, 43	mpbir 87	. . . . . . . . . . . . . 14 ⊢ ⊤⊧(¬ ⊥)
45	44	eqtru 86	. . . . . . . . . . . . 13 ⊢ ⊤⊧[⊤ = (¬ ⊥)]
46	11, 45	eqcomi 79	. . . . . . . . . . . 12 ⊢ ⊤⊧[(¬ ⊥) = ⊤]
47	38, 46	a1i 28	. . . . . . . . . . 11 ⊢ [x:∗ = ⊥]⊧[(¬ ⊥) = ⊤]
48	32, 40, 47	eqtri 95	. . . . . . . . . 10 ⊢ [x:∗ = ⊥]⊧[(¬ x:∗) = ⊤]
49	2, 32, 4, 48	oveq1 99	. . . . . . . . 9 ⊢ [x:∗ = ⊥]⊧[[(¬ x:∗) ∨ A] = [⊤ ∨ A]]
50	33, 37, 49	cl 116	. . . . . . . 8 ⊢ ⊤⊧[(λx:∗ [(¬ x:∗) ∨ A]⊥) = [⊤ ∨ A]]
51	12, 50	mpbir 87	. . . . . . 7 ⊢ ⊤⊧(λx:∗ [(¬ x:∗) ∨ A]⊥)
52	34, 37	ac 197	. . . . . . 7 ⊢ (λx:∗ [(¬ x:∗) ∨ A]⊥)⊧(λx:∗ [(¬ x:∗) ∨ A](ελx:∗ [(¬ x:∗) ∨ A]))
53	51, 52	syl 16	. . . . . 6 ⊢ ⊤⊧(λx:∗ [(¬ x:∗) ∨ A](ελx:∗ [(¬ x:∗) ∨ A]))
54	3, 35	weqi 76	. . . . . . . . . 10 ⊢ [x:∗ = (ελx:∗ [(¬ x:∗) ∨ A])]:∗
55	54	id 25	. . . . . . . . 9 ⊢ [x:∗ = (ελx:∗ [(¬ x:∗) ∨ A])]⊧[x:∗ = (ελx:∗ [(¬ x:∗) ∨ A])]
56	8, 3, 55	ceq2 90	. . . . . . . 8 ⊢ [x:∗ = (ελx:∗ [(¬ x:∗) ∨ A])]⊧[(¬ x:∗) = (¬ (ελx:∗ [(¬ x:∗) ∨ A]))]
57	2, 32, 4, 56	oveq1 99	. . . . . . 7 ⊢ [x:∗ = (ελx:∗ [(¬ x:∗) ∨ A])]⊧[[(¬ x:∗) ∨ A] = [(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]]
58	8, 23	ax-17 105	. . . . . . . . 9 ⊢ ⊤⊧[(λx:∗ ¬ y:∗) = ¬ ]
59	33, 23	ax-hbl1 103	. . . . . . . . . 10 ⊢ ⊤⊧[(λx:∗ λx:∗ [(¬ x:∗) ∨ A]y:∗) = λx:∗ [(¬ x:∗) ∨ A]]
60	1, 34, 23, 25, 59	hbc 110	. . . . . . . . 9 ⊢ ⊤⊧[(λx:∗ (ελx:∗ [(¬ x:∗) ∨ A])y:∗) = (ελx:∗ [(¬ x:∗) ∨ A])]
61	8, 35, 23, 58, 60	hbc 110	. . . . . . . 8 ⊢ ⊤⊧[(λx:∗ (¬ (ελx:∗ [(¬ x:∗) ∨ A]))y:∗) = (¬ (ελx:∗ [(¬ x:∗) ∨ A]))]
62	2, 36, 23, 4, 24, 61, 28	hbov 111	. . . . . . 7 ⊢ ⊤⊧[(λx:∗ [(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]y:∗) = [(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]]
63	33, 35, 57, 62, 60	clf 115	. . . . . 6 ⊢ ⊤⊧[(λx:∗ [(¬ x:∗) ∨ A](ελx:∗ [(¬ x:∗) ∨ A])) = [(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]]
64	53, 63	mpbi 82	. . . . 5 ⊢ ⊤⊧[(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]
65	7, 64	a1i 28	. . . 4 ⊢ (ελx:∗ [x:∗ ∨ A])⊧[(¬ (ελx:∗ [(¬ x:∗) ∨ A])) ∨ A]
66	7, 36	wct 48	. . . . . . . . . . 11 ⊢ ((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))):∗
67	66, 4	simpl 22	. . . . . . . . . 10 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A])))
68	67	simpld 37	. . . . . . . . 9 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧(ελx:∗ [x:∗ ∨ A])
69	3, 4	olc 164	. . . . . . . . . . . . . . 15 ⊢ A⊧[x:∗ ∨ A]
70	69	eqtru 86	. . . . . . . . . . . . . 14 ⊢ A⊧[⊤ = [x:∗ ∨ A]]
71	11, 70	eqcomi 79	. . . . . . . . . . . . 13 ⊢ A⊧[[x:∗ ∨ A] = ⊤]
72	32, 4	olc 164	. . . . . . . . . . . . . 14 ⊢ A⊧[(¬ x:∗) ∨ A]
73	72	eqtru 86	. . . . . . . . . . . . 13 ⊢ A⊧[⊤ = [(¬ x:∗) ∨ A]]
74	5, 71, 73	eqtri 95	. . . . . . . . . . . 12 ⊢ A⊧[[x:∗ ∨ A] = [(¬ x:∗) ∨ A]]
75	5, 74	leq 91	. . . . . . . . . . 11 ⊢ A⊧[λx:∗ [x:∗ ∨ A] = λx:∗ [(¬ x:∗) ∨ A]]
76	1, 6, 75	ceq2 90	. . . . . . . . . 10 ⊢ A⊧[(ελx:∗ [x:∗ ∨ A]) = (ελx:∗ [(¬ x:∗) ∨ A])]
77	76, 66	adantl 56	. . . . . . . . 9 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧[(ελx:∗ [x:∗ ∨ A]) = (ελx:∗ [(¬ x:∗) ∨ A])]
78	68, 77	mpbi 82	. . . . . . . 8 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧(ελx:∗ [(¬ x:∗) ∨ A])
79	67	simprd 38	. . . . . . . . 9 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧(¬ (ελx:∗ [(¬ x:∗) ∨ A]))
80	67	ax-cb1 29	. . . . . . . . . 10 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A):∗
81	35	notval 145	. . . . . . . . . 10 ⊢ ⊤⊧[(¬ (ελx:∗ [(¬ x:∗) ∨ A])) = [(ελx:∗ [(¬ x:∗) ∨ A]) ⇒ ⊥]]
82	80, 81	a1i 28	. . . . . . . . 9 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧[(¬ (ελx:∗ [(¬ x:∗) ∨ A])) = [(ελx:∗ [(¬ x:∗) ∨ A]) ⇒ ⊥]]
83	79, 82	mpbi 82	. . . . . . . 8 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧[(ελx:∗ [(¬ x:∗) ∨ A]) ⇒ ⊥]
84	37, 78, 83	mpd 156	. . . . . . 7 ⊢ (((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A]))), A)⊧⊥
85	84	ex 158	. . . . . 6 ⊢ ((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A])))⊧[A ⇒ ⊥]
86	4	notval 145	. . . . . . 7 ⊢ ⊤⊧[(¬ A) = [A ⇒ ⊥]]
87	66, 86	a1i 28	. . . . . 6 ⊢ ((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A])))⊧[(¬ A) = [A ⇒ ⊥]]
88	85, 87	mpbir 87	. . . . 5 ⊢ ((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A])))⊧(¬ A)
89	4, 9	olc 164	. . . . 5 ⊢ (¬ A)⊧[A ∨ (¬ A)]
90	88, 89	syl 16	. . . 4 ⊢ ((ελx:∗ [x:∗ ∨ A]), (¬ (ελx:∗ [(¬ x:∗) ∨ A])))⊧[A ∨ (¬ A)]
91	4, 9	orc 165	. . . . 5 ⊢ A⊧[A ∨ (¬ A)]
92	91, 7	adantl 56	. . . 4 ⊢ ((ελx:∗ [x:∗ ∨ A]), A)⊧[A ∨ (¬ A)]
93	36, 4, 10, 65, 90, 92	ecase 163	. . 3 ⊢ (ελx:∗ [x:∗ ∨ A])⊧[A ∨ (¬ A)]
94	93, 11	adantl 56	. 2 ⊢ (⊤, (ελx:∗ [x:∗ ∨ A]))⊧[A ∨ (¬ A)]
95	91, 11	adantl 56	. 2 ⊢ (⊤, A)⊧[A ∨ (¬ A)]
96	7, 4, 10, 31, 94, 95	ecase 163	1 ⊢ ⊤⊧[A ∨ (¬ A)]

This proof depends on syntax axioms:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  kct 10  ⊧wffMMJ2 11  wffMMJ2t 12  ⊥tfal 118  ¬ tne 120   ⇒ tim 121   ∨ tor 124  εtat 191

This proof depends on axioms:  ax-syl 15  ax-jca 17  ax-simpl 20  ax-simpr 21  ax-id 24  ax-trud 26  ax-cb1 29  ax-cb2 30  ax-wctl 31  ax-wctr 32  ax-weq 40  ax-refl 42  ax-eqmp 45  ax-ded 46  ax-wct 47  ax-wc 49  ax-ceq 51  ax-wv 63  ax-wl 65  ax-beta 67  ax-distrc 68  ax-leq 69  ax-distrl 70  ax-wov 71  ax-eqtypi 77  ax-eqtypri 80  ax-hbl1 103  ax-17 105  ax-inst 113  ax-wat 192  ax-ac 196

This proof depends on definitions:  df-ov 73  df-al 126  df-fal 127  df-an 128  df-im 129  df-not 130  df-or 132

This theorem is used by:  notnot  200  ax3  205