---

Step * of Lemma setmem-fun-graph

∀b:coSet{i:l}. ∀f:(x:coSet{i:l} × (x ∈ b)) ⟶ coSet{i:l}.
  ((∀z1,z2:x:coSet{i:l} × (x ∈ b).  (seteq(fst(z1);fst(z2)) ⇒ seteq(f z1;f z2)))
  ⇒ (∀y:coSet{i:l}. ((y ∈ fun-graph(b;f)) ⇐⇒ ∃p:x:coSet{i:l} × (x ∈ b). seteq(y;(fst(p),f p)))))
BY
{ ((Intros THEN Auto) THEN ExRepD) }

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

2
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))

---

Latex:

---

Latex:
\mforall{}b:coSet\{i:l\}.  \mforall{}f:(x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b))  {}\mrightarrow{}  coSet\{i:l\}.
    ((\mforall{}z1,z2:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).    (seteq(fst(z1);fst(z2))  {}\mRightarrow{}  seteq(f  z1;f  z2)))
    {}\mRightarrow{}  (\mforall{}y:coSet\{i:l\}.  ((y  \mmember{}  fun-graph(b;f))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}p:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).  seteq(y;(fst(p),f  p)))))


By

---

Latex:
((Intros  THEN  Auto)  THEN  ExRepD)

---

Home Index