---

Step * 2 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))))
⊢ ∃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))))
BY
{ ((Assert ∀i:T. (f1 i ∈ {a:coSet{i:l}| (a ∈ mk-coset(T;f1))} ) BY Auto) THEN (D 0 With ⌜f⌝  THENW Auto)) }

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))} )
⊢ seteq(x;mk-coset(T;λt@0.(f1 t@0,set-item(B[f1 t@0];f t@0))))

---

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))))
\mvdash{}  \mexists{}t:t:T  {}\mrightarrow{}  set-dom(B[f1  t]).  seteq(x;mk-coset(T;\mlambda{}t@0.(f1  t@0,set-item(B[f1  t@0];t  t@0))))


By

---

Latex:
((Assert  \mforall{}i:T.  (f1  i  \mmember{}  \{a:coSet\{i:l\}|  (a  \mmember{}  mk-coset(T;f1))\}  )  BY  Auto)  THEN  (D  0  With  \mkleeneopen{}f\mkleeneclose{}    THENW  Aut\000Co))

---

Home Index