---

Step * of Lemma es-interface-val-disjoint

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[Xs:EClass(A) List].
  ∀[X:EClass(A)]. ∀[e:E]. first-eclass(Xs)(e) = X(e) ∈ A supposing ↑e ∈b X supposing (X ∈ Xs) 
  supposing (∀X∈Xs.(∀Y∈Xs.(X = Y ∈ EClass(A)) ∨ X ⋂ Y = 0))
BY
{ (Auto
   THEN (Assert ↑e ∈b first-eclass(Xs) BY
               (BLemma `in-first-eclass` THEN Auto THEN BLemma `l_exists_iff` THEN Auto THEN With ⌜X⌝ (D 0)⋅ THEN Auto))
   THEN RWW "l_all_iff" 5
   THEN Auto) }

1
1. Info : Type
2. es : EO+(Info)
3. A : Type
4. Xs : EClass(A) List
5. ∀X:EClass(A). ((X ∈ Xs) ⇒ (∀Y:EClass(A). ((Y ∈ Xs) ⇒ ((X = Y ∈ EClass(A)) ∨ X ⋂ Y = 0))))
6. X : EClass(A)
7. (X ∈ Xs)
8. e : E
9. ↑e ∈b X
10. ↑e ∈b first-eclass(Xs)
⊢ first-eclass(Xs)(e) = X(e) ∈ A

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[Xs:EClass(A)  List].
    \mforall{}[X:EClass(A)].  \mforall{}[e:E].  first-eclass(Xs)(e)  =  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X  supposing  (X  \mmember{}  Xs) 
    supposing  (\mforall{}X\mmember{}Xs.(\mforall{}Y\mmember{}Xs.(X  =  Y)  \mvee{}  X  \mcap{}  Y  =  0))


By

---

Latex:
(Auto
  THEN  (Assert  \muparrow{}e  \mmember{}\msubb{}  first-eclass(Xs)  BY
                          (BLemma  `in-first-eclass`
                            THEN  Auto
                            THEN  BLemma  `l\_exists\_iff`
                            THEN  Auto
                            THEN  With  \mkleeneopen{}X\mkleeneclose{}  (D  0)\mcdot{}
                            THEN  Auto))
  THEN  RWW  "l\_all\_iff"  5
  THEN  Auto)

---

Home Index