---

Step * of Lemma cond_rel_equivalent

∀[T:Type]. ∀[R,Q:T ─→ T ─→ ℙ]. ∀[P:T ─→ ℙ].
  (Trans(T;x,y.Q x y)
  ⇒ R => Q
     ⇒ (∀x,y:T.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ T)) ∨ (R y x))))
     ⇒ (∀x,y:T.  (((P x) ∧ (P y)) ⇒ (R x y ⇐⇒ Q x y))) 
     supposing ∀x,y:T.  ((Q x y) ⇒ (¬(Q y x))))
BY
{ Auto }

1
1. [T] : Type
2. [R] : T ─→ T ─→ ℙ
3. [Q] : T ─→ T ─→ ℙ
4. [P] : T ─→ ℙ
5. Trans(T;x,y.Q x y)@i
6. ∀x,y:T.  ((Q x y) ⇒ (¬(Q y x)))
7. R => Q@i
8. ∀x,y:T.  (((P x) ∧ (P y)) ⇒ (((R x y) ∨ (x = y ∈ T)) ∨ (R y x)))@i
9. x : T@i
10. y : T@i
11. P x@i
12. P y@i
13. Q x y@i
⊢ R x y

---

Latex:


\mforall{}[T:Type].  \mforall{}[R,Q:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbP{}].
    (Trans(T;x,y.Q  x  y)
    {}\mRightarrow{}  R  =>  Q
          {}\mRightarrow{}  (\mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (R  y  x))))
          {}\mRightarrow{}  (\mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (R  x  y  \mLeftarrow{}{}\mRightarrow{}  Q  x  y))) 
          supposing  \mforall{}x,y:T.    ((Q  x  y)  {}\mRightarrow{}  (\mneg{}(Q  y  x))))


By

Auto

---

Home Index