---

Step * 1 of Lemma mapfilter-class_functionality


1. Info : Type
2. A1 : Type
3. A2 : Type
4. B : Type
5. P1 : A1 ─→ 𝔹
6. P2 : A2 ─→ 𝔹
7. f1 : A1 ─→ B
8. f2 : A2 ─→ B
9. X1 : EClass(A1)
10. X2 : EClass(A2)
11. ∀es:EO+(Info). ∀e:E.
      ((↑e ∈b X1 ⇐⇒ ↑e ∈b X2)
      ∧ ((↑e ∈b X1)
        ⇒ (↑e ∈b X2)
        ⇒ ((↑P1[X1(e)] ⇐⇒ ↑P2[X2(e)]) ∧ ((↑P1[X1(e)]) ⇒ (↑P2[X2(e)]) ⇒ (f1[X1(e)] = f2[X2(e)] ∈ B)))))
⊢ Singlevalued((f2[v] where v from X2 such that P2[v]))
BY
{ (ProveSV THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  A1  :  Type
3.  A2  :  Type
4.  B  :  Type
5.  P1  :  A1  {}\mrightarrow{}  \mBbbB{}
6.  P2  :  A2  {}\mrightarrow{}  \mBbbB{}
7.  f1  :  A1  {}\mrightarrow{}  B
8.  f2  :  A2  {}\mrightarrow{}  B
9.  X1  :  EClass(A1)
10.  X2  :  EClass(A2)
11.  \mforall{}es:EO+(Info).  \mforall{}e:E.
            ((\muparrow{}e  \mmember{}\msubb{}  X1  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  X2)
            \mwedge{}  ((\muparrow{}e  \mmember{}\msubb{}  X1)
                {}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  X2)
                {}\mRightarrow{}  ((\muparrow{}P1[X1(e)]  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}P2[X2(e)])
                      \mwedge{}  ((\muparrow{}P1[X1(e)])  {}\mRightarrow{}  (\muparrow{}P2[X2(e)])  {}\mRightarrow{}  (f1[X1(e)]  =  f2[X2(e)])))))
\mvdash{}  Singlevalued((f2[v]  where  v  from  X2  such  that  P2[v]))


By

(ProveSV  THEN  Auto)\mcdot{}

---

Home Index