Step
*
1
1
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))))))
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)))
⊢ R:(B ⇒ regextfun(f;Wsup(t;F)))
BY
{ ((D 0 THEN Auto) THEN (RWO "6" (-1) THENA Auto) THEN SetMemDef (-1) THEN D 0 With ⌜regextfun(f;F t1)⌝ 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)
⊢ (regextfun(f;F t1) ∈ regextfun(f;Wsup(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 ∈ 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)
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)))
\mvdash{} R:(B {}\mRightarrow{} regextfun(f;Wsup(t;F)))
By
Latex:
((D 0 THEN Auto)
THEN (RWO "6" (-1) THENA Auto)
THEN SetMemDef (-1)
THEN D 0 With \mkleeneopen{}regextfun(f;F t1)\mkleeneclose{}
THEN Auto)
Home
Index