---

Step * 1 of Lemma regext-lemma

.....antecedent..... 
1. T : Type
2. f : T ⟶ Set{i:l}
3. B : Set{i:l}
4. ∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t)))
5. R : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
6. SetRelation(R)
7.  R:(B ⇒ regext(f"(T)))
⊢ ∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g))
BY
{ (RepeatFor 2 (ParallelOp -4) THEN (NthHypSq (-4) THEN Auto) THEN Computation) }

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  Set\{i:l\}
3.  B  :  Set\{i:l\}
4.  \mexists{}t:T.  \mexists{}g:set-dom(f  t)  {}\mrightarrow{}  Set\{i:l\}.  seteq(B;g"(set-dom(f  t)))
5.  R  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
6.  SetRelation(R)
7.    R:(B  {}\mRightarrow{}  regext(f"(T)))
\mvdash{}  \mexists{}t:T.  \mexists{}g:set-dom(f  t)  {}\mrightarrow{}  coSet\{i:l\}.  seteq(B;mk-coset(set-dom(f  t);g))


By

---

Latex:
(RepeatFor  2  (ParallelOp  -4)  THEN  (NthHypSq  (-4)  THEN  Auto)  THEN  Computation)

---

Home Index