---

Step * 1 1 of Lemma subset-co-regext


1. T : Type
2. f : T ⟶ coSet{i:l}
3. transitive-set(<T, f>)
4. x : coSet{i:l}@i'
5. b : T@i
6. coW-equiv(T.T;x;f b)
⊢ ∃b:coW(T;x.set-dom(f x)). coW-equiv(T.T;x;regextfun(f;b))
BY
{ (RepUR ``transitive-set allsetmem set-dom set-item`` 3
   THEN RepUR ``setsubset allsetmem setmem coWmem coW-dom coW-item`` 3
   THEN Fold `seteq` 3
   THEN (Skolemize 3 `G' THENA Auto)
   THEN All (Fold `seteq`)) }

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. 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))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  transitive-set(<T,  f>)
4.  x  :  coSet\{i:l\}@i'
5.  b  :  T@i
6.  coW-equiv(T.T;x;f  b)
\mvdash{}  \mexists{}b:coW(T;x.set-dom(f  x)).  coW-equiv(T.T;x;regextfun(f;b))


By

---

Latex:
(RepUR  ``transitive-set  allsetmem  set-dom  set-item``  3
  THEN  RepUR  ``setsubset  allsetmem  setmem  coWmem  coW-dom  coW-item``  3
  THEN  Fold  `seteq`  3
  THEN  (Skolemize  3  `G'  THENA  Auto)
  THEN  All  (Fold  `seteq`))

---

Home Index