---

Step * 3 1 2 2 1 1 1 1 of Lemma setmem-setimages-2


1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
5. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
6. seteq(A;set-image(f;b))
7. (A ⊆ x)
8. z : coSet{i:l}
9. pr : coSet{i:l}
10. x1 : coSet{i:l}
11. p1 : (x1 ∈ b)
12. seteq(pr;(fst(<x1, p1>),f <x1, p1>))
13. seteq(z;snd(pr))
14. v : coSet{i:l}
15. (f <x1, p1>) = v ∈ coSet{i:l}
⊢ seteq(snd((x1,v));v)
BY
{ (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  :  (z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
5.  \mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
6.  seteq(A;set-image(f;b))
7.  (A  \msubseteq{}  x)
8.  z  :  coSet\{i:l\}
9.  pr  :  coSet\{i:l\}
10.  x1  :  coSet\{i:l\}
11.  p1  :  (x1  \mmember{}  b)
12.  seteq(pr;(fst(<x1,  p1>),f  <x1,  p1>))
13.  seteq(z;snd(pr))
14.  v  :  coSet\{i:l\}
15.  (f  <x1,  p1>)  =  v
\mvdash{}  seteq(snd((x1,v));v)


By

---

Latex:
(RWO  "snd-orderedpairset"  0  THEN  Auto)

---

Home Index