---

Step * 1 of Lemma cond_rel_equivalent


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
BY
{ (InstHyp [⌈x⌉;⌈y⌉] (-6)⋅ THEN 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
14. ((R x y) ∨ (x = y ∈ T)) ∨ (R y x)
⊢ R x y

---

Latex:



1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  [Q]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
4.  [P]  :  T  {}\mrightarrow{}  \mBbbP{}
5.  Trans(T;x,y.Q  x  y)@i
6.  \mforall{}x,y:T.    ((Q  x  y)  {}\mRightarrow{}  (\mneg{}(Q  y  x)))
7.  R  =>  Q@i
8.  \mforall{}x,y:T.    (((P  x)  \mwedge{}  (P  y))  {}\mRightarrow{}  (((R  x  y)  \mvee{}  (x  =  y))  \mvee{}  (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
\mvdash{}  R  x  y


By

(InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-6)\mcdot{}  THEN  Auto)

---

Home Index