---

Step * 1 1 of Lemma co-regext-transitive


1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. x : coSet{i:l}
4. x2 : T
5. t2 : set-dom(a1 x2) ⟶ coW(T;x.set-dom(a1 x))
6. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ regextfun(a1;<x2, t2>)))
7. x1 : coSet{i:l}
8. (x1 ∈ x)
9. t1 : set-dom(regextfun(a1;<x2, t2>))
10. seteq(x1;set-item(regextfun(a1;<x2, t2>);t1))
⊢ ∃t:coW(T;x.set-dom(a1 x)). seteq(x1;regextfun(a1;t))
BY
{ (RecUnfold `regextfun` (-1) THEN Reduce -1 THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  x2  :  T
5.  t2  :  set-dom(a1  x2)  {}\mrightarrow{}  coW(T;x.set-dom(a1  x))
6.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  regextfun(a1;<x2,  t2>)))
7.  x1  :  coSet\{i:l\}
8.  (x1  \mmember{}  x)
9.  t1  :  set-dom(regextfun(a1;<x2,  t2>))
10.  seteq(x1;set-item(regextfun(a1;<x2,  t2>);t1))
\mvdash{}  \mexists{}t:coW(T;x.set-dom(a1  x)).  seteq(x1;regextfun(a1;t))


By

---

Latex:
(RecUnfold  `regextfun`  (-1)  THEN  Reduce  -1  THEN  Auto)

---

Home Index