---

Step * 2 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))} )
⊢ ∀z:coSet{i:l}
    (∃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)))
    ⇐⇒ (z ∈ mk-coset(T;λt@0.(f1 t@0,set-item(B[f1 t@0];f t@0)))))
BY
{ (RepUR ``set-dom set-item mk-coset`` 0 THEN Fold `set-item` 0 THEN Fold `mk-coset` 0 THEN 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))} )
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))))

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

---

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))\}  )
\mvdash{}  \mforall{}z:coSet\{i:l\}
        (\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)))
        \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  mk-coset(T;\mlambda{}t@0.(f1  t@0,set-item(B[f1  t@0];f  t@0)))))


By

---

Latex:
(RepUR  ``set-dom  set-item  mk-coset``  0  THEN  Fold  `set-item`  0  THEN  Fold  `mk-coset`  0  THEN  Auto)

---

Home Index