---

Step * of Lemma bag-member-map3

∀[T,U:Type].  ∀x:U. ∀bs:bag(T). ∀f:{v:T| v ↓∈ bs}  ⟶ U.  uiff(x ↓∈ bag-map(f;bs);↓∃v:T. (v ↓∈ bs ∧ (x = (f v) ∈ U)))
BY
{ (Intros
   THEN (Assert x ↓∈ bag-map(f;bs) ∈ ℙ BY
               ((MemCD THEN Try (Complete (Auto))) THEN BLemma `bag-map-member-wf` THEN Auto))
   THEN (InstLemma `bag-member-map` [⌜{v:T| v ↓∈ bs} ⌝;⌜U⌝;⌜x⌝;⌜f⌝;⌜bs⌝]⋅
         THENA (Auto THEN BLemma `bag-subtype` THEN Auto)
         )
   THEN (HypSubst' (-1) 0 THENA Auto)
   THEN D 0
   THEN (UnivCD THENA (Auto THEN BLemma `bag-subtype` THEN Auto))
   THEN SquashExRepD
   THEN Try (DVarSets)
   THEN D 0
   THEN InstConcl [⌜v⌝]⋅
   THEN Auto
   THEN Try ((BLemma `bag-subtype` THEN Auto))
   THEN RWO "bag-subtype2<" 0
   THEN Auto
   THEN BLemma `bag-subtype`
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Intros
  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  (InstLemma  `bag-member-map`  [\mkleeneopen{}\{v:T|  v  \mdownarrow{}\mmember{}  bs\}  \mkleeneclose{};\mkleeneopen{}U\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}bs\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  BLemma  `bag-subtype`  THEN  Auto)
              )
  THEN  (HypSubst'  (-1)  0  THENA  Auto)
  THEN  D  0
  THEN  (UnivCD  THENA  (Auto  THEN  BLemma  `bag-subtype`  THEN  Auto))
  THEN  SquashExRepD
  THEN  Try  (DVarSets)
  THEN  D  0
  THEN  InstConcl  [\mkleeneopen{}v\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Try  ((BLemma  `bag-subtype`  THEN  Auto))
  THEN  RWO  "bag-subtype2<"  0
  THEN  Auto
  THEN  BLemma  `bag-subtype`
  THEN  Auto)

---

Home Index