---

Step * 2 1 1 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. ∀x:coSet{i:l}. ((x ∈ f) ⇒ (x ∈ Σ_:A.B))
6. (∀_:coSet{i:l}. ((_ ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B) ∧ ((_,b) ∈ f)))))
∧ (∀_,b1,b2:coSet{i:l}.  ((_ ∈ A) ⇒ (b1 ∈ B) ⇒ (b2 ∈ B) ⇒ ((_,b1) ∈ f) ⇒ ((_,b2) ∈ f) ⇒ seteq(b1;b2)))
7. seteq(x;imageset(B;f))
8. function-graph{i:l}(A;_.B;f)
9. z : coSet{i:l}
10. pr : coSet{i:l}
11. (pr ∈ f)
12. seteq(z;snd(pr))
13. (pr ∈ Σ_:A.B)
⊢ (snd(pr) ∈ B)
BY
{ ((RWO "setmem-sigmaset" (-1) THENA Auto)
   THEN ExRepD
   THEN (RWO  "-1" 0 THENA Auto)
   THEN RWO  "snd-orderedpairset" 0
   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.  \mforall{}x:coSet\{i:l\}.  ((x  \mmember{}  f)  {}\mRightarrow{}  (x  \mmember{}  \mSigma{}$_{}$:A.B))
6.  (\mforall{}$_{}$:coSet\{i:l\}.  (($_{}$  \mmember{}  A)  {}\mRightarrow{}  (\mexists{}b:coSet\{i:l\}.  ((b  \mmember{}\000C  B)  \mwedge{}  (($_{}$,b)  \mmember{}  f)))))
\mwedge{}  (\mforall{}$_{}$,b1,b2:coSet\{i:l\}.
          (($_{}$  \mmember{}  A)  {}\mRightarrow{}  (b1  \mmember{}  B)  {}\mRightarrow{}  (b2  \mmember{}  B)  {}\mRightarrow{}  (($_{}$,b1)  \mmember{}  f\000C)  {}\mRightarrow{}  (($_{}$,b2)  \mmember{}  f)  {}\mRightarrow{}  seteq(b1;b2)))
7.  seteq(x;imageset(B;f))
8.  function-graph\{i:l\}(A;$_{}$.B;f)
9.  z  :  coSet\{i:l\}
10.  pr  :  coSet\{i:l\}
11.  (pr  \mmember{}  f)
12.  seteq(z;snd(pr))
13.  (pr  \mmember{}  \mSigma{}$_{}$:A.B)
\mvdash{}  (snd(pr)  \mmember{}  B)


By

---

Latex:
((RWO  "setmem-sigmaset"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO    "-1"  0  THENA  Auto)
  THEN  RWO    "snd-orderedpairset"  0
  THEN  Auto)

---

Home Index