---

Step * 1 of Lemma closure-set-property


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))
BY
{ (RWO "setmem-closure-set" 0 THEN Auto THEN ExRepD) }

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))
8. b : coSet{i:l}
9. (b ∈ B)
10. A : coSet{i:l}
11. (A ∈ setimages(b;x))
12. (z ∈ Y A)
⊢ ∃A:Set{i:l}. ((A ⊆ x) ∧ (z ∈ Y A))

2
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))
8. A : Set{i:l}
9. (A ⊆ x)
10. (z ∈ Y A)
⊢ ∃b:coSet{i:l}. ((b ∈ B) ∧ (∃A:coSet{i:l}. ((A ∈ setimages(b;x)) ∧ (z ∈ Y A))))

---

Latex:

---

Latex:

1.  B  :  Set\{i:l\}
2.  x  :  Set\{i:l\}
3.  Y  :  x1:Set\{i:l\}  {}\mrightarrow{}  Set\{i:l\}
4.  \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))
5.  \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))))
6.  z  :  Set\{i:l\}
7.  \mforall{}b:Set\{i:l\}.  ((b  \mmember{}  B)  {}\mRightarrow{}  set-function\{i:l\}(setimages(b;x);  A.Y  A))
\mvdash{}  (z  \mmember{}  closure-set(B;Y;x))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}A:Set\{i:l\}.  ((A  \msubseteq{}  x)  \mwedge{}  (z  \mmember{}  Y  A))


By

---

Latex:
(RWO  "setmem-closure-set"  0  THEN  Auto  THEN  ExRepD)

---

Home Index