---

Step * 2 1 of Lemma regext-lemma


1. T : Type
2. f : T ⟶ Set{i:l}
3. B : Set{i:l}
4. ∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t)))
5. R : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
6. SetRelation(R)
7.  R:(B ⇒ regext(f"(T)))
8. coSetRelation(λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)))
⇒  λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ⇒ regext(mk-coset(T;f)))
⇒ (∃b:coSet{i:l}
     ((b ∈ regext(mk-coset(T;f)))
     ∧  λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ⇒ b)
     ∧ λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ─>> b)))
⊢ ∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))
BY
{ (D -1 THENA ((D 0 THEN Reduce 0) THEN Auto THEN RWO "-5<" 0 THEN Auto)) }

1
1. T : Type
2. f : T ⟶ Set{i:l}
3. B : Set{i:l}
4. ∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t)))
5. R : Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
6. SetRelation(R)
7.  R:(B ⇒ regext(f"(T)))
8.  λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ⇒ regext(mk-coset(T;f)))
⇒ (∃b:coSet{i:l}
     ((b ∈ regext(mk-coset(T;f)))
     ∧  λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ⇒ b)
     ∧ λx,y. ((x ∈ B) ∧ (y ∈ regext(f"(T))) ∧ (R x y)):(B ─>> b)))
⊢ ∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -1  THENA  ((D  0  THEN  Reduce  0)  THEN  Auto  THEN  RWO  "-5<"  0  THEN  Auto))

---

Home Index