---

Step * 1 of Lemma setmem-closure-set


1. B : Set{i:l}
2. Y : Set{i:l} ⟶ Set{i:l}
3. x : Set{i:l}
4. ∀b:Set{i:l}. ((b ∈ B) ⇒ set-function{i:l}(setimages(b;x); A.Y A))
5. z : Set{i:l}
⊢ ∃b:coSet{i:l}. ((b ∈ B) ∧ (z ∈  ⋃A∈setimages(b;x).Y A))
⇐⇒ ∃b:coSet{i:l}. ((b ∈ B) ∧ (∃A:coSet{i:l}. ((A ∈ setimages(b;x)) ∧ (z ∈ Y A))))
BY
{ (RWO "setmem-setunionfun" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  B  :  Set\{i:l\}
2.  Y  :  Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
3.  x  :  Set\{i:l\}
4.  \mforall{}b:Set\{i:l\}.  ((b  \mmember{}  B)  {}\mRightarrow{}  set-function\{i:l\}(setimages(b;x);  A.Y  A))
5.  z  :  Set\{i:l\}
\mvdash{}  \mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  (z  \mmember{}    \mcup{}A\mmember{}setimages(b;x).Y  A))
\mLeftarrow{}{}\mRightarrow{}  \mexists{}b:coSet\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  (\mexists{}A:coSet\{i:l\}.  ((A  \mmember{}  setimages(b;x))  \mwedge{}  (z  \mmember{}  Y  A))))


By

---

Latex:
(RWO  "setmem-setunionfun"  0  THEN  Auto)

---

Home Index