---

Step * of Lemma mapfilter-class-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[P:A ─→ 𝔹]. ∀[f:A ─→ B]. ∀[X:EClass(A)]. ∀[e:E].
  (f[v] where v from X such that P[v])(e) ~ f[X(e)] supposing ↑e ∈b (f[v] where v from X such that P[v])
BY
{ ((UnivCD THENA Auto)
   THEN MoveToConcl (-1)
   THEN (Unfold `eclass` -2
         THEN RepUR ``mapfilter-class es-filter-image in-eclass`` 0
         THEN RepUR ``eclass-val eclass-compose1`` 0
         THEN Repeat (AutoSplit))⋅) }

1
.....wf..... 
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. B : Type
5. P : A ─→ 𝔹
6. f : A ─→ B
7. X : es:EO+(Info) ─→ e:E ─→ bag(A)
8. e : E
9. #(X es e) = 1 ∈ ℤ
⊢ P[only(X es e)] ∈ 𝔹

---

Latex:


\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[f:A  {}\mrightarrow{}  B].  \mforall{}[X:EClass(A)].  \mforall{}[e:E].
    (f[v]  where  v  from  X  such  that  P[v])(e)  \msim{}  f[X(e)] 
    supposing  \muparrow{}e  \mmember{}\msubb{}  (f[v]  where  v  from  X  such  that  P[v])


By

((UnivCD  THENA  Auto)
  THEN  MoveToConcl  (-1)
  THEN  (Unfold  `eclass`  -2
              THEN  RepUR  ``mapfilter-class  es-filter-image  in-eclass``  0
              THEN  RepUR  ``eclass-val  eclass-compose1``  0
              THEN  Repeat  (AutoSplit))\mcdot{})

---

Home Index