---

Step * 1 of Lemma co-regext-Regularcoset


1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. B : coSet{i:l}
4. (B ∈ co-regext(mk-coset(T;a1)))
5. R : coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
6. coSetRelation(R)
7.  R:(B ⇒ co-regext(mk-coset(T;a1)))
⊢ ∃t:T. ∃g:set-dom(a1 t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(a1 t);g))
BY
{ (SetMemDef (-4) THEN coWD (-5) THEN D -5 THEN RenameVar `g' (-5) THEN RecUnfold `regextfun` (-4) THEN Reduce -4) }

1
1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. B : coSet{i:l}
4. x : T
5. g : set-dom(a1 x) ⟶ coW(T;x.set-dom(a1 x))
6. seteq(B;λu.regextfun(a1;g u)"(set-dom(a1 x)))
7. R : coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
8. coSetRelation(R)
9.  R:(B ⇒ co-regext(mk-coset(T;a1)))
⊢ ∃t:T. ∃g:set-dom(a1 t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(a1 t);g))

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  B  :  coSet\{i:l\}
4.  (B  \mmember{}  co-regext(mk-coset(T;a1)))
5.  R  :  coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
6.  coSetRelation(R)
7.    R:(B  {}\mRightarrow{}  co-regext(mk-coset(T;a1)))
\mvdash{}  \mexists{}t:T.  \mexists{}g:set-dom(a1  t)  {}\mrightarrow{}  coSet\{i:l\}.  seteq(B;mk-coset(set-dom(a1  t);g))


By

---

Latex:
(SetMemDef  (-4)
  THEN  coWD  (-5)
  THEN  D  -5
  THEN  RenameVar  `g'  (-5)
  THEN  RecUnfold  `regextfun`  (-4)
  THEN  Reduce  -4)

---

Home Index