grfunc_1.miz

    begin

    reserve X,Y for set,

p,x,x1,x2,y,y1,y2,z,z1,z2 for object;

    reserve f,g,h for Function;

    theorem :: GRFUNC_1:1



     Th1: for G be set st G c= f holds G is Function;

    theorem :: GRFUNC_1:2



     Th2: f c= g iff ( dom f) c= ( dom g) & for x be object st x in ( dom f) holds (f . x) = (g . x)

    proof

      thus f c= g implies ( dom f) c= ( dom g) & for x be object st x in ( dom f) holds (f . x) = (g . x)

      proof

        assume

         A1: f c= g;

        hence ( dom f) c= ( dom g) by RELAT_1: 11;

        let x be object;

        assume x in ( dom f);

        then [x, (f . x)] in f by FUNCT_1:def 2;

        hence thesis by A1, FUNCT_1: 1;

      end;

      assume that

       A2: ( dom f) c= ( dom g) and

       A3: for x be object st x in ( dom f) holds (f . x) = (g . x);

      let x,y be object;

      assume

       A4: [x, y] in f;

      then

       A5: x in ( dom f) by FUNCT_1: 1;

      y = (f . x) by A4, FUNCT_1: 1;

      then y = (g . x) by A3, A5;

      hence thesis by A2, A5, FUNCT_1:def 2;

    end;

    theorem :: GRFUNC_1:3

    ( dom f) = ( dom g) & f c= g implies f = g

    proof

      assume that

       A1: ( dom f) = ( dom g) and

       A2: f c= g;

      for x,y be object holds [x, y] in f iff [x, y] in g

      proof

        let x,y be object;

        thus [x, y] in f implies [x, y] in g by A2;

        assume

         A3: [x, y] in g;

        then x in ( dom f) by A1, XTUPLE_0:def 12;

        then [x, (f . x)] in f by FUNCT_1: 1;

        hence thesis by A2, A3, FUNCT_1:def 1;

      end;

      hence thesis;

    end;



     Lm1: (( rng f) /\ ( rng h)) = {} & x in ( dom f) & y in ( dom h) implies (f . x) <> (h . y)

    proof

      assume

       A1: (( rng f) /\ ( rng h)) = {} ;

      assume x in ( dom f) & y in ( dom h);

      then (f . x) in ( rng f) & (h . y) in ( rng h) by FUNCT_1:def 3;

      hence thesis by A1, XBOOLE_0:def 4;

    end;

    theorem :: GRFUNC_1:4

     [x, z] in (g * f) implies [x, (f . x)] in f & [(f . x), z] in g

    proof

      assume [x, z] in (g * f);

      then ex y be object st [x, y] in f & [y, z] in g by RELAT_1:def 8;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:5

     { [x, y]} is Function;



     Lm2: [x, y] in { [x1, y1]} implies x = x1 & y = y1

    proof

      assume [x, y] in { [x1, y1]};

      then [x, y] = [x1, y1] by TARSKI:def 1;

      hence thesis by XTUPLE_0: 1;

    end;

    theorem :: GRFUNC_1:6

    f = { [x, y]} implies (f . x) = y

    proof

      assume f = { [x, y]};

      then [x, y] in f by TARSKI:def 1;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:7



     Th7: ( dom f) = {x} implies f = { [x, (f . x)]}

    proof

      reconsider g = { [x, (f . x)]} as Function;

      assume

       A1: ( dom f) = {x};

      for y,z be object holds [y, z] in f iff [y, z] in g

      proof

        let y,z be object;

        thus [y, z] in f implies [y, z] in g

        proof

          assume

           A2: [y, z] in f;

          then y in {x} by A1, XTUPLE_0:def 12;

          then

           A3: y = x by TARSKI:def 1;



           A4: ( rng f) = {(f . x)} by A1, FUNCT_1: 4;

          z in ( rng f) by A2, XTUPLE_0:def 13;

          then z = (f . x) by A4, TARSKI:def 1;

          hence thesis by A3, TARSKI:def 1;

        end;

        assume [y, z] in g;

        then

         A5: y = x & z = (f . x) by Lm2;

        x in ( dom f) by A1, TARSKI:def 1;

        hence thesis by A5, FUNCT_1:def 2;

      end;

      hence thesis;

    end;

    theorem :: GRFUNC_1:8

     { [x1, y1], [x2, y2]} is Function iff (x1 = x2 implies y1 = y2)

    proof

      thus { [x1, y1], [x2, y2]} is Function & x1 = x2 implies y1 = y2

      proof



         A1: [x1, y1] in { [x1, y1], [x2, y2]} & [x2, y2] in { [x1, y1], [x2, y2]} by TARSKI:def 2;

        assume { [x1, y1], [x2, y2]} is Function;

        hence thesis by A1, FUNCT_1:def 1;

      end;

      assume

       A2: x1 = x2 implies y1 = y2;

      now

        thus p in { [x1, y1], [x2, y2]} implies ex x, y st [x, y] = p

        proof

          assume p in { [x1, y1], [x2, y2]};

          then p = [x1, y1] or p = [x2, y2] by TARSKI:def 2;

          hence thesis;

        end;

        let x, z1, z2;



         A3: [x, z1] = [x1, y1] & [x, z2] = [x1, y1] or [x, z1] = [x2, y2] & [x, z2] = [x2, y2] implies z1 = y1 & z2 = y1 or z1 = y2 & z2 = y2 by XTUPLE_0: 1;

         A4:

        now

          assume

           A5: [x, z1] = [x1, y1] & [x, z2] = [x2, y2] or [x, z1] = [x2, y2] & [x, z2] = [x1, y1];

          then x = x1 & x = x2 by XTUPLE_0: 1;

          hence z1 = z2 by A2, A5, XTUPLE_0: 1;

        end;

        assume [x, z1] in { [x1, y1], [x2, y2]} & [x, z2] in { [x1, y1], [x2, y2]};

        hence z1 = z2 by A3, A4, TARSKI:def 2;

      end;

      hence thesis by FUNCT_1:def 1;

    end;

    theorem :: GRFUNC_1:9



     Th9: f is one-to-one iff for x1, x2, y st [x1, y] in f & [x2, y] in f holds x1 = x2

    proof

      thus f is one-to-one implies for x1, x2, y st [x1, y] in f & [x2, y] in f holds x1 = x2

      proof

        assume

         A1: f is one-to-one;

        let x1, x2, y;

        assume

         A2: [x1, y] in f & [x2, y] in f;

        then

         A3: (f . x1) = y & (f . x2) = y by FUNCT_1: 1;

        x1 in ( dom f) & x2 in ( dom f) by A2, FUNCT_1: 1;

        hence thesis by A1, A3;

      end;

      assume

       A4: for x1, x2, y st [x1, y] in f & [x2, y] in f holds x1 = x2;

      let x1, x2;

      assume x1 in ( dom f) & x2 in ( dom f) & (f . x1) = (f . x2);

      then [x1, (f . x1)] in f & [x2, (f . x1)] in f by FUNCT_1: 1;

      hence thesis by A4;

    end;

    theorem :: GRFUNC_1:10



     Th10: g c= f & f is one-to-one implies g is one-to-one

    proof

      assume g c= f & f is one-to-one;

      then for x1, x2, y st [x1, y] in g & [x2, y] in g holds x1 = x2 by Th9;

      hence thesis by Th9;

    end;

    registration

      let f, X;

      cluster (f /\ X) -> Function-like;

      coherence by Th1, XBOOLE_1: 17;

    end

    theorem :: GRFUNC_1:11

    x in ( dom (f /\ g)) implies ((f /\ g) . x) = (f . x)

    proof

      set y = ((f /\ g) . x);

      assume x in ( dom (f /\ g));

      then [x, y] in (f /\ g) by FUNCT_1:def 2;

      then [x, y] in f by XBOOLE_0:def 4;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:12

    f is one-to-one implies (f /\ g) is one-to-one by Th10, XBOOLE_1: 17;

    theorem :: GRFUNC_1:13

    ( dom f) misses ( dom g) implies (f \/ g) is Function

    proof

      assume

       A1: (( dom f) /\ ( dom g)) = {} ;

      now

        thus p in (f \/ g) implies ex x,y be object st [x, y] = p by RELAT_1:def 1;

        let x, y1, y2;

        assume [x, y1] in (f \/ g);

        then

         A2: [x, y1] in f or [x, y1] in g by XBOOLE_0:def 3;

        assume [x, y2] in (f \/ g);

        then

         A3: [x, y2] in f or [x, y2] in g by XBOOLE_0:def 3;

         not (x in ( dom f) & x in ( dom g)) by A1, XBOOLE_0:def 4;

        hence y1 = y2 by A2, A3, FUNCT_1:def 1, XTUPLE_0:def 12;

      end;

      hence thesis by FUNCT_1:def 1;

    end;

    theorem :: GRFUNC_1:14

    f c= h & g c= h implies (f \/ g) is Function by Th1, XBOOLE_1: 8;



     Lm3: h = (f \/ g) implies (x in ( dom h) iff x in ( dom f) or x in ( dom g))

    proof

      assume

       A1: h = (f \/ g);

      thus x in ( dom h) implies x in ( dom f) or x in ( dom g)

      proof

        assume x in ( dom h);

        then [x, (h . x)] in h by FUNCT_1:def 2;

        then [x, (h . x)] in f or [x, (h . x)] in g by A1, XBOOLE_0:def 3;

        hence thesis by XTUPLE_0:def 12;

      end;

      assume x in ( dom f) or x in ( dom g);

      then [x, (f . x)] in f or [x, (g . x)] in g by FUNCT_1:def 2;

      then [x, (f . x)] in h or [x, (g . x)] in h by A1, XBOOLE_0:def 3;

      hence thesis by XTUPLE_0:def 12;

    end;

    theorem :: GRFUNC_1:15



     Th15: x in ( dom g) & h = (f \/ g) implies (h . x) = (g . x)

    proof

      assume x in ( dom g);

      then [x, (g . x)] in g by FUNCT_1:def 2;

      then h = (f \/ g) implies [x, (g . x)] in h by XBOOLE_0:def 3;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:16

    x in ( dom h) & h = (f \/ g) implies (h . x) = (f . x) or (h . x) = (g . x)

    proof

      assume x in ( dom h);

      then [x, (h . x)] in h by FUNCT_1:def 2;

      then h = (f \/ g) implies [x, (h . x)] in f or [x, (h . x)] in g by XBOOLE_0:def 3;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:17

    f is one-to-one & g is one-to-one & h = (f \/ g) & ( rng f) misses ( rng g) implies h is one-to-one

    proof

      assume that

       A1: f is one-to-one & g is one-to-one and

       A2: h = (f \/ g) and

       A3: (( rng f) /\ ( rng g)) = {} ;

      now

        let x1, x2;

        assume that

         A4: x1 in ( dom h) & x2 in ( dom h) and

         A5: (h . x1) = (h . x2);

         A6:

        now

          assume x1 in ( dom f) & x2 in ( dom g) or x1 in ( dom g) & x2 in ( dom f);

          then (h . x1) = (f . x1) & (h . x2) = (g . x2) & (f . x1) <> (g . x2) or (h . x1) = (g . x1) & (h . x2) = (f . x2) & (f . x2) <> (g . x1) by A2, A3, Lm1, Th15;

          hence x1 = x2 by A5;

        end;



         A7: x1 in ( dom g) & x2 in ( dom g) implies (h . x1) = (g . x1) & (h . x2) = (g . x2) by A2, Th15;

        x1 in ( dom f) & x2 in ( dom f) implies (h . x1) = (f . x1) & (h . x2) = (f . x2) by A2, Th15;

        then x1 in ( dom f) & x2 in ( dom f) or x1 in ( dom g) & x2 in ( dom g) implies x1 = x2 by A1, A5, A7;

        hence x1 = x2 by A2, A4, A6, Lm3;

      end;

      hence thesis;

    end;

    ::$Canceled

    theorem :: GRFUNC_1:20

    f is one-to-one implies for x, y holds [y, x] in (f " ) iff [x, y] in f

    proof

      assume

       A1: f is one-to-one;

      let x, y;

      ( dom (f " )) = ( rng f) by A1, FUNCT_1: 33;

      then y in ( dom (f " )) & x = ((f " ) . y) iff x in ( dom f) & y = (f . x) by A1, FUNCT_1: 32;

      hence thesis by FUNCT_1: 1;

    end;

    theorem :: GRFUNC_1:21

    f = {} implies (f " ) = {}

    proof

      assume f = {} ;

      then ( dom (f " )) = {} by FUNCT_1: 33, RELAT_1: 38;

      hence thesis;

    end;

    theorem :: GRFUNC_1:22

    x in ( dom f) & x in X iff [x, (f . x)] in (f | X)

    proof

      x in ( dom f) iff [x, (f . x)] in f by FUNCT_1:def 2, XTUPLE_0:def 12;

      hence thesis by RELAT_1:def 11;

    end;

    theorem :: GRFUNC_1:23



     Th21: g c= f implies (f | ( dom g)) = g

    proof

      assume

       A1: g c= f;

      for x,y be object holds [x, y] in (f | ( dom g)) implies [x, y] in g

      proof

        let x,y be object;

        assume

         A2: [x, y] in (f | ( dom g));

        then x in ( dom g) by RELAT_1:def 11;

        then

         A3: [x, (g . x)] in g by FUNCT_1:def 2;

         [x, y] in f by A2, RELAT_1:def 11;

        hence thesis by A1, A3, FUNCT_1:def 1;

      end;

      then

       A4: (f | ( dom g)) c= g;

      (g | ( dom g)) c= (f | ( dom g)) by A1, RELAT_1: 76;

      then g c= (f | ( dom g));

      hence thesis by A4;

    end;

    theorem :: GRFUNC_1:24

    x in ( dom f) & (f . x) in Y iff [x, (f . x)] in (Y |` f)

    proof

      x in ( dom f) iff [x, (f . x)] in f by FUNCT_1:def 2, XTUPLE_0:def 12;

      hence thesis by RELAT_1:def 12;

    end;

    theorem :: GRFUNC_1:25

    g c= f & f is one-to-one implies (( rng g) |` f) = g

    proof

      assume

       A1: g c= f;

      assume

       A2: f is one-to-one;

      for x,y be object holds [x, y] in (( rng g) |` f) implies [x, y] in g

      proof

        let x,y be object;

        assume

         A3: [x, y] in (( rng g) |` f);

        then y in ( rng g) by RELAT_1:def 12;

        then

         A4: ex x1 be object st [x1, y] in g by XTUPLE_0:def 13;

         [x, y] in f by A3, RELAT_1:def 12;

        hence thesis by A1, A2, A4, Th9;

      end;

      then

       A5: (( rng g) |` f) c= g;

      (( rng g) |` g) c= (( rng g) |` f) by A1, RELAT_1: 101;

      then g c= (( rng g) |` f);

      hence thesis by A5;

    end;

    theorem :: GRFUNC_1:26

    x in (f " Y) iff [x, (f . x)] in f & (f . x) in Y

    proof

      thus x in (f " Y) implies [x, (f . x)] in f & (f . x) in Y

      proof

        assume x in (f " Y);

        then ex y be object st [x, y] in f & y in Y by RELAT_1:def 14;

        hence thesis by FUNCT_1: 1;

      end;

      thus thesis by RELAT_1:def 14;

    end;

    begin

    theorem :: GRFUNC_1:27

    for X be set, f,g be Function st X c= ( dom f) & f c= g holds (f | X) = (g | X)

    proof

      let X be set, f,g be Function such that

       A1: X c= ( dom f);

      assume f c= g;



      hence (f | X) = ((g | ( dom f)) | X) by Th21

      .= (g | (( dom f) /\ X)) by RELAT_1: 71

      .= (g | X) by A1, XBOOLE_1: 28;

    end;

    theorem :: GRFUNC_1:28



     Th26: for f be Function, x be set st x in ( dom f) holds (f | {x}) = { [x, (f . x)]}

    proof

      let f be Function, x be set such that

       A1: x in ( dom f);



       A2: x in {x} by TARSKI:def 1;

      ( dom (f | {x}) qua Function) = (( dom f) /\ {x}) by RELAT_1: 61

      .= {x} by A1, ZFMISC_1: 46;



      hence (f | {x}) = { [x, ((f | {x}) . x)]} by Th7

      .= { [x, (f . x)]} by A2, FUNCT_1: 49;

    end;

    theorem :: GRFUNC_1:29



     Th27: for f,g be Function, x be set st ( dom f) = ( dom g) & (f . x) = (g . x) holds (f | {x}) = (g | {x})

    proof

      let f,g be Function, x be set such that

       A1: ( dom f) = ( dom g) and

       A2: (f . x) = (g . x);

      per cases ;

        suppose

         A3: x in ( dom f);



        hence (f | {x}) = { [x, (g . x)]} by A2, Th26

        .= (g | {x}) by A1, A3, Th26;

      end;

        suppose not x in ( dom f);

        then

         A4: {x} misses ( dom f) by ZFMISC_1: 50;



        hence (f | {x}) = {} by RELAT_1: 66

        .= (g | {x}) by A1, A4, RELAT_1: 66;

      end;

    end;

    theorem :: GRFUNC_1:30



     Th28: for f,g be Function, x,y be set st ( dom f) = ( dom g) & (f . x) = (g . x) & (f . y) = (g . y) holds (f | {x, y}) = (g | {x, y})

    proof

      let f,g be Function, x,y be set;

      assume ( dom f) = ( dom g) & (f . x) = (g . x) & (f . y) = (g . y);

      then

       A1: (f | {x}) = (g | {x}) & (f | {y}) = (g | {y}) by Th27;

       {x, y} = ( {x} \/ {y}) by ENUMSET1: 1;

      hence thesis by A1, RELAT_1: 150;

    end;

    theorem :: GRFUNC_1:31

    for f,g be Function, x,y,z be set st ( dom f) = ( dom g) & (f . x) = (g . x) & (f . y) = (g . y) & (f . z) = (g . z) holds (f | {x, y, z}) = (g | {x, y, z})

    proof

      let f,g be Function, x,y,z be set;

      assume ( dom f) = ( dom g) & (f . x) = (g . x) & (f . y) = (g . y) & (f . z) = (g . z);

      then

       A1: (f | {x, y}) = (g | {x, y}) & (f | {z}) = (g | {z}) by Th27, Th28;

       {x, y, z} = ( {x, y} \/ {z}) by ENUMSET1: 3;

      hence thesis by A1, RELAT_1: 150;

    end;

    registration

      let f be Function, A be set;

      cluster (f \ A) -> Function-like;

      coherence ;

    end

    theorem :: GRFUNC_1:32

    for f,g be Function st x in (( dom f) \ ( dom g)) holds ((f \ g) . x) = (f . x)

    proof

      let f,g be Function such that

       A1: x in (( dom f) \ ( dom g));

      (f \ g) c= f & (( dom f) \ ( dom g)) c= ( dom (f \ g)) by XTUPLE_0: 25;

      hence thesis by A1, Th2;

    end;

    theorem :: GRFUNC_1:33

    f c= g & f c= h implies (g | ( dom f)) = (h | ( dom f))

    proof

      assume that

       A1: f c= g and

       A2: f c= h;



      thus (g | ( dom f)) = f by A1, Th21

      .= (h | ( dom f)) by A2, Th21;

    end;

    registration

      let f be Function, g be Subset of f;

      cluster g -compatible -> f -compatible for Function;

      coherence

      proof

        let F be Function such that

         A1: F is g -compatible;

        let x;

        assume x in ( dom F);

        then

         A2: (F . x) in (g . x) by A1;

        then x in ( dom g) by FUNCT_1:def 2;

        hence (F . x) in (f . x) by A2, Th2;

      end;

    end

    theorem :: GRFUNC_1:34



     Th32: g c= f implies g = (f | ( dom g))

    proof

      assume

       A1: g c= f;

      then ( dom g) c= ( dom f) by RELAT_1: 11;

      hence ( dom g) = ( dom (f | ( dom g))) by RELAT_1: 62;

      let x;

      assume

       A2: x in ( dom g);



      hence (g . x) = (f . x) by A1, Th2

      .= ((f | ( dom g)) . x) by A2, FUNCT_1: 49;

    end;

    registration

      let f be Function, g be f -compatible Function;

      cluster -> f -compatible for Subset of g;

      coherence

      proof

        let h be Subset of g;

        h = (g | ( dom h)) by Th32;

        hence thesis;

      end;

    end

    theorem :: GRFUNC_1:35

    g c= f & x in X & (X /\ ( dom f)) c= ( dom g) implies (f . x) = (g . x)

    proof

      assume that

       A1: g c= f and

       A2: x in X and

       A3: (X /\ ( dom f)) c= ( dom g);

      per cases ;

        suppose x in ( dom g);

        hence (f . x) = (g . x) by A1, Th2;

      end;

        suppose

         A4: not x in ( dom g);

        then not x in (X /\ ( dom f)) by A3;

        then not x in ( dom f) by A2, XBOOLE_0:def 4;



        hence (f . x) = {} by FUNCT_1:def 2

        .= (g . x) by A4, FUNCT_1:def 2;

      end;

    end;