---

Step * of Lemma is-mapfilter-class

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

---

Latex:


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


By

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

---

Home Index