---

Step * 2 of Lemma setmem-piset-1


1. A : coSet{i:l}
2. B : {a:coSet{i:l}| (a ∈ A)}  ⟶ coSet{i:l}
3. x : coSet{i:l}
4. f : t:set-dom(A) ⟶ set-dom(B[set-item(A;t)])
5. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃t:set-dom(A). seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f t))))
⊢ (x ∈ piset(A;a.B[a]))
BY
{ ((coSetD 1 THEN D 1) THEN SetMemDef 0 THEN RenameVar `f1' 2 THEN All (Fold `mk-coset`)) }

1
1. T : Type
2. f1 : T ⟶ coSet{i:l}
3. B : {a:coSet{i:l}| (a ∈ mk-coset(T;f1))}  ⟶ coSet{i:l}
4. x : coSet{i:l}
5. f : t:set-dom(mk-coset(T;f1)) ⟶ set-dom(B[set-item(mk-coset(T;f1);t)])
6. ∀z:coSet{i:l}
     ((z ∈ x)
     ⇐⇒ ∃t:set-dom(mk-coset(T;f1)). seteq(z;(set-item(mk-coset(T;f1);t),set-item(B[set-item(mk-coset(T;f1);t)];f t))))
⊢ ∃t:t:T ⟶ set-dom(B[f1 t]). seteq(x;mk-coset(T;λt@0.(f1 t@0,set-item(B[f1 t@0];t t@0))))

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  A)\}    {}\mrightarrow{}  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  t:set-dom(A)  {}\mrightarrow{}  set-dom(B[set-item(A;t)])
5.  \mforall{}z:coSet\{i:l\}
          ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}t:set-dom(A).  seteq(z;(set-item(A;t),set-item(B[set-item(A;t)];f  t))))
\mvdash{}  (x  \mmember{}  piset(A;a.B[a]))


By

---

Latex:
((coSetD  1  THEN  D  1)  THEN  SetMemDef  0  THEN  RenameVar  `f1'  2  THEN  All  (Fold  `mk-coset`))

---

Home Index