---

Step * 3 1 1 of Lemma setmem-setimages


1. A : coSet{i:l}
2. B : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. function-graph{i:l}(A;_.B;f)
6. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
7. function-graph{i:l}(A;_.B;f)
8. z : coSet{i:l}
9. pr : coSet{i:l}
10. (pr ∈ f)
11. seteq(z;snd(pr))
⊢ (snd(pr) ∈ B)
BY
{ (D 5 THEN (RWO "setsubset-iff" 5 THENA Auto) THEN (FHyp 5 [-2] THENA Auto)) }

1
1. A : coSet{i:l}
2. B : coSet{i:l}
3. x : coSet{i:l}
4. f : coSet{i:l}
5. ∀x:coSet{i:l}. ((x ∈ f) ⇒ (x ∈ Σ_:A.B))
6. (∀_:coSet{i:l}. ((_ ∈ A) ⇒ (∃b:coSet{i:l}. ((b ∈ B) ∧ ((_,b) ∈ f)))))
∧ (∀_,b1,b2:coSet{i:l}.  ((_ ∈ A) ⇒ (b1 ∈ B) ⇒ (b2 ∈ B) ⇒ ((_,b1) ∈ f) ⇒ ((_,b2) ∈ f) ⇒ seteq(b1;b2)))
7. ∀z:coSet{i:l}. ((z ∈ x) ⇐⇒ ∃pr:coSet{i:l}. ((pr ∈ f) ∧ seteq(z;snd(pr))))
8. function-graph{i:l}(A;_.B;f)
9. z : coSet{i:l}
10. pr : coSet{i:l}
11. (pr ∈ f)
12. seteq(z;snd(pr))
13. (pr ∈ Σ_:A.B)
⊢ (snd(pr) ∈ B)

---

Latex:

---

Latex:

1.  A  :  coSet\{i:l\}
2.  B  :  coSet\{i:l\}
3.  x  :  coSet\{i:l\}
4.  f  :  coSet\{i:l\}
5.  function-graph\{i:l\}(A;$_{}$.B;f)
6.  \mforall{}z:coSet\{i:l\}.  ((z  \mmember{}  x)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}pr:coSet\{i:l\}.  ((pr  \mmember{}  f)  \mwedge{}  seteq(z;snd(pr))))
7.  function-graph\{i:l\}(A;$_{}$.B;f)
8.  z  :  coSet\{i:l\}
9.  pr  :  coSet\{i:l\}
10.  (pr  \mmember{}  f)
11.  seteq(z;snd(pr))
\mvdash{}  (snd(pr)  \mmember{}  B)


By

---

Latex:
(D  5  THEN  (RWO  "setsubset-iff"  5  THENA  Auto)  THEN  (FHyp  5  [-2]  THENA  Auto))

---

Home Index