---

Step * 1 of Lemma regext-lemma1


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))
BY
{ ((Assert ∀x:set-dom(f t). ∃y:W(T;x.set-dom(f x)). (R (g x) regextfun(f;y)) BY
          ((D 0 THENA Auto)
           THEN (InstHyp [⌜g x⌝] (-3)⋅ THENA (Auto THEN RWO "-6" 0 THEN Auto))
           THEN (ExRepD THEN DupHyp (-2))
           THEN SetMemDef (-1)
           THEN D 0 With ⌜b⌝ 
           THEN Auto
           THEN (Assert seteq(g x;g x) BY
                       Auto)
           THEN Auto))
   THEN (Skolemize (-1) `F'  THENA Auto)
   THEN (Assert Wsup(t;F) ∈ W(T;x.set-dom(f x)) BY
               Auto)
   THEN (Assert (regextfun(f;Wsup(t;F)) ∈ λw.regextfun(f;w)"(W(T;x.set-dom(f x)))) BY
               (SetMemDef 0 THEN D 0 With ⌜<t, F>⌝  THEN Auto THEN Fold `Wsup` 0 THEN RelRST THEN Auto))) }

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))))))
11. ∀x:set-dom(f t). ∃y:W(T;x.set-dom(f x)). (R (g x) regextfun(f;y))
12. F : x:set-dom(f t) ⟶ W(T;x.set-dom(f x))
13. ∀x:set-dom(f t). (R (g x) regextfun(f;F x))
14. Wsup(t;F) ∈ W(T;x.set-dom(f x))
15. (regextfun(f;Wsup(t;F)) ∈ λw.regextfun(f;w)"(W(T;x.set-dom(f x))))
⊢ ∃b:coSet{i:l}. ((b ∈ λw.regextfun(f;w)"(W(T;x.set-dom(f x)))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))

---

Latex:

---

Latex:

1.  T  :  Type
2.  f  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  B  :  coSet\{i:l\}
4.  t  :  T
5.  g  :  set-dom(f  t)  {}\mrightarrow{}  coSet\{i:l\}
6.  seteq(B;mk-coset(set-dom(f  t);g))
7.  R  :  coSet\{i:l\}  {}\mrightarrow{}  coSet\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
8.  \mforall{}x,x',y,y':coSet\{i:l\}.    (seteq(x;x')  {}\mRightarrow{}  seteq(y;y')  {}\mRightarrow{}  (R  x  y)  {}\mRightarrow{}  (R  x'  y'))
9.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  B)  {}\mRightarrow{}  (\mexists{}y:coSet\{i:l\}.  ((y  \mmember{}  regext(mk-coset(T;f)))  \mwedge{}  (R  x  y))))
10.  \mforall{}x:coSet\{i:l\}
            ((x  \mmember{}  regext(mk-coset(T;f)))  {}\mRightarrow{}  (\mforall{}x1:coSet\{i:l\}.  ((x1  \mmember{}  x)  {}\mRightarrow{}  (x1  \mmember{}  regext(mk-coset(T;f))))))
\mvdash{}  \mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  \mlambda{}w.regextfun(f;w)"(W(T;x.set-dom(f  x))))  \mwedge{}    R:(B  {}\mRightarrow{}  b)  \mwedge{}  R:(B  {}>>  b))


By

---

Latex:
((Assert  \mforall{}x:set-dom(f  t).  \mexists{}y:W(T;x.set-dom(f  x)).  (R  (g  x)  regextfun(f;y))  BY
                ((D  0  THENA  Auto)
                  THEN  (InstHyp  [\mkleeneopen{}g  x\mkleeneclose{}]  (-3)\mcdot{}  THENA  (Auto  THEN  RWO  "-6"  0  THEN  Auto))
                  THEN  (ExRepD  THEN  DupHyp  (-2))
                  THEN  SetMemDef  (-1)
                  THEN  D  0  With  \mkleeneopen{}b\mkleeneclose{} 
                  THEN  Auto
                  THEN  (Assert  seteq(g  x;g  x)  BY
                                          Auto)
                  THEN  Auto))
  THEN  (Skolemize  (-1)  `F'    THENA  Auto)
  THEN  (Assert  Wsup(t;F)  \mmember{}  W(T;x.set-dom(f  x))  BY
                          Auto)
  THEN  (Assert  (regextfun(f;Wsup(t;F))  \mmember{}  \mlambda{}w.regextfun(f;w)"(W(T;x.set-dom(f  x))))  BY
                          (SetMemDef  0  THEN  D  0  With  \mkleeneopen{}<t,  F>\mkleeneclose{}    THEN  Auto  THEN  Fold  `Wsup`  0  THEN  RelRST  THEN  Auto\000C)))

---

Home Index