---

Step * of Lemma setimage-iff

∀x,b:coSet{i:l}.
  (setimage{i:l}(x;b)
  ⇐⇒ ∃f:(z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
       ((∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))) ∧ seteq(x;set-image(f;b))))
BY
{ (Auto THEN All (Unfold `setimage`) THEN RepeatFor 2 (ParallelLast)) }

1
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. ∀y:coSet{i:l}. ((y ∈ x) ⇐⇒ ∃z:z:coSet{i:l} × (z ∈ b). seteq(y;f z))
⊢ seteq(x;set-image(f;b))

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

---

Latex:

---

Latex:
\mforall{}x,b:coSet\{i:l\}.
    (setimage\{i:l\}(x;b)
    \mLeftarrow{}{}\mRightarrow{}  \mexists{}f:(z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
              ((\mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2)))
              \mwedge{}  seteq(x;set-image(f;b))))


By

---

Latex:
(Auto  THEN  All  (Unfold  `setimage`)  THEN  RepeatFor  2  (ParallelLast))

---

Home Index