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	|- T. |= [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 |- T.:*
12	11, 4	orc 165	. . . . 5 |- T. |= [T. \/ A]
13	3, 11	weqi 76	. . . . . . . 8 |- [x:* = T.]:*
14	13	id 25	. . . . . . 7 |- [x:* = T.] |= [x:* = T.]
15	2, 3, 4, 14	oveq1 99	. . . . . 6 |- [x:* = T.] |= [[x:* \/ A] = [T. \/ A]]
16	5, 11, 15	cl 116	. . . . 5 |- T. |= [(\x:* [x:* \/ A]T.) = [T. \/ A]]
17	12, 16	mpbir 87	. . . 4 |- T. |= (\x:* [x:* \/ A]T.)
18	6, 11	ac 197	. . . 4 |- (\x:* [x:* \/ A]T.) |= (\x:* [x:* \/ A](@\x:* [x:* \/ A]))
19	17, 18	syl 16	. . 3 |- T. |= (\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 |- T. |= [(\x:* \/ y:*) = \/ ]
25	1, 23	ax-17 105	. . . . . 6 |- T. |= [(\x:* @y:*) = @]
26	5, 23	ax-hbl1 103	. . . . . 6 |- T. |= [(\x:* \x:* [x:* \/ A]y:*) = \x:* [x:* \/ A]]
27	1, 6, 23, 25, 26	hbc 110	. . . . 5 |- T. |= [(\x:* (@\x:* [x:* \/ A])y:*) = (@\x:* [x:* \/ A])]
28	4, 23	ax-17 105	. . . . 5 |- T. |= [(\x:* Ay:*) = A]
29	2, 7, 23, 4, 24, 27, 28	hbov 111	. . . 4 |- T. |= [(\x:* [(@\x:* [x:* \/ A]) \/ A]y:*) = [(@\x:* [x:* \/ A]) \/ A]]
30	5, 7, 22, 29, 27	clf 115	. . 3 |- T. |= [(\x:* [x:* \/ A](@\x:* [x:* \/ A])) = [(@\x:* [x:* \/ A]) \/ A]]
31	19, 30	mpbi 82	. 2 |- T. |= [(@\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 |- F.:*
38	3, 37	weqi 76	. . . . . . . . . . . . 13 |- [x:* = F.]:*
39	38	id 25	. . . . . . . . . . . 12 |- [x:* = F.] |= [x:* = F.]
40	8, 3, 39	ceq2 90	. . . . . . . . . . 11 |- [x:* = F.] |= [(~ x:*) = (~ F.)]
41	11, 37	simpr 23	. . . . . . . . . . . . . . . 16 |- (T., F.) |= F.
42	41	ex 158	. . . . . . . . . . . . . . 15 |- T. |= [F. ==> F.]
43	37	notval 145	. . . . . . . . . . . . . . 15 |- T. |= [(~ F.) = [F. ==> F.]]
44	42, 43	mpbir 87	. . . . . . . . . . . . . 14 |- T. |= (~ F.)
45	44	eqtru 86	. . . . . . . . . . . . 13 |- T. |= [T. = (~ F.)]
46	11, 45	eqcomi 79	. . . . . . . . . . . 12 |- T. |= [(~ F.) = T.]
47	38, 46	a1i 28	. . . . . . . . . . 11 |- [x:* = F.] |= [(~ F.) = T.]
48	32, 40, 47	eqtri 95	. . . . . . . . . 10 |- [x:* = F.] |= [(~ x:*) = T.]
49	2, 32, 4, 48	oveq1 99	. . . . . . . . 9 |- [x:* = F.] |= [[(~ x:*) \/ A] = [T. \/ A]]
50	33, 37, 49	cl 116	. . . . . . . 8 |- T. |= [(\x:* [(~ x:*) \/ A]F.) = [T. \/ A]]
51	12, 50	mpbir 87	. . . . . . 7 |- T. |= (\x:* [(~ x:*) \/ A]F.)
52	34, 37	ac 197	. . . . . . 7 |- (\x:* [(~ x:*) \/ A]F.) |= (\x:* [(~ x:*) \/ A](@\x:* [(~ x:*) \/ A]))
53	51, 52	syl 16	. . . . . 6 |- T. |= (\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 |- T. |= [(\x:* ~ y:*) = ~ ]
59	33, 23	ax-hbl1 103	. . . . . . . . . 10 |- T. |= [(\x:* \x:* [(~ x:*) \/ A]y:*) = \x:* [(~ x:*) \/ A]]
60	1, 34, 23, 25, 59	hbc 110	. . . . . . . . 9 |- T. |= [(\x:* (@\x:* [(~ x:*) \/ A])y:*) = (@\x:* [(~ x:*) \/ A])]
61	8, 35, 23, 58, 60	hbc 110	. . . . . . . 8 |- T. |= [(\x:* (~ (@\x:* [(~ x:*) \/ A]))y:*) = (~ (@\x:* [(~ x:*) \/ A]))]
62	2, 36, 23, 4, 24, 61, 28	hbov 111	. . . . . . 7 |- T. |= [(\x:* [(~ (@\x:* [(~ x:*) \/ A])) \/ A]y:*) = [(~ (@\x:* [(~ x:*) \/ A])) \/ A]]
63	33, 35, 57, 62, 60	clf 115	. . . . . 6 |- T. |= [(\x:* [(~ x:*) \/ A](@\x:* [(~ x:*) \/ A])) = [(~ (@\x:* [(~ x:*) \/ A])) \/ A]]
64	53, 63	mpbi 82	. . . . 5 |- T. |= [(~ (@\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 |= [T. = [x:* \/ A]]
71	11, 70	eqcomi 79	. . . . . . . . . . . . 13 |- A |= [[x:* \/ A] = T.]
72	32, 4	olc 164	. . . . . . . . . . . . . 14 |- A |= [(~ x:*) \/ A]
73	72	eqtru 86	. . . . . . . . . . . . 13 |- A |= [T. = [(~ 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 |- T. |= [(~ (@\x:* [(~ x:*) \/ A])) = [(@\x:* [(~ x:*) \/ A]) ==> F.]]
82	80, 81	a1i 28	. . . . . . . . 9 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= [(~ (@\x:* [(~ x:*) \/ A])) = [(@\x:* [(~ x:*) \/ A]) ==> F.]]
83	79, 82	mpbi 82	. . . . . . . 8 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= [(@\x:* [(~ x:*) \/ A]) ==> F.]
84	37, 78, 83	mpd 156	. . . . . . 7 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= F.
85	84	ex 158	. . . . . 6 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= [A ==> F.]
86	4	notval 145	. . . . . . 7 |- T. |= [(~ A) = [A ==> F.]]
87	66, 86	a1i 28	. . . . . 6 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= [(~ A) = [A ==> F.]]
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 |- (T., (@\x:* [x:* \/ A])) |= [A \/ (~ A)]
95	91, 11	adantl 56	. 2 |- (T., A) |= [A \/ (~ A)]
96	7, 4, 10, 31, 94, 95	ecase 163	1 |- T. |= [A \/ (~ A)]

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9  kct 10   |= wffMMJ2 11  wffMMJ2t 12  F.tfal 118  ~ tne 120   ==> tim 121   \/ tor 124  @tat 191

This theorem was proved from 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 theorem 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 referenced by:  notnot  200  ax3  205