---

Step * of Lemma rel-immediate_functionality_wrt_iff

∀[T:Type]. ∀[R,Q:T ⟶ T ⟶ ℙ].  ((∀x,y:T.  (R x y ⇐⇒ Q x y)) ⇒ (∀x,y:T.  (R! x y ⇐⇒ Q! x y)))
BY
{ (RepUR ``rel-immediate`` 0 THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Q : T ⟶ T ⟶ ℙ
4. ∀x,y:T.  (R x y ⇐⇒ Q x y)@i
5. x : T@i
6. y : T@i
7. R x y@i
8. ∀z:T. (¬((R x z) ∧ (R z y)))@i
9. z : T@i
⊢ ¬((Q x z) ∧ (Q z y))

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. Q : T ⟶ T ⟶ ℙ
4. ∀x,y:T.  (R x y ⇐⇒ Q x y)@i
5. x : T@i
6. y : T@i
7. Q x y@i
8. ∀z:T. (¬((Q x z) ∧ (Q z y)))@i
9. z : T@i
⊢ ¬((R x z) ∧ (R z y))

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R,Q:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].    ((\mforall{}x,y:T.    (R  x  y  \mLeftarrow{}{}\mRightarrow{}  Q  x  y))  {}\mRightarrow{}  (\mforall{}x,y:T.    (R!  x  y  \mLeftarrow{}{}\mRightarrow{}  Q!  x  y)))


By

---

Latex:
(RepUR  ``rel-immediate``  0  THEN  Auto)

---

Home Index