Step * of Lemma preserved_by_or

[T:Type]. ∀[P:T ⟶ ℙ]. ∀[R1,R2:T ⟶ T ⟶ ℙ].  (R1 preserves  R2 preserves  R1 ∨ R2 preserves P)
BY
(Unfolds ``rel_or preserved_by`` THEN Reduce THEN Auto THEN (D (-1))) }

1
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

2
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. R2 y
⊢ y


Latex:


Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[R1,R2:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    (R1  preserves  P  {}\mRightarrow{}  R2  preserves  P  {}\mRightarrow{}  R1  \mvee{}  R2  preserves  P)


By


Latex:
(Unfolds  ``rel\_or  preserved\_by``  0  THEN  Reduce  0  THEN  Auto  THEN  (D  (-1)))




Home Index