---

Step * of Lemma setmem-sub-coset

∀s:coSet{i:l}
  ∀[P:{a:coSet{i:l}| (a ∈ s)}  ⟶ ℙ]
    (set-predicate{i:l}(s;a.P[a]) ⇒ (∀a:coSet{i:l}. ((a ∈ {a ∈ s | P[a]}) ⇐⇒ (a ∈ s) ∧ P[a])))
BY
{ (Intros
   THEN Try ((At ⌜𝕌'⌝ (D 0)⋅ THEN BLemma `set-predicate_wf` THEN Auto))
   THEN (RepeatFor 2 (D 0) THENA Auto)
   THEN (coSetD 1 THEN D 1)
   THEN All (\h. ((RepUR ``sub-set`` h THEN Fold `Wsup` h THEN Fold `mk-set` h)
                  THEN (RWO "setmem-mk-set-sq" h THENA Auto)
                  THEN Reduce h) )⋅
   THEN ExRepD
   THEN Try (DProds)
   THEN All Reduce
   THEN Auto) }

1
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]

2
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. b : T
7. seteq(a;s1 b)
8. P[a]
⊢ ∃b:t:T × P[s1 t]. seteq(a;s1 (fst(b)))

---

Latex:

---

Latex:
\mforall{}s:coSet\{i:l\}
    \mforall{}[P:\{a:coSet\{i:l\}|  (a  \mmember{}  s)\}    {}\mrightarrow{}  \mBbbP{}]
        (set-predicate\{i:l\}(s;a.P[a])  {}\mRightarrow{}  (\mforall{}a:coSet\{i:l\}.  ((a  \mmember{}  \{a  \mmember{}  s  |  P[a]\})  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  s)  \mwedge{}  P[a])))


By

---

Latex:
(Intros
  THEN  Try  ((At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}  (D  0)\mcdot{}  THEN  BLemma  `set-predicate\_wf`  THEN  Auto))
  THEN  (RepeatFor  2  (D  0)  THENA  Auto)
  THEN  (coSetD  1  THEN  D  1)
  THEN  All  (\mbackslash{}h.  ((RepUR  ``sub-set``  h  THEN  Fold  `Wsup`  h  THEN  Fold  `mk-set`  h)
                                THEN  (RWO  "setmem-mk-set-sq"  h  THENA  Auto)
                                THEN  Reduce  h)  )\mcdot{}
  THEN  ExRepD
  THEN  Try  (DProds)
  THEN  All  Reduce
  THEN  Auto)

---

Home Index