---

Step * of Lemma setmem-unionfun-implies

∀s:coSet{i:l}. ∀f:{x:coSet{i:l}| (x ∈ s)}  ⟶ coSet{i:l}. ∀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 THEN SetMemDef (-1) THEN D -2 THEN All Reduce) }

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

---

Latex:

---

Latex:
\mforall{}s:coSet\{i:l\}.  \mforall{}f:\{x:coSet\{i:l\}|  (x  \mmember{}  s)\}    {}\mrightarrow{}  coSet\{i:l\}.  \mforall{}y:coSet\{i:l\}.
    ((y  \mmember{}    \mcup{}x\mmember{}s.f[x])  {}\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  THEN  SetMemDef  (-1)  THEN  D  -2  THEN  All  Reduce)

---

Home Index