---

Step * of Lemma Q-R-pre-preserving_functionality_wrt_implies

∀es:EO
  ∀[P1,P2:E ⟶ ℙ]. ∀[Q1,R1,Q2,R2:E ⟶ E ⟶ ℙ].
    ∀f:{e:E| P1 e}  ⟶ E
      (P1 ⇐ P2 ⇒ Q1 ⇐ Q2 ⇒ R1 => R2 ⇒ {f is Q1-R1-pre-preserving on P1 ⇒ f is Q2-R2-pre-preserving on P2})
BY
{ (RepUR ``rel_rev_implies predicate_rev_implies guard predicate_implies rel_implies Q-R-pre-preserving infix_ap`` 0
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}es:EO
    \mforall{}[P1,P2:E  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[Q1,R1,Q2,R2:E  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  E
            (P1  \mLeftarrow{}{}  P2
            {}\mRightarrow{}  Q1  \mLeftarrow{}{}  Q2
            {}\mRightarrow{}  R1  =>  R2
            {}\mRightarrow{}  \{f  is  Q1-R1-pre-preserving  on  P1  {}\mRightarrow{}  f  is  Q2-R2-pre-preserving  on  P2\})


By

---

Latex:
(...
  THEN  Auto
  )

---

Home Index