---

Step * 1 1 2 2 of Lemma bag-member-map


1. T : Type
2. U : Type
3. x : U
4. f : T ⟶ U
5. u : T
6. v : T List
7. x ↓∈ bag-map(f;v) ⇒ (↓∃v@0:T. (v@0 ↓∈ v ∧ (x = (f v@0) ∈ U)))
8. x ↓∈ bag-map(f;v)
⊢ ↓∃v@0:T. (v@0 ↓∈ [u / v] ∧ (x = (f v@0) ∈ U))
BY
{ ((D (-2) THENA Trivial) THEN RepeatFor 2 (ParallelLast) THEN Auto THEN BagMemberD 0⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  T  :  Type
2.  U  :  Type
3.  x  :  U
4.  f  :  T  {}\mrightarrow{}  U
5.  u  :  T
6.  v  :  T  List
7.  x  \mdownarrow{}\mmember{}  bag-map(f;v)  {}\mRightarrow{}  (\mdownarrow{}\mexists{}v@0:T.  (v@0  \mdownarrow{}\mmember{}  v  \mwedge{}  (x  =  (f  v@0))))
8.  x  \mdownarrow{}\mmember{}  bag-map(f;v)
\mvdash{}  \mdownarrow{}\mexists{}v@0:T.  (v@0  \mdownarrow{}\mmember{}  [u  /  v]  \mwedge{}  (x  =  (f  v@0)))


By

---

Latex:
((D  (-2)  THENA  Trivial)  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto  THEN  BagMemberD  0\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index