---

Step * of Lemma setmem-imageset

∀B,f,x:coSet{i:l}.  ((x ∈ imageset(B;f)) ⇐⇒ (x ∈ B) ∧ (∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(x;snd(pr)))))
BY
{ ((UnivCD THENA Auto) THEN Unfold `imageset` 0 THEN (RWO  "setmem-sub-coset" 0 THENA Auto)) }

1
1. B : coSet{i:l}
2. f : coSet{i:l}
3. x : coSet{i:l}
⊢ (x ∈ B) ∧ ∃pr∈f.seteq(x;snd(pr)) ⇐⇒ (x ∈ B) ∧ (∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(x;snd(pr))))

---

Latex:

---

Latex:
\mforall{}B,f,x:coSet\{i:l\}.
    ((x  \mmember{}  imageset(B;f))  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  B)  \mwedge{}  (\mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(x;snd(pr)))))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Unfold  `imageset`  0  THEN  (RWO    "setmem-sub-coset"  0  THENA  Auto))

---

Home Index