The abstract of the Mizar article:

Graphs of Functions

by

Czeslaw Bylinski

Received April 14, 1989

MML identifier: GRFUNC_1

[ Mizar article, MML identifier index ]

environ

 vocabulary FUNCT_1, RELAT_1, BOOLE;
 notation TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
 constructors TARSKI, SUBSET_1, FUNCT_1, XBOOLE_0;
 clusters FUNCT_1, XBOOLE_0, ZFMISC_1;
 requirements SUBSET, BOOLE;


begin

 reserve X,Y,p,x,x1,x2,y,y1,y2,z,z1,z2 for set;
 reserve f,g,h for Function;

canceled 5;

theorem :: GRFUNC_1:6
   for G being set st G c= f holds G is Function;

canceled;

theorem :: GRFUNC_1:8
     f c= g iff
     dom f c= dom g & (for x st x in dom f holds f.x = g.x);

theorem :: GRFUNC_1:9
     dom f = dom g & f c= g implies f = g;

canceled 2;

theorem :: GRFUNC_1:12
     [x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g;

theorem :: GRFUNC_1:13
     h c= f implies g*h c= g*f & h*g c= f*g;

canceled;

theorem :: GRFUNC_1:15
   {[x,y]} is Function;

theorem :: GRFUNC_1:16
     f = {[x,y]} implies f.x = y;

canceled;

theorem :: GRFUNC_1:18
     dom f = {x} implies f = {[x,f.x]};

theorem :: GRFUNC_1:19
     {[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2);

canceled 5;

theorem :: GRFUNC_1:25
   f is one-to-one iff
       for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2;

theorem :: GRFUNC_1:26
   g c= f & f is one-to-one implies g is one-to-one;

theorem :: GRFUNC_1:27
   f /\ X is Function & X /\ f is Function;

theorem :: GRFUNC_1:28
     h = f /\ g
     implies dom h c= dom f /\ dom g & rng h c= rng f /\ rng g;

theorem :: GRFUNC_1:29
     h = f /\ g & x in dom h implies h.x = f.x & h.x = g.x;

theorem :: GRFUNC_1:30
     (f is one-to-one or g is one-to-one) & h = f /\ g
    implies h is one-to-one;

theorem :: GRFUNC_1:31
     dom f misses dom g implies f \/ g is Function;

theorem :: GRFUNC_1:32
     f c= h & g c= h implies f \/ g is Function;

theorem :: GRFUNC_1:33
     h = f \/ g implies dom h = dom f \/ dom g & rng h = rng f \/ rng g;

theorem :: GRFUNC_1:34
   x in dom f & h = f \/ g implies h.x = f.x;

theorem :: GRFUNC_1:35
     x in dom g & h = f \/ g implies h.x = g.x;

theorem :: GRFUNC_1:36
     x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x;

theorem :: GRFUNC_1:37
     f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g
    implies h is one-to-one;

theorem :: GRFUNC_1:38
     f \ X is Function;

canceled 7;

theorem :: GRFUNC_1:46
   f = {} implies f is one-to-one;

theorem :: GRFUNC_1:47
     f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f;

canceled;

theorem :: GRFUNC_1:49
     f = {} implies f" = {};

canceled 2;

theorem :: GRFUNC_1:52
     x in dom f & x in X iff [x,f.x] in f|X;

canceled;

theorem :: GRFUNC_1:54
     ((f|X)*h) c= (f*h) & (g*(f|X)) c= (g*f);

canceled 9;

theorem :: GRFUNC_1:64
     g c= f implies f|dom g = g;

canceled 2;

theorem :: GRFUNC_1:67
     x in dom f & f.x in Y iff [x,f.x] in Y|f;

canceled;

theorem :: GRFUNC_1:69
     ((Y|f)*h) c= (f*h) & (g*(Y|f)) c= (g*f);

canceled 9;

theorem :: GRFUNC_1:79
     g c= f & f is one-to-one implies rng g|f = g;

canceled 7;

theorem :: GRFUNC_1:87
     x in f"Y iff [x,f.x] in f & f.x in Y;