---

Step * 2 of Lemma setmem-image


1. b : coSet{i:l}
2. f : (x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}
3. ∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
4. y : coSet{i:l}
5. x : x:coSet{i:l} × (x ∈ b)
6. seteq(y;f x)
⊢ (y ∈ set-image(f;b))
BY
{ (D -2
   THEN Reduce -1
   THEN (BLemma `setmem-iff`  THENA Auto)
   THEN (coSetD 1 THEN D 1)
   THEN RepUR ``set-image set-dom set-item`` 0) }

1
1. T : Type
2. b1 : T ⟶ coSet{i:l}
3. f : (x:coSet{i:l} × (x ∈ <T, b1>)) ⟶ coSet{i:l}
4. ∀z1,z2:x:coSet{i:l} × (x ∈ <T, b1>).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
5. y : coSet{i:l}
6. x1 : coSet{i:l}
7. x2 : (x1 ∈ <T, b1>)
8. seteq(y;f <x1, x2>)
⊢ ∃t:T. seteq(y;f <b1 t, mem-mk-set(b1;t)>)

---

Latex:

---

Latex:

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


By

---

Latex:
(D  -2
  THEN  Reduce  -1
  THEN  (BLemma  `setmem-iff`    THENA  Auto)
  THEN  (coSetD  1  THEN  D  1)
  THEN  RepUR  ``set-image  set-dom  set-item``  0)

---

Home Index