---

Step * of Lemma regext-lemma

∀T:Type. ∀f:T ⟶ Set{i:l}. ∀B:Set{i:l}.
  ((∃t:T. ∃g:set-dom(f t) ⟶ Set{i:l}. seteq(B;g"(set-dom(f t))))
  ⇒ (∀R:Set{i:l} ⟶ Set{i:l} ⟶ ℙ'
        (SetRelation(R)
        ⇒  R:(B ⇒ regext(f"(T)))
        ⇒ (∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))))))
BY
{ (Auto THEN (InstLemma `regext-lemma1` [⌜T⌝;⌜f⌝;⌜B⌝]⋅ THENA Auto)) }

1
.....antecedent..... 
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)))
⊢ ∃t:T. ∃g:set-dom(f t) ⟶ coSet{i:l}. seteq(B;mk-coset(set-dom(f t);g))

2
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. ∀R:coSet{i:l} ⟶ coSet{i:l} ⟶ ℙ'
     (coSetRelation(R)
     ⇒  R:(B ⇒ regext(mk-coset(T;f)))
     ⇒ (∃b:coSet{i:l}. ((b ∈ regext(mk-coset(T;f))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))))
⊢ ∃b:Set{i:l}. ((b ∈ regext(f"(T))) ∧  R:(B ⇒ b) ∧ R:(B ─>> b))

---

Latex:

---

Latex:
\mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  Set\{i:l\}.  \mforall{}B:Set\{i:l\}.
    ((\mexists{}t:T.  \mexists{}g:set-dom(f  t)  {}\mrightarrow{}  Set\{i:l\}.  seteq(B;g"(set-dom(f  t))))
    {}\mRightarrow{}  (\mforall{}R:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}  {}\mrightarrow{}  \mBbbP{}'
                (SetRelation(R)
                {}\mRightarrow{}    R:(B  {}\mRightarrow{}  regext(f"(T)))
                {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  regext(f"(T)))  \mwedge{}    R:(B  {}\mRightarrow{}  b)  \mwedge{}  R:(B  {}>>  b))))))


By

---

Latex:
(Auto  THEN  (InstLemma  `regext-lemma1`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{};\mkleeneopen{}B\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index