---

Step * of Lemma mapfilter-class_functionality

∀[Info,A1,A2,B:Type]. ∀[P1:A1 ─→ 𝔹]. ∀[P2:A2 ─→ 𝔹]. ∀[f1:A1 ─→ B]. ∀[f2:A2 ─→ B]. ∀[X1:EClass(A1)]. ∀[X2:EClass(A2)].
  (f1[v] where v from X1 such that P1[v]) = (f2[v] where v from X2 such that P2[v]) ∈ EClass(B) 
  supposing ∀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)))))
BY
{ (Auto
   THEN BLemma `es-interface-extensionality`
   THEN Auto
   THEN Try (((RWO "is-mapfilter-class" (-1) THENM RWW "is-mapfilter-class" 0)
              THEN Auto
              THEN (RWO "mapfilter-class-val" 0 THEN Auto)⋅
              THEN (RWW "is-mapfilter-class" 0 THEN Auto THEN Auto)⋅))⋅) }

1
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]))

2
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((f1[v] where v from X1 such that P1[v]))

3
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)))))
12. es : EO+(Info)@i'
13. e : E@i
14. ↑e ∈b (f1[v] where v from X1 such that P1[v])@i
15. ↑e ∈b X2
16. ↑P2[X2(e)]
⊢ f1[X1(e)] = f2[X2(e)] ∈ B

---

Latex:


\mforall{}[Info,A1,A2,B:Type].  \mforall{}[P1:A1  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[P2:A2  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f1:A1  {}\mrightarrow{}  B].  \mforall{}[f2:A2  {}\mrightarrow{}  B].  \mforall{}[X1:EClass(A1)].
\mforall{}[X2:EClass(A2)].
    (f1[v]  where  v  from  X1  such  that  P1[v])  =  (f2[v]  where  v  from  X2  such  that  P2[v]) 
    supposing  \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)])))))


By

(Auto
  THEN  BLemma  `es-interface-extensionality`
  THEN  Auto
  THEN  Try  (((RWO  "is-mapfilter-class"  (-1)  THENM  RWW  "is-mapfilter-class"  0)
                        THEN  Auto
                        THEN  (RWO  "mapfilter-class-val"  0  THEN  Auto)\mcdot{}
                        THEN  (RWW  "is-mapfilter-class"  0  THEN  Auto  THEN  Auto)\mcdot{}))\mcdot{})

---

Home Index