---

Step * 1 2 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))
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))))
BY
{ ((FHyp 5 [-1] THENA Auto) THEN RepeatFor 2 (ParallelLast)) }

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. A : Set{i:l}
9. (A ⊆ x)
10. (z ∈ Y A)
11. b : Set{i:l}
12. (b ∈ B)
13. setimage{i:l}(A;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))
8.  A  :  Set\{i:l\}
9.  (A  \msubseteq{}  x)
10.  (z  \mmember{}  Y  A)
\mvdash{}  \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:
((FHyp  5  [-1]  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast))

---

Home Index