---

Step * of Lemma setmem-setunionfun

∀s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}.
  (set-function{i:l}(s; x.f[x]) ⇒ (∀y:coSet{i:l}. ((y ∈  ⋃x∈s.f[x]) ⇐⇒ ∃x:coSet{i:l}. ((x ∈ s) ∧ (y ∈ f[x])))))
BY
{ (Auto THEN (coSetD 1 THEN D 1) THEN RenameVar `g' 2) }

1
1. T : Type
2. g : T ⟶ coSet{i:l}
3. f : {x:coSet{i:l}| (x ∈ <T, g>)}  ⟶ coSet{i:l}
4. set-function{i:l}(<T, g>; x.f[x])
5. y : coSet{i:l}
6. (y ∈  ⋃x∈<T, g>.f[x])
⊢ ∃x:coSet{i:l}. ((x ∈ <T, g>) ∧ (y ∈ f[x]))

2
1. T : Type
2. g : T ⟶ coSet{i:l}
3. f : {x:coSet{i:l}| (x ∈ <T, g>)}  ⟶ coSet{i:l}
4. set-function{i:l}(<T, g>; x.f[x])
5. y : coSet{i:l}
6. ∃x:coSet{i:l}. ((x ∈ <T, g>) ∧ (y ∈ f[x]))
⊢ (y ∈  ⋃x∈<T, g>.f[x])

---

Latex:

---

Latex:
\mforall{}s:coSet\{i:l\}.  \mforall{}f:\{x:coSet\{i:l\}|  (x  \mmember{}  s)\}    {}\mrightarrow{}  coSet\{i:l\}.
    (set-function\{i:l\}(s;  x.f[x])
    {}\mRightarrow{}  (\mforall{}y:coSet\{i:l\}.  ((y  \mmember{}    \mcup{}x\mmember{}s.f[x])  \mLeftarrow{}{}\mRightarrow{}  \mexists{}x:coSet\{i:l\}.  ((x  \mmember{}  s)  \mwedge{}  (y  \mmember{}  f[x])))))


By

---

Latex:
(Auto  THEN  (coSetD  1  THEN  D  1)  THEN  RenameVar  `g'  2)

---

Home Index