---

Step * 1 of Lemma member-product-map


1. [A] : Type
2. [B] : Type
3. [C] : Type
4. F : A ⟶ B ⟶ C
5. u : A
6. v : A List
7. ∀bs:B List. ∀c:C.
     ((c ∈ concat(map(λa.map(λb.(F a b);bs);v))) ⇐⇒ ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
8. bs : B List
9. c : C
10. (∃y:B. ((y ∈ bs) ∧ (c = ((λb.(F u b)) y) ∈ C))) ∨ (c ∈ concat(map(λa.map(λb.(F a b);bs);v)))
⊢ ∃a:A. (((a = u ∈ A) ∨ (a ∈ v)) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C))))
BY
{ ((RWW "7" (-1) THENM D -1) THENA Auto)⋅ }

1
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. F : A ⟶ B ⟶ C
5. u : A
6. v : A List
7. ∀bs:B List. ∀c:C.
     ((c ∈ concat(map(λa.map(λb.(F a b);bs);v))) ⇐⇒ ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
8. bs : B List
9. c : C
10. ∃y:B. ((y ∈ bs) ∧ (c = ((λb.(F u b)) y) ∈ C))
⊢ ∃a:A. (((a = u ∈ A) ∨ (a ∈ v)) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C))))

2
1. [A] : Type
2. [B] : Type
3. [C] : Type
4. F : A ⟶ B ⟶ C
5. u : A
6. v : A List
7. ∀bs:B List. ∀c:C.
     ((c ∈ concat(map(λa.map(λb.(F a b);bs);v))) ⇐⇒ ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
8. bs : B List
9. c : C
10. ∃a:A. ((a ∈ v) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C))))
⊢ ∃a:A. (((a = u ∈ A) ∨ (a ∈ v)) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C))))

---

Latex:

---

Latex:

1.  [A]  :  Type
2.  [B]  :  Type
3.  [C]  :  Type
4.  F  :  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C
5.  u  :  A
6.  v  :  A  List
7.  \mforall{}bs:B  List.  \mforall{}c:C.
          ((c  \mmember{}  concat(map(\mlambda{}a.map(\mlambda{}b.(F  a  b);bs);v)))
          \mLeftarrow{}{}\mRightarrow{}  \mexists{}a:A.  ((a  \mmember{}  v)  \mwedge{}  (\mexists{}b:B.  ((b  \mmember{}  bs)  \mwedge{}  (c  =  (F  a  b))))))
8.  bs  :  B  List
9.  c  :  C
10.  (\mexists{}y:B.  ((y  \mmember{}  bs)  \mwedge{}  (c  =  ((\mlambda{}b.(F  u  b))  y))))  \mvee{}  (c  \mmember{}  concat(map(\mlambda{}a.map(\mlambda{}b.(F  a  b);bs);v)))
\mvdash{}  \mexists{}a:A.  (((a  =  u)  \mvee{}  (a  \mmember{}  v))  \mwedge{}  (\mexists{}b:B.  ((b  \mmember{}  bs)  \mwedge{}  (c  =  (F  a  b)))))


By

---

Latex:
((RWW  "7"  (-1)  THENM  D  -1)  THENA  Auto)\mcdot{}

---

Home Index