---

Step * of Lemma setmem-closure-set

∀B:Set{i:l}. ∀Y:Set{i:l} ⟶ Set{i:l}. ∀x:Set{i:l}.
  ((∀b:Set{i:l}. ((b ∈ B) ⇒ set-function{i:l}(setimages(b;x); A.Y A)))
  ⇒ (∀z:Set{i:l}
        ((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃b:coSet{i:l}. ((b ∈ B) ∧ (∃A:coSet{i:l}. ((A ∈ setimages(b;x)) ∧ (z ∈ Y A)))))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `closure-set` 0 THEN (RW (AddrC [1] SetMemC) 0 THENA (Auto THEN D 0 THEN Auto))) }

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

---

Latex:

---

Latex:
\mforall{}B:Set\{i:l\}.  \mforall{}Y:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}.  \mforall{}x:Set\{i:l\}.
    ((\mforall{}b:Set\{i:l\}.  ((b  \mmember{}  B)  {}\mRightarrow{}  set-function\{i:l\}(setimages(b;x);  A.Y  A)))
    {}\mRightarrow{}  (\mforall{}z:Set\{i:l\}
                ((z  \mmember{}  closure-set(B;Y;x))
                \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:
((UnivCD  THENA  Auto)
  THEN  Unfold  `closure-set`  0
  THEN  (RW  (AddrC  [1]  SetMemC)  0  THENA  (Auto  THEN  D  0  THEN  Auto)))

---

Home Index