Theorem orval 137

Description: Value of the disjunction.

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 130	. . 3 |- \/ :(* -> (* -> *))
2		imval.1	. . 3 |- A:*
3		imval.2	. . 3 |- B:*
4	1, 2, 3	wov 64	. 2 |- [A \/ B]:*
5		df-or 122	. . 3 |- T. |= [ \/ = \p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
6	1, 2, 3, 5	oveq 92	. 2 |- T. |= [[A \/ B] = [A\p:* \q:* (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])B]]
7		wal 124	. . . 4 |- A.:((* -> *) -> *)
8		wim 127	. . . . . 6 |- ==> :(* -> (* -> *))
9		wv 58	. . . . . . 7 |- p:*:*
10		wv 58	. . . . . . 7 |- x:*:*
11	8, 9, 10	wov 64	. . . . . 6 |- [p:* ==> x:*]:*
12		wv 58	. . . . . . . 8 |- q:*:*
13	8, 12, 10	wov 64	. . . . . . 7 |- [q:* ==> x:*]:*
14	8, 13, 10	wov 64	. . . . . 6 |- [[q:* ==> x:*] ==> x:*]:*
15	8, 11, 14	wov 64	. . . . 5 |- [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:*
16	15	wl 59	. . . 4 |- \x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:(* -> *)
17	7, 16	wc 45	. . 3 |- (A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]):*
18	9, 2	weqi 68	. . . . . . . 8 |- [p:* = A]:*
19	18	id 25	. . . . . . 7 |- [p:* = A] |= [p:* = A]
20	8, 9, 10, 19	oveq1 89	. . . . . 6 |- [p:* = A] |= [[p:* ==> x:*] = [A ==> x:*]]
21	8, 11, 14, 20	oveq1 89	. . . . 5 |- [p:* = A] |= [[[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]]
22	15, 21	leq 81	. . . 4 |- [p:* = A] |= [\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = \x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]]
23	7, 16, 22	ceq2 80	. . 3 |- [p:* = A] |= [(A.\x:* [[p:* ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]) = (A.\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]])]
24	8, 2, 10	wov 64	. . . . . 6 |- [A ==> x:*]:*
25	8, 24, 14	wov 64	. . . . 5 |- [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:*
26	25	wl 59	. . . 4 |- \x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]:(* -> *)
27	12, 3	weqi 68	. . . . . . . . 9 |- [q:* = B]:*
28	27	id 25	. . . . . . . 8 |- [q:* = B] |= [q:* = B]
29	8, 12, 10, 28	oveq1 89	. . . . . . 7 |- [q:* = B] |= [[q:* ==> x:*] = [B ==> x:*]]
30	8, 13, 10, 29	oveq1 89	. . . . . 6 |- [q:* = B] |= [[[q:* ==> x:*] ==> x:*] = [[B ==> x:*] ==> x:*]]
31	8, 24, 14, 30	oveq2 91	. . . . 5 |- [q:* = B] |= [[[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]]]
32	25, 31	leq 81	. . . 4 |- [q:* = B] |= [\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]] = \x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]]]
33	7, 26, 32	ceq2 80	. . 3 |- [q:* = B] |= [(A.\x:* [[A ==> x:*] ==> [[q:* ==> x:*] ==> x:*]]) = (A.\x:* [[A ==> x:*] ==> [[B ==> x:*] ==> x:*]])]
34	17, 2, 3, 23, 33	ovl 107	. 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 85	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 111  A.tal 112   \/ tor 114

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-ceq 46  ax-beta 60  ax-distrc 61  ax-leq 62  ax-distrl 63  ax-hbl1 93  ax-17 95  ax-inst 103

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

This theorem is referenced by:  ecase  153  olc  154  orc  155