Theorem exmid 186

Description: Diaconescu's theorem, which derives the law of the excluded middle from the axiom of choice.

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 180	. . 3 |- @:((* -> *) -> *)
2		wor 130	. . . . 5 |- \/ :(* -> (* -> *))
3		wv 58	. . . . 5 |- x:*:*
4		exmid.1	. . . . 5 |- A:*
5	2, 3, 4	wov 64	. . . 4 |- [x:* \/ A]:*
6	5	wl 59	. . 3 |- \x:* [x:* \/ A]:(* -> *)
7	1, 6	wc 45	. 2 |- (@\x:* [x:* \/ A]):*
8		wnot 128	. . . 4 |- ~ :(* -> *)
9	8, 4	wc 45	. . 3 |- (~ A):*
10	2, 4, 9	wov 64	. 2 |- [A \/ (~ A)]:*
11		wtru 40	. . . . . 6 |- T.:*
12	11, 4	orc 155	. . . . 5 |- T. |= [T. \/ A]
13	3, 11	weqi 68	. . . . . . . 8 |- [x:* = T.]:*
14	13	id 25	. . . . . . 7 |- [x:* = T.] |= [x:* = T.]
15	2, 3, 4, 14	oveq1 89	. . . . . 6 |- [x:* = T.] |= [[x:* \/ A] = [T. \/ A]]
16	5, 11, 15	cl 106	. . . . 5 |- T. |= [(\x:* [x:* \/ A]T.) = [T. \/ A]]
17	12, 16	mpbir 77	. . . 4 |- T. |= (\x:* [x:* \/ A]T.)
18	6, 11	ac 184	. . . 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 68	. . . . . 6 |- [x:* = (@\x:* [x:* \/ A])]:*
21	20	id 25	. . . . 5 |- [x:* = (@\x:* [x:* \/ A])] |= [x:* = (@\x:* [x:* \/ A])]
22	2, 3, 4, 21	oveq1 89	. . . 4 |- [x:* = (@\x:* [x:* \/ A])] |= [[x:* \/ A] = [(@\x:* [x:* \/ A]) \/ A]]
23		wv 58	. . . . 5 |- y:*:*
24	2, 23	ax-17 95	. . . . 5 |- T. |= [(\x:* \/ y:*) = \/ ]
25	1, 23	ax-17 95	. . . . . 6 |- T. |= [(\x:* @y:*) = @]
26	5, 23	ax-hbl1 93	. . . . . 6 |- T. |= [(\x:* \x:* [x:* \/ A]y:*) = \x:* [x:* \/ A]]
27	1, 6, 23, 25, 26	hbc 100	. . . . 5 |- T. |= [(\x:* (@\x:* [x:* \/ A])y:*) = (@\x:* [x:* \/ A])]
28	4, 23	ax-17 95	. . . . 5 |- T. |= [(\x:* Ay:*) = A]
29	2, 7, 23, 4, 24, 27, 28	hbov 101	. . . 4 |- T. |= [(\x:* [(@\x:* [x:* \/ A]) \/ A]y:*) = [(@\x:* [x:* \/ A]) \/ A]]
30	5, 7, 22, 29, 27	clf 105	. . 3 |- T. |= [(\x:* [x:* \/ A](@\x:* [x:* \/ A])) = [(@\x:* [x:* \/ A]) \/ A]]
31	19, 30	mpbi 72	. 2 |- T. |= [(@\x:* [x:* \/ A]) \/ A]
32	8, 3	wc 45	. . . . . . . 8 |- (~ x:*):*
33	2, 32, 4	wov 64	. . . . . . 7 |- [(~ x:*) \/ A]:*
34	33	wl 59	. . . . . 6 |- \x:* [(~ x:*) \/ A]:(* -> *)
35	1, 34	wc 45	. . . . 5 |- (@\x:* [(~ x:*) \/ A]):*
36	8, 35	wc 45	. . . 4 |- (~ (@\x:* [(~ x:*) \/ A])):*
37		wfal 125	. . . . . . . . 9 |- F.:*
38	3, 37	weqi 68	. . . . . . . . . . . . 13 |- [x:* = F.]:*
39	38	id 25	. . . . . . . . . . . 12 |- [x:* = F.] |= [x:* = F.]
40	8, 3, 39	ceq2 80	. . . . . . . . . . 11 |- [x:* = F.] |= [(~ x:*) = (~ F.)]
41	11, 37	simpr 23	. . . . . . . . . . . . . . . 16 |- (T., F.) |= F.
42	41	ex 148	. . . . . . . . . . . . . . 15 |- T. |= [F. ==> F.]
43	37	notval 135	. . . . . . . . . . . . . . 15 |- T. |= [(~ F.) = [F. ==> F.]]
44	42, 43	mpbir 77	. . . . . . . . . . . . . 14 |- T. |= (~ F.)
45	44	eqtru 76	. . . . . . . . . . . . 13 |- T. |= [T. = (~ F.)]
46	11, 45	eqcomi 70	. . . . . . . . . . . 12 |- T. |= [(~ F.) = T.]
47	38, 46	a1i 28	. . . . . . . . . . 11 |- [x:* = F.] |= [(~ F.) = T.]
48	32, 40, 47	eqtri 85	. . . . . . . . . 10 |- [x:* = F.] |= [(~ x:*) = T.]
49	2, 32, 4, 48	oveq1 89	. . . . . . . . 9 |- [x:* = F.] |= [[(~ x:*) \/ A] = [T. \/ A]]
50	33, 37, 49	cl 106	. . . . . . . 8 |- T. |= [(\x:* [(~ x:*) \/ A]F.) = [T. \/ A]]
51	12, 50	mpbir 77	. . . . . . 7 |- T. |= (\x:* [(~ x:*) \/ A]F.)
52	34, 37	ac 184	. . . . . . 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 68	. . . . . . . . . 10 |- [x:* = (@\x:* [(~ x:*) \/ A])]:*
55	54	id 25	. . . . . . . . 9 |- [x:* = (@\x:* [(~ x:*) \/ A])] |= [x:* = (@\x:* [(~ x:*) \/ A])]
56	8, 3, 55	ceq2 80	. . . . . . . 8 |- [x:* = (@\x:* [(~ x:*) \/ A])] |= [(~ x:*) = (~ (@\x:* [(~ x:*) \/ A]))]
57	2, 32, 4, 56	oveq1 89	. . . . . . 7 |- [x:* = (@\x:* [(~ x:*) \/ A])] |= [[(~ x:*) \/ A] = [(~ (@\x:* [(~ x:*) \/ A])) \/ A]]
58	8, 23	ax-17 95	. . . . . . . . 9 |- T. |= [(\x:* ~ y:*) = ~ ]
59	33, 23	ax-hbl1 93	. . . . . . . . . 10 |- T. |= [(\x:* \x:* [(~ x:*) \/ A]y:*) = \x:* [(~ x:*) \/ A]]
60	1, 34, 23, 25, 59	hbc 100	. . . . . . . . 9 |- T. |= [(\x:* (@\x:* [(~ x:*) \/ A])y:*) = (@\x:* [(~ x:*) \/ A])]
61	8, 35, 23, 58, 60	hbc 100	. . . . . . . 8 |- T. |= [(\x:* (~ (@\x:* [(~ x:*) \/ A]))y:*) = (~ (@\x:* [(~ x:*) \/ A]))]
62	2, 36, 23, 4, 24, 61, 28	hbov 101	. . . . . . 7 |- T. |= [(\x:* [(~ (@\x:* [(~ x:*) \/ A])) \/ A]y:*) = [(~ (@\x:* [(~ x:*) \/ A])) \/ A]]
63	33, 35, 57, 62, 60	clf 105	. . . . . 6 |- T. |= [(\x:* [(~ x:*) \/ A](@\x:* [(~ x:*) \/ A])) = [(~ (@\x:* [(~ x:*) \/ A])) \/ A]]
64	53, 63	mpbi 72	. . . . 5 |- T. |= [(~ (@\x:* [(~ x:*) \/ A])) \/ A]
65	7, 64	a1i 28	. . . 4 |- (@\x:* [x:* \/ A]) |= [(~ (@\x:* [(~ x:*) \/ A])) \/ A]
66	7, 36	wct 44	. . . . . . . . . . 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 35	. . . . . . . . 9 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= (@\x:* [x:* \/ A])
69	3, 4	olc 154	. . . . . . . . . . . . . . 15 |- A |= [x:* \/ A]
70	69	eqtru 76	. . . . . . . . . . . . . 14 |- A |= [T. = [x:* \/ A]]
71	11, 70	eqcomi 70	. . . . . . . . . . . . 13 |- A |= [[x:* \/ A] = T.]
72	32, 4	olc 154	. . . . . . . . . . . . . 14 |- A |= [(~ x:*) \/ A]
73	72	eqtru 76	. . . . . . . . . . . . 13 |- A |= [T. = [(~ x:*) \/ A]]
74	5, 71, 73	eqtri 85	. . . . . . . . . . . 12 |- A |= [[x:* \/ A] = [(~ x:*) \/ A]]
75	5, 74	leq 81	. . . . . . . . . . 11 |- A |= [\x:* [x:* \/ A] = \x:* [(~ x:*) \/ A]]
76	1, 6, 75	ceq2 80	. . . . . . . . . 10 |- A |= [(@\x:* [x:* \/ A]) = (@\x:* [(~ x:*) \/ A])]
77	76, 66	adantl 51	. . . . . . . . 9 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= [(@\x:* [x:* \/ A]) = (@\x:* [(~ x:*) \/ A])]
78	68, 77	mpbi 72	. . . . . . . 8 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= (@\x:* [(~ x:*) \/ A])
79	67	simprd 36	. . . . . . . . 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 135	. . . . . . . . . 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 72	. . . . . . . 8 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= [(@\x:* [(~ x:*) \/ A]) ==> F.]
84	37, 78, 83	mpd 146	. . . . . . 7 |- (((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))), A) |= F.
85	84	ex 148	. . . . . 6 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= [A ==> F.]
86	4	notval 135	. . . . . . 7 |- T. |= [(~ A) = [A ==> F.]]
87	66, 86	a1i 28	. . . . . 6 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= [(~ A) = [A ==> F.]]
88	85, 87	mpbir 77	. . . . 5 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= (~ A)
89	4, 9	olc 154	. . . . 5 |- (~ A) |= [A \/ (~ A)]
90	88, 89	syl 16	. . . 4 |- ((@\x:* [x:* \/ A]), (~ (@\x:* [(~ x:*) \/ A]))) |= [A \/ (~ A)]
91	4, 9	orc 155	. . . . 5 |- A |= [A \/ (~ A)]
92	91, 7	adantl 51	. . . 4 |- ((@\x:* [x:* \/ A]), A) |= [A \/ (~ A)]
93	36, 4, 10, 65, 90, 92	ecase 153	. . 3 |- (@\x:* [x:* \/ A]) |= [A \/ (~ A)]
94	93, 11	adantl 51	. 2 |- (T., (@\x:* [x:* \/ A])) |= [A \/ (~ A)]
95	91, 11	adantl 51	. 2 |- (T., A) |= [A \/ (~ A)]
96	7, 4, 10, 31, 94, 95	ecase 153	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 108  ~ tne 110   ==> tim 111   \/ tor 114  @tat 179

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-refl 39  ax-eqmp 42  ax-ded 43  ax-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103  ax-ac 183

This theorem depends on definitions:  df-ov 65  df-al 116  df-fal 117  df-an 118  df-im 119  df-not 120  df-or 122

This theorem is referenced by:  notnot  187  ax3  192