---

Step * of Lemma regext-lemma1

∀T:Type. ∀f:T ⟶ coSet{i:l}. ∀B:coSet{i:l}.
  ((∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g)))
  ⇒ (∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
        (coSetRelation(R)
        ⇒  R:(B ⇒ regext(mk-coset(T;f)))
        ⇒ (∃b:coSet{i:l}. ((b ∈ regext(mk-coset(T;f))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))))))
BY
{ (Auto
   THEN (Assert transitive-set(regext(mk-coset(T;f))) BY
               Auto)
   THEN (RWO "transitive-set-iff" (-1) THENA Auto)
   THEN RWO "setsubset-iff" (-1)
   THEN Auto
   THEN (UnfoldTopAb (-3) THEN UnfoldTopAb (-2))
   THEN ExRepD
   THEN RepUR ``regext`` 0) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. B : coSet{i:l}
4. t : T
5. g : set-dom(f t) ⟶ coSet{i:l}
6. seteq(B;mk-coset(set-dom(f t);g))
7. R : coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
8. ∀x,x',y,y':coSet{i:l}.  (seteq(x;x') ⇒ seteq(y;y') ⇒ (R x y) ⇒ (R x' y'))
9. ∀x:coSet{i:l}. ((x ∈ B) ⇒ (∃y:coSet{i:l}. ((y ∈ regext(mk-coset(T;f))) ∧ (R x y))))
10. ∀x:coSet{i:l}. ((x ∈ regext(mk-coset(T;f))) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ regext(mk-coset(T;f))))))
⊢ ∃b:coSet{i:l}. ((b ∈ λw.regextfun(f;w)"(W(T;x.set-dom(f x)))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  coSet\{i:l\}.  \mforall{}B:coSet\{i:l\}.
    ((\mexists{}t:T.  \mexists{}g:set-dom(f  t)  {}\mrightarrow{}  coSet\{i:l\}.  seteq(B;mk-coset(set-dom(f  t);g)))
    {}\mRightarrow{}  (\mforall{}R:coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
                (coSetRelation(R)
                {}\mRightarrow{}    R:(B  {}\mRightarrow{}  regext(mk-coset(T;f)))
                {}\mRightarrow{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  regext(mk-coset(T;f)))  \mwedge{}    R:(B  {}\mRightarrow{}  b)  \mwedge{}  R:(B  {}>>  b))))))


By

---

Latex:
(Auto
  THEN  (Assert  transitive-set(regext(mk-coset(T;f)))  BY
                          Auto)
  THEN  (RWO  "transitive-set-iff"  (-1)  THENA  Auto)
  THEN  RWO  "setsubset-iff"  (-1)
  THEN  Auto
  THEN  (UnfoldTopAb  (-3)  THEN  UnfoldTopAb  (-2))
  THEN  ExRepD
  THEN  RepUR  ``regext``  0)

---

Home Index