Step * 1 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. T
8. T
9. x
10. R1 y
⊢ y
BY
(InstHyp [x;y] 5⋅ 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  R1  y
\mvdash{}  P  y


By


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




Home Index