---

Step * 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. set-predicate{i:l}(<T, s1>;a.P[a])
5. a : coSet{i:l}
6. t : T
7. b1 : P[s1 t]
8. seteq(a;s1 t)
9. ∃b:T. seteq(a;s1 b)
⊢ P[a]
BY
{ ((Assert seteq(s1 t;a) BY
          Auto)
   THEN Unfold `set-predicate` 4
   THEN FHyp 4 [-1]
   THEN Auto
   THEN Fold `mk-coset` 0
   THEN (RWO "setmem-iff" 0 THEN Auto)
   THEN RepUR ``mk-coset set-dom set-item`` 0
   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.  set-predicate\{i:l\}(<T,  s1>a.P[a])
5.  a  :  coSet\{i:l\}
6.  t  :  T
7.  b1  :  P[s1  t]
8.  seteq(a;s1  t)
9.  \mexists{}b:T.  seteq(a;s1  b)
\mvdash{}  P[a]


By

---

Latex:
((Assert  seteq(s1  t;a)  BY
                Auto)
  THEN  Unfold  `set-predicate`  4
  THEN  FHyp  4  [-1]
  THEN  Auto
  THEN  Fold  `mk-coset`  0
  THEN  (RWO  "setmem-iff"  0  THEN  Auto)
  THEN  RepUR  ``mk-coset  set-dom  set-item``  0
  THEN  Auto)

---

Home Index