---

Step * 2 of Lemma setimage-iff


1. x : coSet{i:l}
2. b : coSet{i:l}
3. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
4. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
5. seteq(x;set-image(f;b))
⊢ ∀y:coSet{i:l}. ((y ∈ x) ⇐⇒ ∃z:z:coSet{i:l} × (z ∈ b). seteq(y;f z))
BY
{ ((RWO "-1" 0 THENA Auto) THEN RWO "setmem-image" 0 THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  f  :  (z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
4.  \mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
5.  seteq(x;set-image(f;b))
\mvdash{}  \mforall{}y:coSet\{i:l\}.  ((y  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}z:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).  seteq(y;f  z))


By

---

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

---

Home Index