HOLE Home Higher-Order Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HOLE Home  >  Th. List  >  df-or GIF version

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
StepHypRef 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
83, 4tv 1 . . . . . . . . 9 term p:∗
93, 7tv 1 . . . . . . . . 9 term x:∗
10 tim 121 . . . . . . . . 9 term
118, 9, 10kbr 9 . . . . . . . 8 term [p:∗ ⇒ x:∗]
123, 5tv 1 . . . . . . . . . 10 term q:∗
1312, 9, 10kbr 9 . . . . . . . . 9 term [q:∗ ⇒ x:∗]
1413, 9, 10kbr 9 . . . . . . . 8 term [[q:∗ ⇒ x:∗] ⇒ x:∗]
1511, 14, 10kbr 9 . . . . . . 7 term [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]
163, 7, 15kl 6 . . . . . 6 term λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]]
176, 16kc 5 . . . . 5 term (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
183, 5, 17kl 6 . . . 4 term λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
193, 4, 18kl 6 . . 3 term λp:∗ λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])
20 ke 7 . . 3 term =
212, 19, 20kbr 9 . 2 term [ = λp:∗ λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
221, 21wffMMJ2 11 1 wff ⊤⊧[ = λp:∗ λq:∗ (λx:∗ [[p:∗ ⇒ x:∗] ⇒ [[q:∗ ⇒ x:∗] ⇒ x:∗]])]
Colors of variables: type var term
This definition is referenced by:  wor  140  orval  147
  Copyright terms: Public domain W3C validator