---

Step * of Lemma single-valued-bag-combine

∀[A,B:Type]. ∀[as:bag(A)]. ∀[f:A ⟶ bag(B)].
  (single-valued-bag(⋃x∈as.f[x];B)) supposing ((∀a:A. single-valued-bag(f[a];B)) and single-valued-bag(as;A))
BY
{ (Auto
   THEN D 0
   THEN Auto
   THEN BagMemberD (-2)
   THEN BagMemberD (-1)
   THEN SquashExRepD
   THEN Unfold `single-valued-bag` (-10)
   THEN (InstHyp [⌜x2⌝;⌜x1⌝] (-10)⋅ THENA Auto)
   THEN (InstHyp [⌜x1⌝] (-10)⋅ THENA Auto)
   THEN Unfold `single-valued-bag` (-1)
   THEN InstHyp [⌜x⌝;⌜y⌝] (-1)⋅
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[as:bag(A)].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].
    (single-valued-bag(\mcup{}x\mmember{}as.f[x];B))  supposing 
          ((\mforall{}a:A.  single-valued-bag(f[a];B))  and 
          single-valued-bag(as;A))


By

---

Latex:
(Auto
  THEN  D  0
  THEN  Auto
  THEN  BagMemberD  (-2)
  THEN  BagMemberD  (-1)
  THEN  SquashExRepD
  THEN  Unfold  `single-valued-bag`  (-10)
  THEN  (InstHyp  [\mkleeneopen{}x2\mkleeneclose{};\mkleeneopen{}x1\mkleeneclose{}]  (-10)\mcdot{}  THENA  Auto)
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-10)\mcdot{}  THENA  Auto)
  THEN  Unfold  `single-valued-bag`  (-1)
  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index