---

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 3 (ParallelLast) THEN Try (RepeatFor 3 (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