---

Step * 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.  R:(B ⇒ regextfun(f;Wsup(t;F)))
⊢ R:(B ─>> regextfun(f;Wsup(t;F)))
BY
{ (D 0 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.  R:(B ⇒ regextfun(f;Wsup(t;F)))
18. y : coSet{i:l}
19. (y ∈ regextfun(f;Wsup(t;F)))
⊢ ∃x:coSet{i:l}. ((x ∈ B) ∧ (R x y))

---

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.    R:(B  {}\mRightarrow{}  regextfun(f;Wsup(t;F)))
\mvdash{}  R:(B  {}>>  regextfun(f;Wsup(t;F)))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index