---

Step * of Lemma class-ap-val-classrel

∀[Info,A,B:Type]. ∀[X:EClass(A ─→ B)]. ∀[a:A]. ∀[b:B]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(b ∈ X(a)(e);↓∃f:A ─→ B. ((b = (f a) ∈ B) ∧ f ∈ X(e)))
BY
{ Auto }

1
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))

2
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)

---

Latex:


\mforall{}[Info,A,B:Type].  \mforall{}[X:EClass(A  {}\mrightarrow{}  B)].  \mforall{}[a:A].  \mforall{}[b:B].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(b  \mmember{}  X(a)(e);\mdownarrow{}\mexists{}f:A  {}\mrightarrow{}  B.  ((b  =  (f  a))  \mwedge{}  f  \mmember{}  X(e)))


By

Auto

---

Home Index