---

Step * 2 1 of Lemma setmem-sub-coset


1. T : Type
2. s1 : T ⟶ coSet{i:l}
3. [P] : {a:coSet{i:l}| ∃b:T. seteq(a;s1 b)}  ⟶ ℙ
4. ∀a1,a2:coSet{i:l}.  ((a1 ∈ <T, s1>) ⇒ (a2 ∈ <T, s1>) ⇒ seteq(a1;a2) ⇒ P[a1] ⇒ P[a2])
5. a : coSet{i:l}
6. b : T
7. seteq(a;s1 b)
8. P[a]
9. P[s1 b]
⊢ ∃b:t:T × P[s1 t]. seteq(a;s1 (fst(b)))
BY
{ (RenameVar `m' (-1) THEN D 0 With ⌜<b, m>⌝  THEN Auto) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  s1  :  T  {}\mrightarrow{}  coSet\{i:l\}
3.  [P]  :  \{a:coSet\{i:l\}|  \mexists{}b:T.  seteq(a;s1  b)\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}a1,a2:coSet\{i:l\}.    ((a1  \mmember{}  <T,  s1>)  {}\mRightarrow{}  (a2  \mmember{}  <T,  s1>)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  P[a1]  {}\mRightarrow{}  P[a2])
5.  a  :  coSet\{i:l\}
6.  b  :  T
7.  seteq(a;s1  b)
8.  P[a]
9.  P[s1  b]
\mvdash{}  \mexists{}b:t:T  \mtimes{}  P[s1  t].  seteq(a;s1  (fst(b)))


By

---

Latex:
(RenameVar  `m'  (-1)  THEN  D  0  With  \mkleeneopen{}<b,  m>\mkleeneclose{}    THEN  Auto)

---

Home Index