---

Step * of Lemma disjoint-union-comb-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(A)]. ∀[Y:EClass(B)].
  (single-valued-classrel(es;X (+) Y;A + B)) supposing 
     (disjoint-classrel(es;A;X;B;Y) and 
     single-valued-classrel(es;Y;B) and 
     single-valued-classrel(es;X;A))
BY
{ ((UnivCD THENA MaAuto)
   THEN Unfold `disjoint-union-comb` 0
   THEN SingleValThm
   THEN RepeatFor 2 (((BLemma `simple-comb-1-disjoint-classrel` THENA Auto)
                      THEN (BLemma `disjoint-classrel-symm` THENA Auto)
                      ))
   THEN Trivial) }

---

Latex:

---

Latex:
\mforall{}[Info,A,B:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].
    (single-valued-classrel(es;X  (+)  Y;A  +  B))  supposing 
          (disjoint-classrel(es;A;X;B;Y)  and 
          single-valued-classrel(es;Y;B)  and 
          single-valued-classrel(es;X;A))


By

---

Latex:
((UnivCD  THENA  MaAuto)
  THEN  Unfold  `disjoint-union-comb`  0
  THEN  SingleValThm
  THEN  RepeatFor  2  (((BLemma  `simple-comb-1-disjoint-classrel`  THENA  Auto)
                                        THEN  (BLemma  `disjoint-classrel-symm`  THENA  Auto)
                                        ))
  THEN  Trivial)

---

Home Index