---

Step * 2 of Lemma setmem-sigmaset


1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. ∀a1,a2:coSet{i:l}.  ((a1 ∈ A) ⇒ (a2 ∈ A) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
4. x : coSet{i:l}
5. a : coSet{i:l}
6. (a ∈ A)
7. b : coSet{i:l}
8. (b ∈ B[a])
9. seteq(x;(a,b))
⊢ (x ∈ Σa:A.B[a])
BY
{ ((coSetD 1 THEN D 1) THEN SetMemDef 0 THEN RenameVar `f' 2) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. B : {a:coSet{i:l}| (a ∈ <T, f>)}  ⟶ coSet{i:l}
4. ∀a1,a2:coSet{i:l}.  ((a1 ∈ <T, f>) ⇒ (a2 ∈ <T, f>) ⇒ seteq(a1;a2) ⇒ seteq(B[a1];B[a2]))
5. x : coSet{i:l}
6. a : coSet{i:l}
7. (a ∈ <T, f>)
8. b : coSet{i:l}
9. (b ∈ B[a])
10. seteq(x;(a,b))
⊢ ∃t:t:T × set-dom(B[f t]). seteq(x;let t,s = t in (f t,set-item(B[f t];s)))

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  A)  {}\mRightarrow{}  (a2  \mmember{}  A)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  seteq(B[a1];B[a2]))
4.  x  :  coSet\{i:l\}
5.  a  :  coSet\{i:l\}
6.  (a  \mmember{}  A)
7.  b  :  coSet\{i:l\}
8.  (b  \mmember{}  B[a])
9.  seteq(x;(a,b))
\mvdash{}  (x  \mmember{}  \mSigma{}a:A.B[a])


By

---

Latex:
((coSetD  1  THEN  D  1)  THEN  SetMemDef  0  THEN  RenameVar  `f'  2)

---

Home Index