---

Step * 2 1 1 1 1 of Lemma setmem-piset-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))))
7. ∀i:T. (f1 i ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;f1))} )
8. z : coSet{i:l}
9. ∃t:T. seteq(z;(f1 t,set-item(B[f1 t];f t)))
⊢ (z ∈ mk-coset(T;λt@0.(f1 t@0,set-item(B[f1 t@0];f t@0))))
BY
{ (SetMemDef 0 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  f1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  B  :  \{a:coSet\{i:l\}|  (a  \mmember{}  mk-coset(T;f1))\}    {}\mrightarrow{}  coSet\{i:l\}
4.  x  :  coSet\{i:l\}
5.  f  :  t:set-dom(mk-coset(T;f1))  {}\mrightarrow{}  set-dom(B[set-item(mk-coset(T;f1);t)])
6.  \mforall{}z:coSet\{i:l\}
          ((z  \mmember{}  x)
          \mLeftarrow{}{}\mRightarrow{}  \mexists{}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))))
7.  \mforall{}i:T.  (f1  i  \mmember{}  \{a:coSet\{i:l\}|  (a  \mmember{}  mk-coset(T;f1))\}  )
8.  z  :  coSet\{i:l\}
9.  \mexists{}t:T.  seteq(z;(f1  t,set-item(B[f1  t];f  t)))
\mvdash{}  (z  \mmember{}  mk-coset(T;\mlambda{}t@0.(f1  t@0,set-item(B[f1  t@0];f  t@0))))


By

---

Latex:
(SetMemDef  0  THEN  Auto)

---

Home Index