---

Step * 2 of Lemma bag-combine-null


1. A : Type
2. B : Type
3. f : A ⟶ bag(B)
4. b : bag(A)
5. ∀x:A. (x ↓∈ b ⇒ (↑bag-null(f[x])))
⊢ ⋃x∈b.f[x] = {} ∈ bag(B)
BY
{ (RWO "empty-bag-iff-no-member" 0
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN BagMemberD (-1)
   THEN SquashExRepD
   THEN (InstHyp [⌜x1⌝] (-5)⋅ THENA Auto)
   THEN (RWO "assert-bag-null" (-1) THENA Auto)
   THEN (RWO "-1" (-2) THENA Auto)
   THEN BagMemberD (-2)) }

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  Type
3.  f  :  A  {}\mrightarrow{}  bag(B)
4.  b  :  bag(A)
5.  \mforall{}x:A.  (x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (\muparrow{}bag-null(f[x])))
\mvdash{}  \mcup{}x\mmember{}b.f[x]  =  \{\}


By

---

Latex:
(RWO  "empty-bag-iff-no-member"  0
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  BagMemberD  (-1)
  THEN  SquashExRepD
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (RWO  "assert-bag-null"  (-1)  THENA  Auto)
  THEN  (RWO  "-1"  (-2)  THENA  Auto)
  THEN  BagMemberD  (-2))

---

Home Index