---

Step * of Lemma closure-set-property

∀B,x:Set{i:l}. ∀Y:x1:Set{i:l} ⟶ Set{i:l}.
  ((∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ (a1 ∈ Y x1) ⇒ (a2 ∈ Y x2)))
  ⇒ (∀x,a:Set{i:l}.  ((a ∈ Y x) ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b)))))
  ⇒ (∀z:Set{i:l}. ((z ∈ closure-set(B;Y;x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ (z ∈ Y A)))))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ∀b:Set{i:l}. ((b ∈ B) ⇒ set-function{i:l}(setimages(b;x); A.Y A)) BY
               ((Auto THEN D 0)
                THEN Auto
                THEN ((RWO "seteq-iff" 0 THENM D 0) THENA Auto)
                THEN (Assert seteq(x1;x1) ∧ seteq(y;A) BY
                            Auto)
                THEN Auto))
   ) }

1
1. B : Set{i:l}
2. x : Set{i:l}
3. Y : x1:Set{i:l} ⟶ Set{i:l}
4. ∀x1,x2,a1,a2:Set{i:l}.  (seteq(x1;x2) ⇒ seteq(a1;a2) ⇒ (a1 ∈ Y x1) ⇒ (a2 ∈ Y x2))
5. ∀x,a:Set{i:l}.  ((a ∈ Y x) ⇒ (∃b:Set{i:l}. ((b ∈ B) ∧ setimage{i:l}(x;b))))
6. z : Set{i:l}
7. ∀b:Set{i:l}. ((b ∈ B) ⇒ set-function{i:l}(setimages(b;x); A.Y A))
⊢ (z ∈ closure-set(B;Y;x)) ⇐⇒ ∃A:Set{i:l}. ((A ⊆ x) ∧ (z ∈ Y A))

---

Latex:

---

Latex:
\mforall{}B,x:Set\{i:l\}.  \mforall{}Y:x1:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}.
    ((\mforall{}x1,x2,a1,a2:Set\{i:l\}.    (seteq(x1;x2)  {}\mRightarrow{}  seteq(a1;a2)  {}\mRightarrow{}  (a1  \mmember{}  Y  x1)  {}\mRightarrow{}  (a2  \mmember{}  Y  x2)))
    {}\mRightarrow{}  (\mforall{}x,a:Set\{i:l\}.    ((a  \mmember{}  Y  x)  {}\mRightarrow{}  (\mexists{}b:Set\{i:l\}.  ((b  \mmember{}  B)  \mwedge{}  setimage\{i:l\}(x;b)))))
    {}\mRightarrow{}  (\mforall{}z:Set\{i:l\}.  ((z  \mmember{}  closure-set(B;Y;x))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  (z  \mmember{}  Y  A)))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mforall{}b:Set\{i:l\}.  ((b  \mmember{}  B)  {}\mRightarrow{}  set-function\{i:l\}(setimages(b;x);  A.Y  A))  BY
                          ((Auto  THEN  D  0)
                            THEN  Auto
                            THEN  ((RWO  "seteq-iff"  0  THENM  D  0)  THENA  Auto)
                            THEN  (Assert  seteq(x1;x1)  \mwedge{}  seteq(y;A)  BY
                                                    Auto)
                            THEN  Auto))
  )

---

Home Index