---

Step * 1 1 of Lemma regext-Regularcoset


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

---

Home Index