---

Step * of Lemma regext-transitive

No Annotations
∀a:coSet{i:l}. transitive-set(regext(a))
BY
{ (RWO "transitive-set-iff" 0
   THEN Auto
   THEN coSetD 1
   THEN D 1
   THEN All (Fold `mk-coet`)
   THEN SetMemDef (-1)
   THEN RWO  "setsubset-iff" 0
   THEN Auto
   THEN SetMemDef 0
   THEN (RWO "co-seteq-iff" (-3) THENA Auto)) }

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

---

Latex:

---

Latex:
No  Annotations
\mforall{}a:coSet\{i:l\}.  transitive-set(regext(a))


By

---

Latex:
(RWO  "transitive-set-iff"  0
  THEN  Auto
  THEN  coSetD  1
  THEN  D  1
  THEN  All  (Fold  `mk-coet`)
  THEN  SetMemDef  (-1)
  THEN  RWO    "setsubset-iff"  0
  THEN  Auto
  THEN  SetMemDef  0
  THEN  (RWO  "co-seteq-iff"  (-3)  THENA  Auto))

---

Home Index