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