Definition df-or 132

Description: Define the 'or' operator. (Contributed by Mario Carneiro, 8-Oct-2014.)

Assertion

Ref	Expression
df-or	⊢ ⊤⊧[ ∨ = λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]

Distinct variable group:   p,q,x

Detailed syntax breakdown of Definition df-or

Step	Hyp	Ref	Expression
1		kt 8	. 2 term ⊤
2		tor 124	. . 3 term ∨
3		hb 3	. . . 4 type ∗
4		vp	. . . 4 var p
5		vq	. . . . 5 var q
6		tal 122	. . . . . 6 term ∀
7		vx	. . . . . . 7 var x
8	3, 4	tv 1	. . . . . . . . 9 term p:∗
9	3, 7	tv 1	. . . . . . . . 9 term x:∗
10		tim 121	. . . . . . . . 9 term ⇒
11	8, 9, 10	kbr 9	. . . . . . . 8 term [p:∗ ⇒ x:∗]
12	3, 5	tv 1	. . . . . . . . . 10 term q:∗
13	12, 9, 10	kbr 9	. . . . . . . . 9 term [q:∗ ⇒ x:∗]
14	13, 9, 10	kbr 9	. . . . . . . 8 term [[q:∗ ⇒ x:∗] ⇒ x:∗]
15	11, 14, 10	kbr 9	. . . . . . 7 term [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]
16	3, 7, 15	kl 6	. . . . . 6 term λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]
17	6, 16	kc 5	. . . . 5 term (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
18	3, 5, 17	kl 6	. . . 4 term λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
19	3, 4, 18	kl 6	. . 3 term λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
20		ke 7	. . 3 term =
21	2, 19, 20	kbr 9	. 2 term [ ∨ = λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
22	1, 21	wffMMJ2 11	1 wff ⊤⊧[ ∨ = λp:∗ λq:∗ (∀λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]

This definition is referenced by:  wor  140  orval  147