Step
*
1
1
of Lemma
co-regext-lemma
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 ∈ co-regext(mk-coset(T;f))) ∧ (R x y))))
10. ∀x:coSet{i:l}. ((x ∈ co-regext(mk-coset(T;f))) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ co-regext(mk-coset(T;f))))))
11. ∀x:set-dom(f t). ∃y:coW(T;x.set-dom(f x)). (R (g x) regextfun(f;y))
12. F : x:set-dom(f t) ⟶ coW(T;x.set-dom(f x))
13. ∀x:set-dom(f t). (R (g x) regextfun(f;F x))
14. coWsup(t;F) ∈ coW(T;x.set-dom(f x))
15. (regextfun(f;coWsup(t;F)) ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w)))
⊢ ∃b:coSet{i:l}. ((b ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w))) ∧ R:(B ⇒ b) ∧ R:(B ─>> b))
BY
{ (D 0 With ⌜regextfun(f;coWsup(t;F))⌝ 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 ∈ co-regext(mk-coset(T;f))) ∧ (R x y))))
10. ∀x:coSet{i:l}. ((x ∈ co-regext(mk-coset(T;f))) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ co-regext(mk-coset(T;f))))))
11. ∀x:set-dom(f t). ∃y:coW(T;x.set-dom(f x)). (R (g x) regextfun(f;y))
12. F : x:set-dom(f t) ⟶ coW(T;x.set-dom(f x))
13. ∀x:set-dom(f t). (R (g x) regextfun(f;F x))
14. coWsup(t;F) ∈ coW(T;x.set-dom(f x))
15. (regextfun(f;coWsup(t;F)) ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w)))
16. (regextfun(f;coWsup(t;F)) ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w)))
⊢ R:(B ⇒ regextfun(f;coWsup(t;F)))
2
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 ∈ co-regext(mk-coset(T;f))) ∧ (R x y))))
10. ∀x:coSet{i:l}. ((x ∈ co-regext(mk-coset(T;f))) ⇒ (∀x1:coSet{i:l}. ((x1 ∈ x) ⇒ (x1 ∈ co-regext(mk-coset(T;f))))))
11. ∀x:set-dom(f t). ∃y:coW(T;x.set-dom(f x)). (R (g x) regextfun(f;y))
12. F : x:set-dom(f t) ⟶ coW(T;x.set-dom(f x))
13. ∀x:set-dom(f t). (R (g x) regextfun(f;F x))
14. coWsup(t;F) ∈ coW(T;x.set-dom(f x))
15. (regextfun(f;coWsup(t;F)) ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w)))
16. (regextfun(f;coWsup(t;F)) ∈ mk-coset(coW(T;x.set-dom(f x));λw.regextfun(f;w)))
17. R:(B ⇒ regextfun(f;coWsup(t;F)))
⊢ R:(B ─>> regextfun(f;coWsup(t;F)))
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{} co-regext(mk-coset(T;f))) \mwedge{} (R x y))))
10. \mforall{}x:coSet\{i:l\}
((x \mmember{} co-regext(mk-coset(T;f)))
{}\mRightarrow{} (\mforall{}x1:coSet\{i:l\}. ((x1 \mmember{} x) {}\mRightarrow{} (x1 \mmember{} co-regext(mk-coset(T;f))))))
11. \mforall{}x:set-dom(f t). \mexists{}y:coW(T;x.set-dom(f x)). (R (g x) regextfun(f;y))
12. F : x:set-dom(f t) {}\mrightarrow{} coW(T;x.set-dom(f x))
13. \mforall{}x:set-dom(f t). (R (g x) regextfun(f;F x))
14. coWsup(t;F) \mmember{} coW(T;x.set-dom(f x))
15. (regextfun(f;coWsup(t;F)) \mmember{} mk-coset(coW(T;x.set-dom(f x));\mlambda{}w.regextfun(f;w)))
\mvdash{} \mexists{}b:coSet\{i:l\}
((b \mmember{} mk-coset(coW(T;x.set-dom(f x));\mlambda{}w.regextfun(f;w))) \mwedge{} R:(B {}\mRightarrow{} b) \mwedge{} R:(B {}>> b))
By
Latex:
(D 0 With \mkleeneopen{}regextfun(f;coWsup(t;F))\mkleeneclose{} THEN Auto)
Home
Index