---

Step * of Lemma function-graph-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)))
  ⇒ (∀x:coSet{i:l}. ((set-image(f;b) ⊆ x) ⇒ function-graph{i:l}(b;_.x;fun-graph(b;f)))))
BY
{ (Auto
   THEN (Assert ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x) BY
               ((RWO "setsubset-iff" (-1) THENA Auto) THEN RWO "setmem-image" (-1) THEN Auto))
   THEN D 0
   THEN Auto) }

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. x : coSet{i:l}
5. (set-image(f;b) ⊆ x)
6. ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x)
⊢ (fun-graph(b;f) ⊆ Σ_:b.x)

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. x : coSet{i:l}
5. (set-image(f;b) ⊆ x)
6. ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x)
7. _ : coSet{i:l}
8. (_ ∈ b)
⊢ ∃b@0:coSet{i:l}. ((b@0 ∈ x) ∧ ((_,b@0) ∈ fun-graph(b;f)))

3
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. x : coSet{i:l}
5. (set-image(f;b) ⊆ x)
6. ∀p:x:coSet{i:l} × (x ∈ b). (f p ∈ x)
7. ∀_:coSet{i:l}. ((_ ∈ b) ⇒ (∃b@0:coSet{i:l}. ((b@0 ∈ x) ∧ ((_,b@0) ∈ fun-graph(b;f)))))
8. _ : coSet{i:l}
9. b1 : coSet{i:l}
10. b2 : coSet{i:l}
11. (_ ∈ b)
12. (b1 ∈ x)
13. (b2 ∈ x)
14. ((_,b1) ∈ fun-graph(b;f))
15. ((_,b2) ∈ fun-graph(b;f))
⊢ seteq(b1;b2)

---

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{}x:coSet\{i:l\}.  ((set-image(f;b)  \msubseteq{}  x)  {}\mRightarrow{}  function-graph\{i:l\}(b;$_{}$.x;fun-\000Cgraph(b;f)))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}p:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).  (f  p  \mmember{}  x)  BY
                          ((RWO  "setsubset-iff"  (-1)  THENA  Auto)  THEN  RWO  "setmem-image"  (-1)  THEN  Auto))
  THEN  D  0
  THEN  Auto)

---

Home Index