---

Step * 1 1 of Lemma co-regext-Regularcoset


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))
BY
{ (InstConcl [⌜x⌝;⌜λu.regextfun(a1;g u)⌝]⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  B  :  coSet\{i:l\}
4.  x  :  T
5.  g  :  set-dom(a1  x)  {}\mrightarrow{}  coW(T;x.set-dom(a1  x))
6.  seteq(B;\mlambda{}u.regextfun(a1;g  u)"(set-dom(a1  x)))
7.  R  :  coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
8.  coSetRelation(R)
9.    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:
(InstConcl  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}\mlambda{}u.regextfun(a1;g  u)\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index