---

Step * 2 1 of Lemma member-mapl


1. [T] : Type
2. [T'] : Type
3. u : T
4. v : T List
5. ∀y:T'. ∀f:{x:T| (x ∈ v)}  ⟶ T'.  ((y ∈ mapl(f;v)) ⇐⇒ ∃a:T. ((a ∈ v) ∧ (y = (f a) ∈ T')))
⊢ ∀y:T'. ∀f:{x:T| (x ∈ [u / v])}  ⟶ T'.  ((y ∈ [f u / mapl(f;v)]) ⇐⇒ ∃a:T. ((a ∈ [u / v]) ∧ (y = (f a) ∈ T')))
BY
{ (Auto THEN ExRepD) }

1
1. [T] : Type
2. [T'] : Type
3. u : T
4. v : T List
5. ∀y:T'. ∀f:{x:T| (x ∈ v)}  ⟶ T'.  ((y ∈ mapl(f;v)) ⇐⇒ ∃a:T. ((a ∈ v) ∧ (y = (f a) ∈ T')))
6. y : T'
7. f : {x:T| (x ∈ [u / v])}  ⟶ T'
8. (y ∈ [f u / mapl(f;v)])
⊢ ∃a:T. ((a ∈ [u / v]) ∧ (y = (f a) ∈ T'))

2
1. [T] : Type
2. [T'] : Type
3. u : T
4. v : T List
5. ∀y:T'. ∀f:{x:T| (x ∈ v)}  ⟶ T'.  ((y ∈ mapl(f;v)) ⇐⇒ ∃a:T. ((a ∈ v) ∧ (y = (f a) ∈ T')))
6. y : T'
7. f : {x:T| (x ∈ [u / v])}  ⟶ T'
8. a : T
9. (a ∈ [u / v])
10. y = (f a) ∈ T'
⊢ (y ∈ [f u / mapl(f;v)])

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [T']  :  Type
3.  u  :  T
4.  v  :  T  List
5.  \mforall{}y:T'.  \mforall{}f:\{x:T|  (x  \mmember{}  v)\}    {}\mrightarrow{}  T'.    ((y  \mmember{}  mapl(f;v))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:T.  ((a  \mmember{}  v)  \mwedge{}  (y  =  (f  a))))
\mvdash{}  \mforall{}y:T'.  \mforall{}f:\{x:T|  (x  \mmember{}  [u  /  v])\}    {}\mrightarrow{}  T'.
        ((y  \mmember{}  [f  u  /  mapl(f;v)])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:T.  ((a  \mmember{}  [u  /  v])  \mwedge{}  (y  =  (f  a))))


By

---

Latex:
(Auto  THEN  ExRepD)

---

Home Index