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	⊢ ⊤⊧[[A ∨ B] = (∀λ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 ⊢ ⊤⊧[ ∨ = λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
6	1, 2, 3, 5	oveq 102	. 2 ⊢ ⊤⊧[[A ∨ B] = [Aλp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])B]]
7		wal 134	. . . 4 ⊢ ∀:((∗ → ∗) → ∗)
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 ⊢ (∀λ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]⊧[(∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]) = (∀λ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]⊧[(∀λx:∗ [[A ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]) = (∀λx:∗ [[A ⇒ x:∗] ⇒ [[B ⇒ x:∗] ⇒ x:∗]])]
34	17, 2, 3, 23, 33	ovl 117	. 2 ⊢ ⊤⊧[[Aλp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])B] = (∀λx:∗ [[A ⇒ x:∗] ⇒ [[B ⇒ x:∗] ⇒ x:∗]])]
35	4, 6, 34	eqtri 95	1 ⊢ ⊤⊧[[A ∨ B] = (∀λx:∗ [[A ⇒ x:∗] ⇒ [[B ⇒ x:∗] ⇒ x:∗]])]

This proof depends on syntax axioms:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12   ⇒ tim 121  ∀tal 122   ∨ tor 124

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-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 proof depends on definitions:  df-ov 73  df-al 126  df-an 128  df-im 129  df-or 132

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