---

Step * 1 1 1 1 of Lemma bag-member-map3-deq


1. T : Type
2. U : Type
3. x : U
4. bs : bag(T)
5. f : {v:T| v ↓∈ bs}  ⟶ U
6. Inj({v:T| v ↓∈ bs} ;U;f)
7. g : ∀x,y:U.  Dec(x = y ∈ U)
8. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
9. single-valued-bag([v∈bs|dec2bool(g x (f v))];T)
10. 0 < #([v∈bs|dec2bool(g x (f v))])
11. [x@0∈bs|dec2bool(g x (f x@0))] ∈ bag({x@0:{b:T| b ↓∈ bs} | ↑dec2bool(g x (f x@0))} )
12. x ↓∈ bag-map(f;bs)
13. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ sv-bag-only([v∈bs|dec2bool(g x (f v))]) ↓∈ bs
BY
{ ((InstLemma `bag-member-sv-bag-only` [⌜T⌝;⌜[v∈bs|dec2bool(g x (f v))]⌝]⋅ THENA Auto)⋅
   THEN RWO "bag-member-filter2" (-1)⋅
   THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  bs  :  bag(T)
5.  f  :  \{v:T|  v  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  U
6.  Inj(\{v:T|  v  \mdownarrow{}\mmember{}  bs\}  ;U;f)
7.  g  :  \mforall{}x,y:U.    Dec(x  =  y)
8.  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))
9.  single-valued-bag([v\mmember{}bs|dec2bool(g  x  (f  v))];T)
10.  0  <  \#([v\mmember{}bs|dec2bool(g  x  (f  v))])
11.  [x@0\mmember{}bs|dec2bool(g  x  (f  x@0))]  \mmember{}  bag(\{x@0:\{b:T|  b  \mdownarrow{}\mmember{}  bs\}  |  \muparrow{}dec2bool(g  x  (f  x@0))\}  )
12.  x  \mdownarrow{}\mmember{}  bag-map(f;bs)
13.  \mdownarrow{}\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))
\mvdash{}  sv-bag-only([v\mmember{}bs|dec2bool(g  x  (f  v))])  \mdownarrow{}\mmember{}  bs


By

---

Latex:
((InstLemma  `bag-member-sv-bag-only`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}[v\mmember{}bs|dec2bool(g  x  (f  v))]\mkleeneclose{}]\mcdot{}  THENA  Auto)\mcdot{}
  THEN  RWO  "bag-member-filter2"  (-1)\mcdot{}
  THEN  Auto)\mcdot{}

---

Home Index