---

Step * 3 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)))))
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
BY
{ (BackThruSomeHyp 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)))))
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)]
⊢ ↑P1[X1(e)]

---

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)])))))
12.  es  :  EO+(Info)@i'
13.  e  :  E@i
14.  \muparrow{}e  \mmember{}\msubb{}  (f1[v]  where  v  from  X1  such  that  P1[v])@i
15.  \muparrow{}e  \mmember{}\msubb{}  X2
16.  \muparrow{}P2[X2(e)]
\mvdash{}  f1[X1(e)]  =  f2[X2(e)]


By

(BackThruSomeHyp  THEN  Auto)

---

Home Index