---

Step * 2 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. ↓∃f:A ─→ B. ((b = (f a) ∈ B) ∧ f ∈ X(e))
⊢ b ∈ X(a)(e)
BY
{ (RepUR ``class-ap-val classrel class-ap`` 0
   THEN BagMemberD  0
   THEN Fold `classrel` 0
   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.  \mdownarrow{}\mexists{}f:A  {}\mrightarrow{}  B.  ((b  =  (f  a))  \mwedge{}  f  \mmember{}  X(e))
\mvdash{}  b  \mmember{}  X(a)(e)


By

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

---

Home Index