---

Step * of Lemma bag-member-map3-deq

∀[T,U:Type].
  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.
    (Inj({v:T| v ↓∈ bs} ;U;f) ⇒ (∀x,y:U.  Dec(x = y ∈ U)) ⇒ uiff(x ↓∈ bag-map(f;bs);∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))\000C)
BY
{ (Intros
   THEN (InstLemma `bag-member-map3` [⌜T⌝;⌜U⌝;⌜x⌝;⌜bs⌝;⌜f⌝]⋅ THENA Auto)
   THEN (Assert x ↓∈ bag-map(f;bs) ∈ ℙ BY
               ((MemCD THEN Try (Complete (Auto))) THEN BLemma `bag-map-member-wf` THEN Auto))
   THEN (HypSubst' (-2) 0 THENA Try (Complete (Auto)))
   THEN D 0
   THEN (UnivCD THENA Auto)
   THEN Try (Complete ((D 0 THEN Auto)))
   THEN Thin (-2)) }

1
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. ∀x,y:U.  Dec(x = y ∈ U)
8. uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
9. ↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))
⊢ ∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U))

---

Latex:

---

Latex:
\mforall{}[T,U:Type].
    \mforall{}x:U.  \mforall{}bs:bag(T).  \mforall{}f:\{v:T|  v  \mdownarrow{}\mmember{}  bs\}    {}\mrightarrow{}  U.
        (Inj(\{v:T|  v  \mdownarrow{}\mmember{}  bs\}  ;U;f)
        {}\mRightarrow{}  (\mforall{}x,y:U.    Dec(x  =  y))
        {}\mRightarrow{}  uiff(x  \mdownarrow{}\mmember{}  bag-map(f;bs);\mexists{}v:T.  (v  \mdownarrow{}\mmember{}  bs  \mwedge{}  (x  =  (f  v)))))


By

---

Latex:
(Intros
  THEN  (InstLemma  `bag-member-map3`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (Assert  x  \mdownarrow{}\mmember{}  bag-map(f;bs)  \mmember{}  \mBbbP{}  BY
                          ((MemCD  THEN  Try  (Complete  (Auto)))  THEN  BLemma  `bag-map-member-wf`  THEN  Auto))
  THEN  (HypSubst'  (-2)  0  THENA  Try  (Complete  (Auto)))
  THEN  D  0
  THEN  (UnivCD  THENA  Auto)
  THEN  Try  (Complete  ((D  0  THEN  Auto)))
  THEN  Thin  (-2))

---

Home Index