---

Step * 1 of Lemma regext-transitive


1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. x : coSet{i:l}@i'
4. b : W(T;x.set-dom(a1 x))@i
5. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ regextfun(a1;b)))
6. x1 : coSet{i:l}@i'
7. (x1 ∈ x)
⊢ ∃b:W(T;x.set-dom(a1 x)). seteq(x1;regextfun(a1;b))
BY
{ ((Assert (x1 ∈ regextfun(a1;b)) BY Auto) THEN (RWO "setmem-iff" (-1) THENA Auto) THEN ExRepD THEN DWtype 4 THEN D 4) }

1
1. T : Type
2. a1 : T ⟶ coSet{i:l}
3. x : coSet{i:l}@i'
4. a : T
5. b1 : set-dom(a1 a) ⟶ W(T;a.set-dom(a1 a))
6. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ (z ∈ regextfun(a1;<a, b1>)))
7. x1 : coSet{i:l}@i'
8. (x1 ∈ x)
9. t : set-dom(regextfun(a1;<a, b1>))
10. seteq(x1;set-item(regextfun(a1;<a, b1>);t))
⊢ ∃b:W(T;x.set-dom(a1 x)). seteq(x1;regextfun(a1;b))

---

Latex:

---

Latex:

1.  T  :  Type
2.  a1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  x  :  coSet\{i:l\}@i'
4.  b  :  W(T;x.set-dom(a1  x))@i
5.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  regextfun(a1;b)))
6.  x1  :  coSet\{i:l\}@i'
7.  (x1  \mmember{}  x)
\mvdash{}  \mexists{}b:W(T;x.set-dom(a1  x)).  seteq(x1;regextfun(a1;b))


By

---

Latex:
((Assert  (x1  \mmember{}  regextfun(a1;b))  BY
                Auto)
  THEN  (RWO  "setmem-iff"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  DWtype  4
  THEN  D  4)

---

Home Index