---

Step * of Lemma bag-combine-is-single-if

∀[A,B:Type]. ∀[f:A ⟶ bag(B)]. ∀[bs:bag(A)]. ∀[x:B].
  ⋃x∈bs.f[x] = {x} ∈ bag(B) supposing ↓∃y:A. ((bs = {y} ∈ bag(A)) ∧ (f[y] = {x} ∈ bag(B)))
BY
{ ((UnivCD THENA Auto)
   THEN SquashExRepD
   THEN (HypSubst' (-2) 0 THENA Auto)
   THEN RWO "bag-combine-single-left" 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A,B:Type].  \mforall{}[f:A  {}\mrightarrow{}  bag(B)].  \mforall{}[bs:bag(A)].  \mforall{}[x:B].
    \mcup{}x\mmember{}bs.f[x]  =  \{x\}  supposing  \mdownarrow{}\mexists{}y:A.  ((bs  =  \{y\})  \mwedge{}  (f[y]  =  \{x\}))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SquashExRepD
  THEN  (HypSubst'  (-2)  0  THENA  Auto)
  THEN  RWO  "bag-combine-single-left"  0
  THEN  Auto)

---

Home Index