---

Step * 2 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))} )
⊢ seteq(x;mk-coset(T;λt@0.(f1 t@0,set-item(B[f1 t@0];f t@0))))
BY
{ ((RWO "co-seteq-iff" 0 THENA Auto) THEN (RWO "-2" 0 THENA 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))} )
⊢ ∀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)))))

---

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


By

---

Latex:
((RWO  "co-seteq-iff"  0  THENA  Auto)  THEN  (RWO  "-2"  0  THENA  Auto))

---

Home Index