---

Step * of Lemma setmem-setimages

∀A,B,x:coSet{i:l}.
  ((x ∈ setimages(A;B))
  ⇐⇒ ∃f:coSet{i:l}
       (function-graph{i:l}(A;_.B;f) ∧ (∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr)))))))
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `setimages` 0
   THEN (RWO  "setmem-setunionfun" 0 THENA Auto)
   THEN (RWO "setmem-funset setmem-singleset" 0 THENA Auto)
   THEN Auto
   THEN ParallelLast
   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. 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)))

2
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 ∈ x)

3
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))

---

Latex:

---

Latex:
\mforall{}A,B,x:coSet\{i:l\}.
    ((x  \mmember{}  setimages(A;B))
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}f:coSet\{i:l\}
              (function-graph\{i:l\}(A;$_{}$.B;f)
              \mwedge{}  (\mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr)))))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `setimages`  0
  THEN  (RWO    "setmem-setunionfun"  0  THENA  Auto)
  THEN  (RWO  "setmem-funset  setmem-singleset"  0  THENA  Auto)
  THEN  Auto
  THEN  ParallelLast
  THEN  Auto)

---

Home Index