---

Step * of Lemma sv-classrel

∀[Info,A:Type]. ∀[X:EClass(A)].
  (Singlevalued(X) ⇒ (∀es:EO+(Info). ∀e:E. ∀v:A.  (v ∈ X(e) ⇐⇒ (↑e ∈b X) ∧ (v = X(e) ∈ A))))
BY
{ (UnivCD THENA Auto) }

1
1. Info : Type
2. A : Type
3. X : EClass(A)
4. Singlevalued(X)@i'
5. es : EO+(Info)@i'
6. e : E@i
7. v : A@i
⊢ v ∈ X(e) ⇐⇒ (↑e ∈b X) ∧ (v = X(e) ∈ A)

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[X:EClass(A)].
    (Singlevalued(X)  {}\mRightarrow{}  (\mforall{}es:EO+(Info).  \mforall{}e:E.  \mforall{}v:A.    (v  \mmember{}  X(e)  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}e  \mmember{}\msubb{}  X)  \mwedge{}  (v  =  X(e)))))


By

(UnivCD  THENA  Auto)

---

Home Index