---

Step * 1 of Lemma monot_shift


1. [A] : Type
2. [B] : Type
3. [R] : A ⟶ A ⟶ ℙ
4. [S] : B ⟶ B ⟶ ℙ
5. opa : A ⟶ A@i
6. opb : B ⟶ B@i
7. f : A ⟶ B@i
8. ∀[a:A]. ((f (opa a)) = (opb (f a)) ∈ B)
9. ∀x,y:A.  (R x y ⇐⇒ S (f x) (f y))@i
10. ∀x,y:B.  ((S x y) ⇒ (S (opb x) (opb y)))@i
11. x : A@i
12. y : A@i
13. R x y@i
⊢ R (opa x) (opa y)
BY
{ ((RWW "8 9" 0 THENM HypBackchain) THENA Auto) }

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [R]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
4.  [S]  :  B  {}\mrightarrow{}  B  {}\mrightarrow{}  \mBbbP{}
5.  opa  :  A  {}\mrightarrow{}  A@i
6.  opb  :  B  {}\mrightarrow{}  B@i
7.  f  :  A  {}\mrightarrow{}  B@i
8.  \mforall{}[a:A].  ((f  (opa  a))  =  (opb  (f  a)))
9.  \mforall{}x,y:A.    (R  x  y  \mLeftarrow{}{}\mRightarrow{}  S  (f  x)  (f  y))@i
10.  \mforall{}x,y:B.    ((S  x  y)  {}\mRightarrow{}  (S  (opb  x)  (opb  y)))@i
11.  x  :  A@i
12.  y  :  A@i
13.  R  x  y@i
\mvdash{}  R  (opa  x)  (opa  y)


By

---

Latex:
((RWW  "8  9"  0  THENM  HypBackchain)  THENA  Auto)

---

Home Index