---

Step * of Lemma es-interface-extensionality

∀[Info,A:Type]. ∀[X,Y:EClass(A)].
  (X = Y ∈ EClass(A)) supposing 
     ((∀es:EO+(Info). ∀e:E.  ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ (X(e) = Y(e) ∈ A))) and 
     (∀es:EO+(Info). ∀e:E.  (↑e ∈b X ⇐⇒ ↑e ∈b Y)) and 
     Singlevalued(X) and 
     Singlevalued(Y))
BY
{ (Auto
   THEN Auto
   THEN All (Unfold `eclass`)
   THEN Ext
   THEN Auto
   THEN RenameVar `es' (-1)
   THEN Ext
   THEN Auto
   THEN RenameVar `e' (-1)) }

1
1. Info : Type
2. A : Type
3. X : es:EO+(Info) ─→ e:E ─→ bag(A)
4. Y : es:EO+(Info) ─→ e:E ─→ bag(A)
5. Singlevalued(Y)
6. Singlevalued(X)
7. ∀es:EO+(Info). ∀e:E.  (↑e ∈b X ⇐⇒ ↑e ∈b Y)
8. ∀es:EO+(Info). ∀e:E.  ((↑e ∈b X) ⇒ (↑e ∈b Y) ⇒ (X(e) = Y(e) ∈ A))
9. es : EO+(Info)
10. e : E
⊢ (X es e) = (Y es e) ∈ bag(A)

---

Latex:


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


By

(Auto
  THEN  Auto
  THEN  All  (Unfold  `eclass`)
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `es'  (-1)
  THEN  Ext
  THEN  Auto
  THEN  RenameVar  `e'  (-1))

---

Home Index