---

Step * 3 of Lemma function-graph-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. 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)
BY
{ ((RWO "setmem-fun-graph" (-2) THENA Auto)
   THEN (RWO "setmem-fun-graph" (-1) THENA Auto)
   THEN ExRepD
   THEN (RWO "seteq-orderedpairs-iff" (-3) THENA Auto)
   THEN RWO "seteq-orderedpairs-iff" (-1)
   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)
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. p1 : x:coSet{i:l} × (x ∈ b)
15. seteq(_;fst(p1))
16. seteq(b1;f p1)
17. p : x:coSet{i:l} × (x ∈ b)
18. seteq(_;fst(p))
19. seteq(b2;f p)
⊢ seteq(b1;b2)

---

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.  x  :  coSet\{i:l\}
5.  (set-image(f;b)  \msubseteq{}  x)
6.  \mforall{}p:x:coSet\{i:l\}  \mtimes{}  (x  \mmember{}  b).  (f  p  \mmember{}  x)
7.  \mforall{}$_{}$:coSet\{i:l\}.  (($_{}$  \mmember{}  b)  {}\mRightarrow{}  (\mexists{}b@0:coSet\{i:l\}.  ((b@\000C0  \mmember{}  x)  \mwedge{}  (($_{}$,b@0)  \mmember{}  fun-graph(b;f)))))
8.  $_{}$  :  coSet\{i:l\}
9.  b1  :  coSet\{i:l\}
10.  b2  :  coSet\{i:l\}
11.  ($_{}$  \mmember{}  b)
12.  (b1  \mmember{}  x)
13.  (b2  \mmember{}  x)
14.  (($_{}$,b1)  \mmember{}  fun-graph(b;f))
15.  (($_{}$,b2)  \mmember{}  fun-graph(b;f))
\mvdash{}  seteq(b1;b2)


By

---

Latex:
((RWO  "setmem-fun-graph"  (-2)  THENA  Auto)
  THEN  (RWO  "setmem-fun-graph"  (-1)  THENA  Auto)
  THEN  ExRepD
  THEN  (RWO  "seteq-orderedpairs-iff"  (-3)  THENA  Auto)
  THEN  RWO  "seteq-orderedpairs-iff"  (-1)
  THEN  Auto)

---

Home Index