---

Step * 1 of Lemma setimages_functionality


1. b1 : coSet{i:l}
2. b2 : coSet{i:l}
3. x1 : coSet{i:l}
4. x2 : coSet{i:l}
5. seteq(b1;b2)
6. seteq(x1;x2)
7. z : coSet{i:l}
8. ∀z:coSet{i:l}. ((z ∈ b1) ⇐⇒ (z ∈ b2))
⊢ (z ∈ setimages(b1;x1)) ⇐⇒ (z ∈ setimages(b2;x2))
BY
{ ((RWO "setmem-setimages-2" 0 THENA Auto)
   THEN RWO "-3" 0
   THEN Auto
   THEN (RWO "setimage-iff" (-2) THENA Auto)
   THEN (RWO "setimage-iff" 0 THENA Auto)
   THEN ExRepD) }

1
1. b1 : coSet{i:l}
2. b2 : coSet{i:l}
3. x1 : coSet{i:l}
4. x2 : coSet{i:l}
5. seteq(b1;b2)
6. seteq(x1;x2)
7. z : coSet{i:l}
8. ∀z:coSet{i:l}. ((z ∈ b1) ⇐⇒ (z ∈ b2))
9. f : (z:coSet{i:l} × (z ∈ b1)) ⟶ coSet{i:l}
10. ∀z1,z2:z:coSet{i:l} × (z ∈ b1).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
11. seteq(z;set-image(f;b1))
12. (z ⊆ x2)
⊢ ∃f:(z:coSet{i:l} × (z ∈ b2)) ⟶ coSet{i:l}
   ((∀z1,z2:z:coSet{i:l} × (z ∈ b2).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))) ∧ seteq(z;set-image(f;b2)))

2
1. b1 : coSet{i:l}
2. b2 : coSet{i:l}
3. x1 : coSet{i:l}
4. x2 : coSet{i:l}
5. seteq(b1;b2)
6. seteq(x1;x2)
7. z : coSet{i:l}
8. ∀z:coSet{i:l}. ((z ∈ b1) ⇐⇒ (z ∈ b2))
9. f : (z:coSet{i:l} × (z ∈ b2)) ⟶ coSet{i:l}
10. ∀z1,z2:z:coSet{i:l} × (z ∈ b2).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
11. seteq(z;set-image(f;b2))
12. (z ⊆ x2)
⊢ ∃f:(z:coSet{i:l} × (z ∈ b1)) ⟶ coSet{i:l}
   ((∀z1,z2:z:coSet{i:l} × (z ∈ b1).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))) ∧ seteq(z;set-image(f;b1)))

---

Latex:

---

Latex:

1.  b1  :  coSet\{i:l\}
2.  b2  :  coSet\{i:l\}
3.  x1  :  coSet\{i:l\}
4.  x2  :  coSet\{i:l\}
5.  seteq(b1;b2)
6.  seteq(x1;x2)
7.  z  :  coSet\{i:l\}
8.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  b1)  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  b2))
\mvdash{}  (z  \mmember{}  setimages(b1;x1))  \mLeftarrow{}{}\mRightarrow{}  (z  \mmember{}  setimages(b2;x2))


By

---

Latex:
((RWO  "setmem-setimages-2"  0  THENA  Auto)
  THEN  RWO  "-3"  0
  THEN  Auto
  THEN  (RWO  "setimage-iff"  (-2)  THENA  Auto)
  THEN  (RWO  "setimage-iff"  0  THENA  Auto)
  THEN  ExRepD)

---

Home Index