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  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