---

Step * 1 1 1 of Lemma subset-co-regext


1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. x : coSet{i:l}@i'
5. b : T@i
6. seteq(x;f b)
7. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
8. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
⊢ ∃b:coW(T;x.set-dom(f x)). seteq(x;regextfun(f;b))
BY
{ ((D 0 With ⌜regextW(G;b)⌝  THENW Auto) THEN (RWO "-3" 0 THENA Auto) THEN ThinVar `x') }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. ∀i:T. ∀i@0:set-dom(f i).  ∃b:T. seteq(set-item(f i;i@0);f b)
4. b : T@i
5. G : i:T ⟶ i@0:set-dom(f i) ⟶ T
6. ∀i:T. ∀i@0:set-dom(f i).  seteq(set-item(f i;i@0);f (G i i@0))
⊢ seteq(f b;regextfun(f;regextW(G;b)))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    \mexists{}b:T.  seteq(set-item(f  i;i@0);f  b)
4.  x  :  coSet\{i:l\}@i'
5.  b  :  T@i
6.  seteq(x;f  b)
7.  G  :  i:T  {}\mrightarrow{}  i@0:set-dom(f  i)  {}\mrightarrow{}  T
8.  \mforall{}i:T.  \mforall{}i@0:set-dom(f  i).    seteq(set-item(f  i;i@0);f  (G  i  i@0))
\mvdash{}  \mexists{}b:coW(T;x.set-dom(f  x)).  seteq(x;regextfun(f;b))


By

---

Latex:
((D  0  With  \mkleeneopen{}regextW(G;b)\mkleeneclose{}    THENW  Auto)  THEN  (RWO  "-3"  0  THENA  Auto)  THEN  ThinVar  `x')

---

Home Index