---

Step * 3 1 2 of Lemma setmem-setimages-2


1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
5. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
6. seteq(A;set-image(f;b))
7. (A ⊆ x)
⊢ ∀z:coSet{i:l}. ((z ∈ A) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ fun-graph(b;f)) ∧ seteq(z;snd(pr))))
BY
{ ((D 0 THENA Auto) THEN (RWO "-3" 0 THENA Auto) THEN RWO "setmem-image setmem-fun-graph" 0 THEN Auto THEN ExRepD) }

1
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
5. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
6. seteq(A;set-image(f;b))
7. (A ⊆ x)
8. z : coSet{i:l}
9. x1 : x:coSet{i:l} × (x ∈ b)
10. seteq(z;f x1)
⊢ ∃pr:coSet{i:l}. ((∃p:x:coSet{i:l} × (x ∈ b). seteq(pr;(fst(p),f p))) ∧ seteq(z;snd(pr)))

2
1. A : coSet{i:l}
2. b : coSet{i:l}
3. x : coSet{i:l}
4. f : (z:coSet{i:l} × (z ∈ b)) ⟶ coSet{i:l}
5. ∀z1,z2:z:coSet{i:l} × (z ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2))
6. seteq(A;set-image(f;b))
7. (A ⊆ x)
8. z : coSet{i:l}
9. pr : coSet{i:l}
10. p : x:coSet{i:l} × (x ∈ b)
11. seteq(pr;(fst(p),f p))
12. seteq(z;snd(pr))
⊢ ∃x:x:coSet{i:l} × (x ∈ b). seteq(z;f x)

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  b  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  (z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}
5.  \mforall{}z1,z2:z:coSet\{i:l\}  \mtimes{}  (z  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2))
6.  seteq(A;set-image(f;b))
7.  (A  \msubseteq{}  x)
\mvdash{}  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  A)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  fun-graph(b;f))  \mwedge{}  seteq(z;snd(pr))))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  (RWO  "-3"  0  THENA  Auto)
  THEN  RWO  "setmem-image  setmem-fun-graph"  0
  THEN  Auto
  THEN  ExRepD)

---

Home Index