---

Step * 2 of Lemma preserved_by_or


1. [T] : Type
2. [P] : T ⟶ ℙ
3. [R1] : T ⟶ T ⟶ ℙ
4. [R2] : T ⟶ T ⟶ ℙ
5. ∀x,y:T.  ((P x) ⇒ (x R1 y) ⇒ (P y))
6. ∀x,y:T.  ((P x) ⇒ (x R2 y) ⇒ (P y))
7. x : T
8. y : T
9. P x
10. x R2 y
⊢ P y
BY
{ (InstHyp [x;y] 6⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
3.  [R1]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  [R2]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
5.  \mforall{}x,y:T.    ((P  x)  {}\mRightarrow{}  (x  R1  y)  {}\mRightarrow{}  (P  y))
6.  \mforall{}x,y:T.    ((P  x)  {}\mRightarrow{}  (x  R2  y)  {}\mRightarrow{}  (P  y))
7.  x  :  T
8.  y  :  T
9.  P  x
10.  x  R2  y
\mvdash{}  P  y


By

---

Latex:
(InstHyp  [x;y]  6\mcdot{}  THEN  Auto)

---

Home Index