---

Step * 2 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. ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr)))
⊢ (z ∈ B)
BY
{ (ExRepD THEN (RWO "-1" 0 THENA 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. seteq(x;imageset(B;f))
7. function-graph{i:l}(A;_.B;f)
8. z : coSet{i:l}
9. pr : coSet{i:l}
10. (pr ∈ f)
11. seteq(z;snd(pr))
⊢ (snd(pr) ∈ 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.  seteq(x;imageset(B;f))
7.  function-graph\{i:l\}(A;$_{}$.B;f)
8.  z  :  coSet\{i:l\}
9.  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr)))
\mvdash{}  (z  \mmember{}  B)


By

---

Latex:
(ExRepD  THEN  (RWO  "-1"  0  THENA  Auto))

---

Home Index