Theorem orval 147

Description: Value of the disjunction. (Contributed by Mario Carneiro, 9-Oct-2014.)

Hypotheses

Ref	Expression
imval.1	|- A:*
imval.2	|- B:*

Assertion

Ref	Expression
orval	|- T. |= [[A \/ B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]

Distinct variable groups:   x,A   x,B

Proof of Theorem orval

Dummy variables p q are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		wor 140	. . 3 |- \/ :(* -> (* -> *))
2		imval.1	. . 3 |- A:*
3		imval.2	. . 3 |- B:*
4	1, 2, 3	wov 72	. 2 |- [A \/ B]:*
5		df-or 132	. . 3 |- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
6	1, 2, 3, 5	oveq 102	. 2 |- T. |= [[A \/ B] = [A\p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])B]]
7		wal 134	. . . 4 |- A.:((* -> *) -> *)
8		wim 137	. . . . . 6 |- ==> :(* -> (* -> *))
9		wv 64	. . . . . . 7 |- p:*:*
10		wv 64	. . . . . . 7 |- x:*:*
11	8, 9, 10	wov 72	. . . . . 6 |- [p:* ==> x:*]:*
12		wv 64	. . . . . . . 8 |- q:*:*
13	8, 12, 10	wov 72	. . . . . . 7 |- [q:* ==> x:*]:*
14	8, 13, 10	wov 72	. . . . . 6 |- [[q:* ==> x:*] ==> x:*]:*
15	8, 11, 14	wov 72	. . . . 5 |- [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:*
16	15	wl 66	. . . 4 |- \x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:(* -> *)
17	7, 16	wc 50	. . 3 |- (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]):*
18	9, 2	weqi 76	. . . . . . . 8 |- [p:* = A]:*
19	18	id 25	. . . . . . 7 |- [p:* = A] |= [p:* = A]
20	8, 9, 10, 19	oveq1 99	. . . . . 6 |- [p:* = A] |= [[p:* ==> x:*] = [A ==> x:*]]
21	8, 11, 14, 20	oveq1 99	. . . . 5 |- [p:* = A] |= [[[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]]
22	15, 21	leq 91	. . . 4 |- [p:* = A] |= [\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = \x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]]
23	7, 16, 22	ceq2 90	. . 3 |- [p:* = A] |= [(A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]) = (A.\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
24	8, 2, 10	wov 72	. . . . . 6 |- [A ==> x:*]:*
25	8, 24, 14	wov 72	. . . . 5 |- [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:*
26	25	wl 66	. . . 4 |- \x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:(* -> *)
27	12, 3	weqi 76	. . . . . . . . 9 |- [q:* = B]:*
28	27	id 25	. . . . . . . 8 |- [q:* = B] |= [q:* = B]
29	8, 12, 10, 28	oveq1 99	. . . . . . 7 |- [q:* = B] |= [[q:* ==> x:*] = [B ==> x:*]]
30	8, 13, 10, 29	oveq1 99	. . . . . 6 |- [q:* = B] |= [[[q:* ==> x:*] ==> x:*] = [[B ==> x:*] ==> x:*]]
31	8, 24, 14, 30	oveq2 101	. . . . 5 |- [q:* = B] |= [[[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]]]
32	25, 31	leq 91	. . . 4 |- [q:* = B] |= [\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = \x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]]]
33	7, 26, 32	ceq2 90	. . 3 |- [q:* = B] |= [(A.\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]) = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
34	17, 2, 3, 23, 33	ovl 117	. 2 |- T. |= [[A\p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
35	4, 6, 34	eqtri 95	1 |- T. |= [[A \/ B] = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]

Syntax hints:  tv 1   -> ht 2  *hb 3  kc 5  \kl 6   = ke 7  T.kt 8  [kbr 9   |= wffMMJ2 11  wffMMJ2t 12   ==> tim 121  A.tal 122   \/ tor 124

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

This theorem depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129  df-or 132

This theorem is referenced by:  ecase  163  olc  164  orc  165