---

Step * of Lemma subset-co-regext

∀a:coSet{i:l}. (transitive-set(a) ⇒ (a ⊆ co-regext(a)))
BY
{ (Auto
   THEN RWO "setsubset-iff" 0
   THEN Auto
   THEN coSetD 1
   THEN D 1
   THEN RenameVar `f' 2
   THEN RepUR ``co-regext setmem coWmem coW-dom mk-coset coW-item`` 0) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. transitive-set(<T, f>)
4. x : coSet{i:l}@i'
5. (x ∈ <T, f>)
⊢ ∃b:coW(T;x.set-dom(f x)). coW-equiv(T.T;x;regextfun(f;b))

---

Latex:

---

Latex:
\mforall{}a:coSet\{i:l\}.  (transitive-set(a)  {}\mRightarrow{}  (a  \msubseteq{}  co-regext(a)))


By

---

Latex:
(Auto
  THEN  RWO  "setsubset-iff"  0
  THEN  Auto
  THEN  coSetD  1
  THEN  D  1
  THEN  RenameVar  `f'  2
  THEN  RepUR  ``co-regext  setmem  coWmem  coW-dom  mk-coset  coW-item``  0)

---

Home Index