---

Step * 2 of Lemma setmem-fun-graph


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. p : x:coSet{i:l} × (x ∈ b)
6. seteq(y;(fst(p),f p))
⊢ (y ∈ fun-graph(b;f))
BY
{ (D -2 THEN Reduce -1) }

1
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 : coSet{i:l}
6. p1 : (x ∈ b)
7. seteq(y;(x,f <x, p1>))
⊢ (y ∈ fun-graph(b;f))

---

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.  p  :  x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b)
6.  seteq(y;(fst(p),f  p))
\mvdash{}  (y  \mmember{}  fun-graph(b;f))


By

---

Latex:
(D  -2  THEN  Reduce  -1)

---

Home Index