---

Step * 1 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. seteq(x;imageset(B;f))
7. function-graph{i:l}(A;_.B;f)
8. z : coSet{i:l}
9. (z ∈ x)
⊢ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr)))
BY
{ ((RWO "6" (-1) THEN Auto) THEN RWO "setmem-imageset" (-1) THEN Auto) }

---

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.  seteq(x;imageset(B;f))
7.  function-graph\{i:l\}(A;$_{}$.B;f)
8.  z  :  coSet\{i:l\}
9.  (z  \mmember{}  x)
\mvdash{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr)))


By

---

Latex:
((RWO  "6"  (-1)  THEN  Auto)  THEN  RWO  "setmem-imageset"  (-1)  THEN  Auto)

---

Home Index