---

Step * 1 of Lemma class-ap-val-classrel


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A ─→ B)
5. a : A
6. b : B
7. es : EO+(Info)
8. e : E
9. b ∈ X(a)(e)
⊢ ↓∃f:A ─→ B. ((b = (f a) ∈ B) ∧ f ∈ X(e))
BY
{ (RepUR ``class-ap-val classrel class-ap`` (-1)
   THEN BagMemberD (-1)
   THEN Fold `classrel` (-1)
   THEN RepeatFor 2 (ParallelLast)
   THEN Auto) }

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A  {}\mrightarrow{}  B)
5.  a  :  A
6.  b  :  B
7.  es  :  EO+(Info)
8.  e  :  E
9.  b  \mmember{}  X(a)(e)
\mvdash{}  \mdownarrow{}\mexists{}f:A  {}\mrightarrow{}  B.  ((b  =  (f  a))  \mwedge{}  f  \mmember{}  X(e))


By

(RepUR  ``class-ap-val  classrel  class-ap``  (-1)
  THEN  BagMemberD  (-1)
  THEN  Fold  `classrel`  (-1)
  THEN  RepeatFor  2  (ParallelLast)
  THEN  Auto)

---

Home Index