---

Step * 1 1 1 2 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))))))
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))))
16. (regextfun(f;Wsup(t;F)) ∈ mk-coset(W(T;x.set-dom(f x));λw.regextfun(f;w)))
17. x : coSet{i:l}
18. t1 : set-dom(f t)
19. seteq(x;g t1)
20. (regextfun(f;F t1) ∈ regextfun(f;Wsup(t;F)))
⊢ R x regextfun(f;F t1)
BY
{ ((Assert R (g t1) regextfun(f;F t1) BY
          Auto)
   THEN (Assert seteq(regextfun(f;F t1);regextfun(f;F t1)) ∧ seteq(g t1;x) BY
               (D 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))))
16. (regextfun(f;Wsup(t;F)) ∈ mk-coset(W(T;x.set-dom(f x));λw.regextfun(f;w)))
17. x : coSet{i:l}
18. t1 : set-dom(f t)
19. seteq(x;g t1)
20. (regextfun(f;F t1) ∈ regextfun(f;Wsup(t;F)))
21. R (g t1) regextfun(f;F t1)
22. seteq(regextfun(f;F t1);regextfun(f;F t1)) ∧ seteq(g t1;x)
⊢ R x regextfun(f;F t1)

---

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))))))
11.  \mforall{}x:set-dom(f  t).  \mexists{}y:W(T;x.set-dom(f  x)).  (R  (g  x)  regextfun(f;y))
12.  F  :  x:set-dom(f  t)  {}\mrightarrow{}  W(T;x.set-dom(f  x))
13.  \mforall{}x:set-dom(f  t).  (R  (g  x)  regextfun(f;F  x))
14.  Wsup(t;F)  \mmember{}  W(T;x.set-dom(f  x))
15.  (regextfun(f;Wsup(t;F))  \mmember{}  \mlambda{}w.regextfun(f;w)"(W(T;x.set-dom(f  x))))
16.  (regextfun(f;Wsup(t;F))  \mmember{}  mk-coset(W(T;x.set-dom(f  x));\mlambda{}w.regextfun(f;w)))
17.  x  :  coSet\{i:l\}
18.  t1  :  set-dom(f  t)
19.  seteq(x;g  t1)
20.  (regextfun(f;F  t1)  \mmember{}  regextfun(f;Wsup(t;F)))
\mvdash{}  R  x  regextfun(f;F  t1)


By

---

Latex:
((Assert  R  (g  t1)  regextfun(f;F  t1)  BY
                Auto)
  THEN  (Assert  seteq(regextfun(f;F  t1);regextfun(f;F  t1))  \mwedge{}  seteq(g  t1;x)  BY
                          (D  0  THEN  RelRST  THEN  Auto))
  )

---

Home Index