---

Step * of Lemma mem-mk-set_wf

∀[T:Type]. ∀[f:T ⟶ coSet{i:l}]. ∀[t:T].  (mem-mk-set(f;t) ∈ (f t ∈ mk-coset(T;f)))
BY
{ ((Auto THEN RepUR ``mem-mk-set setmem mk-coset coWmem coW-dom coW-item Wsup`` 0) THEN Fold `seteq` 0 THEN Auto) }

1
1. T : Type
2. f : T ⟶ coSet{i:l}
3. t : T
⊢ seteqweaken(f t) Ax ∈ seteq(f t;f t)

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[f:T  {}\mrightarrow{}  coSet\{i:l\}].  \mforall{}[t:T].    (mem-mk-set(f;t)  \mmember{}  (f  t  \mmember{}  mk-coset(T;f)))


By

---

Latex:
((Auto  THEN  RepUR  ``mem-mk-set  setmem  mk-coset  coWmem  coW-dom  coW-item  Wsup``  0)
  THEN  Fold  `seteq`  0
  THEN  Auto)

---

Home Index