---

Step * of Lemma sub-set_wf

∀[s:coSet{i:l}]. ∀[P:{a:coSet{i:l}| (a ∈ s)}  ⟶ ℙ].  ({a ∈ s | P[a]} ∈ coSet{i:l})
BY
{ (Intros
   THEN Unhide
   THEN coSetD 1
   THEN D 1
   THEN RepUR ``sub-set`` 0
   THEN RepeatFor 2 ((Fold  `mk-coset` 0 THEN Auto))
   THEN MemTypeCD
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s:coSet\{i:l\}].  \mforall{}[P:\{a:coSet\{i:l\}|  (a  \mmember{}  s)\}    {}\mrightarrow{}  \mBbbP{}].    (\{a  \mmember{}  s  |  P[a]\}  \mmember{}  coSet\{i:l\})


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  coSetD  1
  THEN  D  1
  THEN  RepUR  ``sub-set``  0
  THEN  RepeatFor  2  ((Fold    `mk-coset`  0  THEN  Auto))
  THEN  MemTypeCD
  THEN  Auto)

---

Home Index