Theorem orval 137

Description: Value of the disjunction.

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

Syntax hints:  tv 1   → ht 2  ∗hb 3  kc 5  λkl 6   = ke 7  ⊤kt 8  [kbr 9  ⊧wffMMJ2 11  wffMMJ2t 12   ⇒ tim 111  ∀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