---

Step * 3 of Lemma setmem-setimages


1. A : coSet{i:l}
2. B : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. function-graph{i:l}(A;_.B;f)
6. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
7. function-graph{i:l}(A;_.B;f)
⊢ seteq(x;imageset(B;f))
BY
{ (ProveSetEq1 THEN Auto) }

1
1. A : coSet{i:l}
2. B : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. function-graph{i:l}(A;_.B;f)
6. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
7. function-graph{i:l}(A;_.B;f)
8. z : coSet{i:l}
9. (z ∈ x)
⊢ (z ∈ B)

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  B  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  coSet\{i:l\}
5.  function-graph\{i:l\}(A;$_{}$.B;f)
6.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr))))
7.  function-graph\{i:l\}(A;$_{}$.B;f)
\mvdash{}  seteq(x;imageset(B;f))


By

---

Latex:
(ProveSetEq1  THEN  Auto)

---

Home Index