Step * of Lemma weak-antecedent-surjection_functionality_wrt_pred_equiv

es:EO
  ∀[P1,P2,Q1,Q2:E ⟶ ℙ].  ∀f:{e:E| P1 e}  ⟶ {e:E| Q1 e} (P1 ⇐⇒ P2  Q1 ⇐⇒ Q2  (Q1 ←←f== P1 ⇐⇒ Q2 ←←f== P2))
BY
(Unfold `predicate_equivalent` 0
   THEN Auto
   THEN Try (Complete (Auto))
   THEN Try ((RepeatFor (ParallelLast) THEN Try (RepeatFor (ParallelLast))))
   THEN ParallelLast⋅
   THEN Auto⋅}


Latex:


Latex:
\mforall{}es:EO
    \mforall{}[P1,P2,Q1,Q2:E  {}\mrightarrow{}  \mBbbP{}].
        \mforall{}f:\{e:E|  P1  e\}    {}\mrightarrow{}  \{e:E|  Q1  e\}  .  (P1  \mLeftarrow{}{}\mRightarrow{}  P2  {}\mRightarrow{}  Q1  \mLeftarrow{}{}\mRightarrow{}  Q2  {}\mRightarrow{}  (Q1  \mleftarrow{}\mleftarrow{}=  f==  P1  \mLeftarrow{}{}\mRightarrow{}  Q2  \mleftarrow{}\mleftarrow{}=  f==  P2))


By


Latex:
(Unfold  `predicate\_equivalent`  0
  THEN  Auto
  THEN  Try  (Complete  (Auto))
  THEN  Try  ((RepeatFor  3  (ParallelLast)  THEN  Try  (RepeatFor  3  (ParallelLast))))
  THEN  ParallelLast\mcdot{}
  THEN  Auto\mcdot{})




Home Index