---

Step * 1 of Lemma disjoint-union-class-single-val


1. Info : Type
2. A : Type
3. B : Type
4. es : EO+(Info)
5. X : EClass(A)
6. Y : EClass(B)
7. ∀e:E. ∀v1,v2:B.  (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))@i
8. e : E@i
9. ∀v1,v2:B.  (v1 ∈ Y(e) ⇒ v2 ∈ Y(e) ⇒ (v1 = v2 ∈ B))
10. ∀v1,v2:A.  (v1 ∈ X(e) ⇒ v2 ∈ X(e) ⇒ (v1 = v2 ∈ A))@i
11. x : A@i
12. y : B@i
13. x ∈ X(e)
14. y ∈ Y(e)
15. ∀w:A. (¬w ∈ X(e))
⊢ (inl x) = (inr y ) ∈ (A + B)
BY
{ (With ⌈x⌉ (D (-1))⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  es  :  EO+(Info)
5.  X  :  EClass(A)
6.  Y  :  EClass(B)
7.  \mforall{}e:E.  \mforall{}v1,v2:B.    (v1  \mmember{}  Y(e)  {}\mRightarrow{}  v2  \mmember{}  Y(e)  {}\mRightarrow{}  (v1  =  v2))@i
8.  e  :  E@i
9.  \mforall{}v1,v2:B.    (v1  \mmember{}  Y(e)  {}\mRightarrow{}  v2  \mmember{}  Y(e)  {}\mRightarrow{}  (v1  =  v2))
10.  \mforall{}v1,v2:A.    (v1  \mmember{}  X(e)  {}\mRightarrow{}  v2  \mmember{}  X(e)  {}\mRightarrow{}  (v1  =  v2))@i
11.  x  :  A@i
12.  y  :  B@i
13.  x  \mmember{}  X(e)
14.  y  \mmember{}  Y(e)
15.  \mforall{}w:A.  (\mneg{}w  \mmember{}  X(e))
\mvdash{}  (inl  x)  =  (inr  y  )


By

---

Latex:
(With  \mkleeneopen{}x\mkleeneclose{}  (D  (-1))\mcdot{}  THEN  Auto)

---

Home Index