relset_2.miz

    begin

    reserve x,y for object,

X,Y,A,B,C,M for set;

    reserve P,Q,R,R1,R2 for Relation;

    notation

      let X be set;

      synonym {_{X}_} for SmallestPartition X;

    end

    theorem :: RELSET_2:1



     Th1: y in {_{X}_} iff ex x st y = {x} & x in X

    proof

      thus y in {_{X}_} implies ex x st y = {x} & x in X

      proof

        assume

         A1: y in {_{X}_};

        per cases ;

          suppose

           A2: X is empty;

          ex x be object st x in X & y = ( Class (( id X),x)) by A1, EQREL_1:def 3;

          hence thesis by A2;

        end;

          suppose X is non empty;

          then

          reconsider X9 = X as non empty set;

          y in the set of all {x} where x be Element of X9 by A1, EQREL_1: 37;

          then ex x be Element of X9 st (y = {x});

          hence thesis;

        end;

      end;

      given x such that

       A3: y = {x} and

       A4: x in X;

      reconsider X9 = X as non empty set by A4;

      y in the set of all {z} where z be Element of X9 by A3, A4;

      hence thesis by EQREL_1: 37;

    end;

    theorem :: RELSET_2:2



     Th2: X = {} iff {_{X}_} = {}

    proof

      thus X = {} implies {_{X}_} = {}

      proof

        assume

         A1: X = {} ;

        assume not thesis;

        then

        consider y be object such that

         A2: y in {_{X}_} by XBOOLE_0:def 1;

        ex x be object st (y = {x}) & (x in X) by A2, Th1;

        hence contradiction by A1;

      end;

      assume

       A3: {_{X}_} = {} ;

      assume not thesis;

      then

      consider x be object such that

       A4: x in X by XBOOLE_0:def 1;

       {x} in {_{X}_} by A4, Th1;

      hence contradiction by A3;

    end;

    theorem :: RELSET_2:3



     Th3: {_{(X \/ Y)}_} = ( {_{X}_} \/ {_{Y}_})

    proof

      thus {_{(X \/ Y)}_} c= ( {_{X}_} \/ {_{Y}_})

      proof

        let y be object;

        assume y in {_{(X \/ Y)}_};

        then

        consider x be object such that

         A1: y = {x} and

         A2: x in (X \/ Y) by Th1;

        x in X or x in Y by A2, XBOOLE_0:def 3;

        then y in {_{X}_} or y in {_{Y}_} by A1, Th1;

        hence thesis by XBOOLE_0:def 3;

      end;

      let y be object;

      assume

       A3: y in ( {_{X}_} \/ {_{Y}_});

      per cases by A3, XBOOLE_0:def 3;

        suppose y in {_{X}_};

        then

        consider x be object such that

         A4: y = {x} and

         A5: x in X by Th1;

        x in (X \/ Y) by A5, XBOOLE_0:def 3;

        hence thesis by A4, Th1;

      end;

        suppose y in {_{Y}_};

        then

        consider x be object such that

         A6: y = {x} and

         A7: x in Y by Th1;

        x in (X \/ Y) by A7, XBOOLE_0:def 3;

        hence thesis by A6, Th1;

      end;

    end;

    theorem :: RELSET_2:4



     Th4: {_{(X /\ Y)}_} = ( {_{X}_} /\ {_{Y}_})

    proof

      thus {_{(X /\ Y)}_} c= ( {_{X}_} /\ {_{Y}_})

      proof

        let y be object;

        assume y in {_{(X /\ Y)}_};

        then

        consider x be object such that

         A1: y = {x} and

         A2: x in (X /\ Y) by Th1;



         A3: x in X by A2, XBOOLE_0:def 4;



         A4: x in Y by A2, XBOOLE_0:def 4;



         A5: y in {_{X}_} by A1, A3, Th1;

        y in {_{Y}_} by A1, A4, Th1;

        hence thesis by A5, XBOOLE_0:def 4;

      end;

      let y be object;

      assume

       A6: y in ( {_{X}_} /\ {_{Y}_});

      then

       A7: y in {_{X}_} by XBOOLE_0:def 4;



       A8: y in {_{Y}_} by A6, XBOOLE_0:def 4;

      consider x be object such that

       A9: y = {x} and

       A10: x in X by A7, Th1;

      consider x1 be object such that

       A11: y = {x1} and

       A12: x1 in Y by A8, Th1;

      x = x1 by A9, A11, ZFMISC_1: 3;

      then x in (X /\ Y) by A10, A12, XBOOLE_0:def 4;

      hence thesis by A9, Th1;

    end;

    theorem :: RELSET_2:5

     {_{(X \ Y)}_} = ( {_{X}_} \ {_{Y}_})

    proof

      thus {_{(X \ Y)}_} c= ( {_{X}_} \ {_{Y}_})

      proof

        let y be object;

        assume y in {_{(X \ Y)}_};

        then

        consider x be object such that

         A1: y = {x} and

         A2: x in (X \ Y) by Th1;



         A3: not x in Y by A2, XBOOLE_0:def 5;



         A4: y in {_{X}_} by A1, A2, Th1;

         not y in {_{Y}_}

        proof

          assume not thesis;

          then ex x1 be object st (y = {x1}) & (x1 in Y) by Th1;

          hence contradiction by A1, A3, ZFMISC_1: 3;

        end;

        hence thesis by A4, XBOOLE_0:def 5;

      end;

      let y be object;

      assume

       A5: y in ( {_{X}_} \ {_{Y}_});

      then

       A6: y in {_{X}_};



       A7: not y in {_{Y}_} by A5, XBOOLE_0:def 5;

      consider x be object such that

       A8: y = {x} and

       A9: x in X by A6, Th1;

       not x in Y by A7, A8, Th1;

      then x in (X \ Y) by A9, XBOOLE_0:def 5;

      hence thesis by A8, Th1;

    end;

    theorem :: RELSET_2:6



     Th6: X c= Y iff {_{X}_} c= {_{Y}_}

    proof

      thus X c= Y implies {_{X}_} c= {_{Y}_}

      proof

        assume

         A1: X c= Y;

        let y be object;

        assume y in {_{X}_};

        then ex x be object st (y = {x}) & (x in X) by Th1;

        hence thesis by A1, Th1;

      end;

      assume

       A2: {_{X}_} c= {_{Y}_};

      let y be object;

      assume y in X;

      then {y} in {_{X}_} by Th1;

      then ex x1 be object st ( {y} = {x1}) & (x1 in Y) by A2, Th1;

      hence thesis by ZFMISC_1: 3;

    end;

    theorem :: RELSET_2:7

    for B1,B2 be Subset-Family of M holds (( Intersect B1) /\ ( Intersect B2)) c= ( Intersect (B1 /\ B2))

    proof

      let B1,B2 be Subset-Family of M;

      ( Intersect (B1 \/ B2)) c= ( Intersect (B1 /\ B2)) by SETFAM_1: 44, XBOOLE_1: 29;

      hence thesis by MSSUBFAM: 8;

    end;

    theorem :: RELSET_2:8

    ((P /\ Q) * R) c= ((P * R) /\ (Q * R))

    proof

      let x,y be object;

      assume [x, y] in ((P /\ Q) * R);

      then

      consider z be object such that

       A1: [x, z] in (P /\ Q) and

       A2: [z, y] in R by RELAT_1:def 8;



       A3: [x, z] in P by A1, XBOOLE_0:def 4;



       A4: [x, z] in Q by A1, XBOOLE_0:def 4;



       A5: [x, y] in (P * R) by A2, A3, RELAT_1:def 8;

       [x, y] in (Q * R) by A2, A4, RELAT_1:def 8;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    begin

    theorem :: RELSET_2:9



     Th9: y in ( Im (R,x)) iff [x, y] in R

    proof

      thus y in ( Im (R,x)) implies [x, y] in R

      proof

        assume y in ( Im (R,x));

        then ex a be object st ( [a, y] in R) & (a in {x}) by RELAT_1:def 13;

        hence thesis by TARSKI:def 1;

      end;

      assume

       A1: [x, y] in R;

      x in {x} by TARSKI:def 1;

      hence thesis by A1, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:10



     Th10: ( Im ((R1 \/ R2),x)) = (( Im (R1,x)) \/ ( Im (R2,x)))

    proof

      thus ( Im ((R1 \/ R2),x)) c= (( Im (R1,x)) \/ ( Im (R2,x)))

      proof

        let y be object;

        assume y in ( Im ((R1 \/ R2),x));

        then [x, y] in (R1 \/ R2) by Th9;

        then [x, y] in R1 or [x, y] in R2 by XBOOLE_0:def 3;

        then y in ( Im (R1,x)) or y in ( Im (R2,x)) by Th9;

        hence thesis by XBOOLE_0:def 3;

      end;

      let y be object;

      assume

       A1: y in (( Im (R1,x)) \/ ( Im (R2,x)));

      per cases by A1, XBOOLE_0:def 3;

        suppose y in ( Im (R1,x));

        then [x, y] in R1 by Th9;

        then [x, y] in (R1 \/ R2) by XBOOLE_0:def 3;

        hence thesis by Th9;

      end;

        suppose y in ( Im (R2,x));

        then [x, y] in R2 by Th9;

        then [x, y] in (R1 \/ R2) by XBOOLE_0:def 3;

        hence thesis by Th9;

      end;

    end;

    theorem :: RELSET_2:11



     Th11: ( Im ((R1 /\ R2),x)) = (( Im (R1,x)) /\ ( Im (R2,x)))

    proof

      thus ( Im ((R1 /\ R2),x)) c= (( Im (R1,x)) /\ ( Im (R2,x)))

      proof

        let y be object;

        assume y in ( Im ((R1 /\ R2),x));

        then

         A1: [x, y] in (R1 /\ R2) by Th9;

        then

         A2: [x, y] in R1 by XBOOLE_0:def 4;



         A3: [x, y] in R2 by A1, XBOOLE_0:def 4;



         A4: y in ( Im (R1,x)) by A2, Th9;

        y in ( Im (R2,x)) by A3, Th9;

        hence thesis by A4, XBOOLE_0:def 4;

      end;

      let y be object;

      assume

       A5: y in (( Im (R1,x)) /\ ( Im (R2,x)));

      then

       A6: y in ( Im (R1,x)) by XBOOLE_0:def 4;



       A7: y in ( Im (R2,x)) by A5, XBOOLE_0:def 4;



       A8: [x, y] in R1 by A6, Th9;

       [x, y] in R2 by A7, Th9;

      then [x, y] in (R1 /\ R2) by A8, XBOOLE_0:def 4;

      hence thesis by Th9;

    end;

    theorem :: RELSET_2:12

    ( Im ((R1 \ R2),x)) = (( Im (R1,x)) \ ( Im (R2,x)))

    proof

      thus ( Im ((R1 \ R2),x)) c= (( Im (R1,x)) \ ( Im (R2,x)))

      proof

        let y be object;

        assume y in ( Im ((R1 \ R2),x));

        then

         A1: [x, y] in (R1 \ R2) by Th9;

        then

         A2: not [x, y] in R2 by XBOOLE_0:def 5;



         A3: y in ( Im (R1,x)) by A1, Th9;

         not y in ( Im (R2,x)) by A2, Th9;

        hence thesis by A3, XBOOLE_0:def 5;

      end;

      let y be object;

      assume

       A4: y in (( Im (R1,x)) \ ( Im (R2,x)));

      then

       A5: not y in ( Im (R2,x)) by XBOOLE_0:def 5;



       A6: [x, y] in R1 by A4, Th9;

       not [x, y] in R2 by A5, Th9;

      then [x, y] in (R1 \ R2) by A6, XBOOLE_0:def 5;

      hence thesis by Th9;

    end;

    theorem :: RELSET_2:13

    ((R1 /\ R2) .: {_{X}_}) c= ((R1 .: {_{X}_}) /\ (R2 .: {_{X}_}))

    proof

      let y be object;

      assume y in ((R1 /\ R2) .: {_{X}_});

      then

      consider x be object such that

       A1: [x, y] in (R1 /\ R2) and

       A2: x in {_{X}_} by RELAT_1:def 13;



       A3: [x, y] in R1 by A1, XBOOLE_0:def 4;



       A4: [x, y] in R2 by A1, XBOOLE_0:def 4;



       A5: y in (R1 .: {_{X}_}) by A2, A3, RELAT_1:def 13;

      y in (R2 .: {_{X}_}) by A2, A4, RELAT_1:def 13;

      hence thesis by A5, XBOOLE_0:def 4;

    end;

    definition

      let X,Y be set;

      let R be Relation of X, Y;

      let x be object;

      :: original: Im

      redefine

      func Im (R,x) -> Subset of Y ;

      coherence

      proof

        ( Im (R,x)) = (R .: {x});

        hence thesis;

      end;

      :: original: Coim

      redefine

      func Coim (R,x) -> Subset of X ;

      coherence

      proof

        ( Coim (R,x)) = (R " {x});

        hence thesis;

      end;

    end

    theorem :: RELSET_2:14

    for A be set, F be Subset-Family of A, R be Relation holds (R .: ( union F)) = ( union { (R .: X) where X be Subset of A : X in F })

    proof

      let A be set, F be Subset-Family of A, R be Relation;

      thus (R .: ( union F)) c= ( union { (R .: f) where f be Subset of A : f in F })

      proof

        let y be object;

        assume y in (R .: ( union F));

        then

        consider x be object such that

         A1: [x, y] in R and

         A2: x in ( union F) by RELAT_1:def 13;

        consider Y be set such that

         A3: x in Y and

         A4: Y in F by A2, TARSKI:def 4;

        set Z = (R .: Y);



         A5: y in Z by A1, A3, RELAT_1:def 13;

        Z in { (R .: f) where f be Subset of A : f in F } by A4;

        hence thesis by A5, TARSKI:def 4;

      end;

      let y be object;

      assume y in ( union { (R .: f) where f be Subset of A : f in F });

      then

      consider Y be set such that

       A6: y in Y and

       A7: Y in { (R .: f) where f be Subset of A : f in F } by TARSKI:def 4;

      consider f be Subset of A such that

       A8: Y = (R .: f) and

       A9: f in F by A7;

      consider x be object such that

       A10: [x, y] in R and

       A11: x in f by A6, A8, RELAT_1:def 13;

      x in ( union F) by A9, A11, TARSKI:def 4;

      hence thesis by A10, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:15



     Th15: for A be set, X be Subset of A holds X = ( union { {x} where x be Element of A : x in X })

    proof

      let A be set, X be Subset of A;

      thus X c= ( union { {x} where x be Element of A : x in X })

      proof

        let a be object;

        assume

         A1: a in X;

        set Y = {a};



         A2: a in Y by TARSKI:def 1;

        Y in { {x} where x be Element of A : x in X } by A1;

        hence thesis by A2, TARSKI:def 4;

      end;

      let a be object;

      assume a in ( union { {x} where x be Element of A : x in X });

      then

      consider Y be set such that

       A3: a in Y and

       A4: Y in { {x} where x be Element of A : x in X } by TARSKI:def 4;

      ex x be Element of A st (Y = {x}) & (x in X) by A4;

      hence thesis by A3, TARSKI:def 1;

    end;

    theorem :: RELSET_2:16

    for A be set, X be Subset of A holds { {x} where x be Element of A : x in X } is Subset-Family of A

    proof

      let A be set, X be Subset of A;

      { {x} where x be Element of A : x in X } c= ( bool A)

      proof

        let a be object;

        reconsider aa = a as set by TARSKI: 1;

        assume a in { {x} where x be Element of A : x in X };

        then ex x be Element of A st (a = {x}) & (x in X);

        then aa c= A by ZFMISC_1: 31;

        hence thesis;

      end;

      hence thesis;

    end;

    theorem :: RELSET_2:17

    for A,B be set, X be Subset of A, R be Relation of A, B holds (R .: X) = ( union { ( Class (R,x)) where x be Element of A : x in X })

    proof

      let A,B be set, X be Subset of A, R be Relation of A, B;

      thus (R .: X) c= ( union { ( Class (R,x)) where x be Element of A : x in X })

      proof

        let y be object;

        assume y in (R .: X);

        then

        consider x1 be object such that

         A1: [x1, y] in R and

         A2: x1 in X by RELAT_1:def 13;

        x1 in ( union { {x} where x be Element of A : x in X }) by A2, Th15;

        then

        consider S be set such that

         A3: x1 in S and

         A4: S in { {x} where x be Element of A : x in X } by TARSKI:def 4;

        consider x be Element of A such that

         A5: S = {x} and

         A6: x in X by A4;



         A7: y in (R .: {x}) by A1, A3, A5, RELAT_1:def 13;

        set Y = (R .: {x});

        Y = ( Class (R,x));

        then Y in { ( Class (R,xs)) where xs be Element of A : xs in X } by A6;

        hence thesis by A7, TARSKI:def 4;

      end;

      let a be object;

      assume a in ( union { ( Class (R,x)) where x be Element of A : x in X });

      then

      consider Y be set such that

       A8: a in Y and

       A9: Y in { ( Class (R,x)) where x be Element of A : x in X } by TARSKI:def 4;

      consider x be Element of A such that

       A10: Y = ( Class (R,x)) and

       A11: x in X by A9;

      Y c= (R .: X)

      proof

        let b be object;

        assume b in Y;

        then

        consider x1 be object such that

         A12: [x1, b] in R and

         A13: x1 in {x} by A10, RELAT_1:def 13;

        x1 = x by A13, TARSKI:def 1;

        hence thesis by A11, A12, RELAT_1:def 13;

      end;

      hence thesis by A8;

    end;

    theorem :: RELSET_2:18

    for A be non empty set, B be set, X be Subset of A, R be Relation of A, B holds { (R .: x) where x be Element of A : x in X } is Subset-Family of B

    proof

      let A be non empty set, B be set, X be Subset of A, R be Relation of A, B;

      deffunc F( Element of A) = (R .: $1);

      defpred P[ set] means $1 in X;

      set Y = { F(x) where x be Element of A : P[x] };

      thus Y is Subset-Family of B from DOMAIN_1:sch 8;

    end;

    definition

      let A be set, R be Relation;

      :: RELSET_2:def1

      func .: (R,A) -> Function means

      : Def1: ( dom it ) = ( bool A) & for X be set st X c= A holds (it . X) = (R .: X);

      existence

      proof

        defpred P[ object, object] means for X st $1 = X holds $2 = (R .: X);



         A1: for x be object st x in ( bool A) holds ex y be object st P[x, y]

        proof

          let x be object such that x in ( bool A);

          reconsider x as set by TARSKI: 1;

          take (R .: x);

          thus thesis;

        end;

        consider g be Function such that

         A2: ( dom g) = ( bool A) and

         A3: for x be object st x in ( bool A) holds P[x, (g . x)] from CLASSES1:sch 1( A1);

        take g;

        thus thesis by A2, A3;

      end;

      uniqueness

      proof

        let R1,R2 be Function such that

         A4: ( dom R1) = ( bool A) and

         A5: for X st X c= A holds (R1 . X) = (R .: X) and

         A6: ( dom R2) = ( bool A) and

         A7: for X st X c= A holds (R2 . X) = (R .: X);

        for x be object st x in ( bool A) holds (R1 . x) = (R2 . x)

        proof

          let x be object;

          assume

           A8: x in ( bool A);

          reconsider xx = x as set by TARSKI: 1;

          (R1 . x) = (R .: xx) by A5, A8;

          hence thesis by A7, A8;

        end;

        hence thesis by A4, A6, FUNCT_1: 2;

      end;

    end

    notation

      let B,A be set;

      let R be Subset of [:A, B:];

      synonym .: R for .: (R,A);

    end

    theorem :: RELSET_2:19



     Th19: for A,B be set, R be Subset of [:A, B:] st X in ( dom ( .: R)) holds (( .: R) . X) = (R .: X)

    proof

      let A,B be set;

      let R be Subset of [:A, B:];

      assume X in ( dom ( .: R));

      then X in ( bool A) by Def1;

      hence thesis by Def1;

    end;

    theorem :: RELSET_2:20



     Th20: for A,B be set, R be Subset of [:A, B:] holds ( rng ( .: R)) c= ( bool ( rng R))

    proof

      let A,B be set, R be Subset of [:A, B:];

      let y be object;

      reconsider yy = y as set by TARSKI: 1;

      assume y in ( rng ( .: R));

      then

      consider x be object such that

       A1: x in ( dom ( .: R)) and

       A2: y = (( .: R) . x) by FUNCT_1:def 3;

      reconsider x as set by TARSKI: 1;

      y = (R .: x) by A1, A2, Th19;

      then yy c= ( rng R) by RELAT_1: 111;

      hence thesis;

    end;

    theorem :: RELSET_2:21



     Th21: for A,B be set, R be Subset of [:A, B:] holds ( .: R) is Function of ( bool A), ( bool ( rng R))

    proof

      let A,B be set, R be Subset of [:A, B:];



       A1: ( dom ( .: R)) = ( bool A) by Def1;

      ( rng ( .: R)) c= ( bool ( rng R)) by Th20;

      hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

    end;

    definition

      let B,A be set;

      let R be Subset of [:A, B:];

      :: original: .:

      redefine

      func .: R -> Function of ( bool A), ( bool B) ;

      correctness

      proof



         A1: ( dom ( .: R)) = ( bool A) by Def1;

        ( .: R) is Function of ( bool A), ( bool ( rng R)) by Th21;

        then

         A2: ( rng ( .: R)) c= ( bool ( rng R)) by RELAT_1:def 19;

        ( bool ( rng R)) c= ( bool B) by ZFMISC_1: 67;

        then ( rng ( .: R)) c= ( bool B) by A2;

        hence thesis by A1, FUNCT_2:def 1, RELSET_1: 4;

      end;

    end

    theorem :: RELSET_2:22

    for A,B be set, R be Subset of [:A, B:] holds ( union (( .: R) .: A)) c= (R .: ( union A))

    proof

      let A,B be set, R be Subset of [:A, B:];

      let y be object;

      assume y in ( union (( .: R) .: A));

      then

      consider Z be set such that

       A1: y in Z and

       A2: Z in (( .: R) .: A) by TARSKI:def 4;

      consider X be object such that

       A3: X in ( dom ( .: R)) and

       A4: X in A and

       A5: Z = (( .: R) . X) by A2, FUNCT_1:def 6;

      reconsider X as set by TARSKI: 1;

      y in (R .: X) by A1, A3, A5, Th19;

      then

      consider x be object such that

       A6: [x, y] in R and

       A7: x in X by RELAT_1:def 13;

      x in ( union A) by A4, A7, TARSKI:def 4;

      hence thesis by A6, RELAT_1:def 13;

    end;

    begin

    reserve X,X1,X2 for Subset of A;

    reserve Y for Subset of B;

    reserve R,R1,R2 for Subset of [:A, B:];

    reserve FR for Subset-Family of [:A, B:];

    definition

      let A,B be set, X be Subset of A, R be Subset of [:A, B:];

      :: RELSET_2:def2

      func R .:^ X -> set equals ( Intersect (( .: R) .: {_{X}_}));

      correctness ;

    end

    definition

      let A,B be set;

      let X be Subset of A;

      let R be Subset of [:A, B:];

      :: original: .:^

      redefine

      func R .:^ X -> Subset of B ;

      coherence ;

    end

    theorem :: RELSET_2:23



     Th23: (( .: R) .: {_{X}_}) = {} iff X = {}

    proof

      thus (( .: R) .: {_{X}_}) = {} implies X = {}

      proof

        assume (( .: R) .: {_{X}_}) = {} ;

        then ( dom ( .: R)) misses {_{X}_} by RELAT_1: 118;

        then

         A1: ( bool A) misses {_{X}_} by Def1;

         {_{X}_} c= ( bool A)

        proof

          let y be object;

          reconsider yy = y as set by TARSKI: 1;

          assume y in {_{X}_};

          then

          consider x be object such that

           A2: y = {x} and

           A3: x in X by Th1;



           A4: x in A by A3;

          yy c= A by A2, A4, TARSKI:def 1;

          hence thesis;

        end;

        then

         A5: (( bool A) /\ {_{X}_}) = {_{X}_} by XBOOLE_1: 28;

        assume X <> {} ;

        then {_{X}_} <> {} by Th2;

        hence thesis by A1, A5;

      end;

      assume X = {} ;

      then {_{X}_} = {} by Th2;

      hence thesis;

    end;

    theorem :: RELSET_2:24



     Th24: y in (R .:^ X) implies for x be set st x in X holds y in ( Im (R,x))

    proof

      assume

       A1: y in (R .:^ X);

      per cases ;

        suppose (( .: R) .: {_{X}_}) = {} ;

        hence thesis by Th23;

      end;

        suppose (( .: R) .: {_{X}_}) <> {} ;

        then

         A2: y in ( meet (( .: R) .: {_{X}_})) by A1, SETFAM_1:def 9;

        for x be set st x in X holds y in (R .: {x})

        proof

          let x be set;

          assume

           A3: x in X;

          then

           A4: {x} in {_{X}_} by Th1;



           A5: {x} c= A

          proof

            let a be object;

            assume a in {x};

            then a = x by TARSKI:def 1;

            hence thesis by A3;

          end;

          then

           A6: (( .: R) . {x}) = (R .: {x}) by Def1;

          ( dom ( .: R)) = ( bool A) by Def1;

          then [ {x}, (R .: {x})] in ( .: R) by A5, A6, FUNCT_1: 1;

          then (R .: {x}) in (( .: R) .: {_{X}_}) by A4, RELAT_1:def 13;

          hence thesis by A2, SETFAM_1:def 1;

        end;

        hence thesis;

      end;

    end;

    theorem :: RELSET_2:25



     Th25: for B be non empty set, A be set, X be Subset of A, y be Element of B, R be Subset of [:A, B:] holds y in (R .:^ X) iff for x be set st x in X holds y in ( Im (R,x))

    proof

      let B be non empty set, A be set, X be Subset of A, y be Element of B, R be Subset of [:A, B:];

      thus y in (R .:^ X) implies for x be set st x in X holds y in ( Im (R,x)) by Th24;

      assume

       A1: for x be set st x in X holds y in ( Im (R,x));

      per cases ;

        suppose (( .: R) .: {_{X}_}) = {} ;

        then ( Intersect (( .: R) .: {_{X}_})) = B by SETFAM_1:def 9;

        hence thesis;

      end;

        suppose

         A2: (( .: R) .: {_{X}_}) <> {} ;

        then

         A3: ( Intersect (( .: R) .: {_{X}_})) = ( meet (( .: R) .: {_{X}_})) by SETFAM_1:def 9;

        for Y be set holds Y in (( .: R) .: {_{X}_}) implies y in Y

        proof

          let Y be set;

          assume Y in (( .: R) .: {_{X}_});

          then

          consider z be object such that

           A4: [z, Y] in ( .: R) and

           A5: z in {_{X}_} by RELAT_1:def 13;

          consider x be object such that

           A6: z = {x} and

           A7: x in X by A5, Th1;



           A8: z in ( dom ( .: R)) by A4, FUNCT_1: 1;

          Y = (( .: R) . z) by A4, FUNCT_1: 1;

          then Y = ( Im (R,x)) by A6, A8, Def1;

          hence thesis by A1, A7;

        end;

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

      end;

    end;

    theorem :: RELSET_2:26

    (( .: R) .: {_{X1}_}) = {} implies (R .:^ (X1 \/ X2)) = (R .:^ X2)

    proof



       A1: {_{(X1 \/ X2)}_} = ( {_{X1}_} \/ {_{X2}_}) by Th3;

      assume

       A2: (( .: R) .: {_{X1}_}) = {} ;

      (R .:^ (X1 \/ X2)) = ( Intersect ((( .: R) .: {_{X1}_}) \/ (( .: R) .: {_{X2}_}))) by A1, RELAT_1: 120

      .= (R .:^ X2) by A2;

      hence thesis;

    end;

    theorem :: RELSET_2:27

    (R .:^ (X1 \/ X2)) = ((R .:^ X1) /\ (R .:^ X2))

    proof

      (R .:^ (X1 \/ X2)) = ( Intersect (( .: R) .: ( {_{X1}_} \/ {_{X2}_}))) by Th3

      .= ( Intersect ((( .: R) .: {_{X1}_}) \/ (( .: R) .: {_{X2}_}))) by RELAT_1: 120

      .= ((R .:^ X1) /\ (R .:^ X2)) by MSSUBFAM: 8;

      hence thesis;

    end;

    theorem :: RELSET_2:28

    for A be non empty set, B be set, F be Subset-Family of A, R be Relation of A, B holds { (R .:^ X) where X be Subset of A : X in F } is Subset-Family of B

    proof

      let A be non empty set, B be set, F be Subset-Family of A, R be Relation of A, B;

      deffunc F( Subset of A) = (R .:^ $1);

      defpred P[ set] means $1 in F;

      set Y = { F(X) where X be Subset of A : P[X] };

      thus Y is Subset-Family of B from DOMAIN_1:sch 8;

    end;

    theorem :: RELSET_2:29



     Th29: X = {} implies (R .:^ X) = B by Th23, SETFAM_1:def 9;

    theorem :: RELSET_2:30

    for A be set, B be non empty set, R be Relation of A, B, F be Subset-Family of A, G be Subset-Family of B st G = { (R .:^ Y) where Y be Subset of A : Y in F } holds (R .:^ ( union F)) = ( Intersect G)

    proof

      let A be set, B be non empty set, R be Relation of A, B, F be Subset-Family of A, G be Subset-Family of B;

      assume

       A1: G = { (R .:^ Y) where Y be Subset of A : Y in F };

      per cases ;

        suppose

         A2: ( union F) = {} ;

        then

         A3: (R .:^ ( union F)) = B by Th29;

        per cases ;

          suppose

           A4: G <> {} ;

          G c= {B}

          proof

            let x be object;

            assume x in G;

            then

            consider Y be Subset of A such that

             A5: x = (R .:^ Y) and

             A6: Y in F by A1;

            Y = {} by A2, A6, ORDERS_1: 6;

            then (( .: R) .: {_{Y}_}) = {} by Th23;

            then ( Intersect (( .: R) .: {_{Y}_})) = B by SETFAM_1:def 9;

            hence thesis by A5, TARSKI:def 1;

          end;

          then ( meet {B}) c= ( meet G) by A4, SETFAM_1: 6;

          then B c= ( meet G) by SETFAM_1: 10;

          then ( meet G) = B;

          hence thesis by A3, SETFAM_1:def 9;

        end;

          suppose G = {} ;

          hence thesis by A3, SETFAM_1:def 9;

        end;

      end;

        suppose ( union F) <> {} ;

        then

        consider Z1 be set such that Z1 <> {} and

         A7: Z1 in F by ORDERS_1: 6;

        reconsider Z1 as Subset of A by A7;



         A8: G <> {}

        proof

          assume not thesis;

          then not (R .:^ Z1) in G;

          hence contradiction by A1, A7;

        end;

        thus (R .:^ ( union F)) c= ( Intersect G)

        proof

          let a be object;

          assume

           A9: a in (R .:^ ( union F));

          for Y be set holds Y in G implies a in Y

          proof

            let Z2 be set;

            assume Z2 in G;

            then

            consider Z3 be Subset of A such that

             A10: Z2 = (R .:^ Z3) and

             A11: Z3 in F by A1;

            reconsider a as Element of B by A9;

            for x be set st x in Z3 holds a in ( Im (R,x))

            proof

              let x be set;

              assume x in Z3;

              then x in ( union F) by A11, TARSKI:def 4;

              hence thesis by A9, Th24;

            end;

            hence thesis by A10, Th25;

          end;

          then a in ( meet G) by A8, SETFAM_1:def 1;

          hence thesis by A8, SETFAM_1:def 9;

        end;

        let a be object;

        assume

         A12: a in ( Intersect G);

        then

         A13: a in ( meet G) by A8, SETFAM_1:def 9;

        reconsider a as Element of B by A12;

        for X be set st X in ( union F) holds a in ( Im (R,X))

        proof

          let X be set;

          assume X in ( union F);

          then

          consider Z be set such that

           A14: X in Z and

           A15: Z in F by TARSKI:def 4;

          reconsider Z as Subset of A by A15;

          set C = (R .:^ Z);

          C in G by A1, A15;

          then a in C by A13, SETFAM_1:def 1;

          hence thesis by A14, Th24;

        end;

        hence thesis by Th25;

      end;

    end;

    theorem :: RELSET_2:31



     Th31: X1 c= X2 implies (R .:^ X2) c= (R .:^ X1)

    proof

      assume X1 c= X2;

      then

       A1: {_{X1}_} c= {_{X2}_} by Th6;

      let y be object;

      assume

       A2: y in (R .:^ X2);

      per cases ;

        suppose

         A3: (( .: R) .: {_{X2}_}) = {} ;

        per cases ;

          suppose (( .: R) .: {_{X1}_}) = {} ;

          then ( Intersect (( .: R) .: {_{X1}_})) = B by SETFAM_1:def 9;

          hence thesis by A2;

        end;

          suppose

           A4: (( .: R) .: {_{X1}_}) <> {} ;

          for Y be set holds Y in (( .: R) .: {_{X1}_}) implies y in Y

          proof

            let Y be set;

            assume Y in (( .: R) .: {_{X1}_});

            then ex x be object st ( [x, Y] in ( .: R)) & (x in {_{X1}_}) by RELAT_1:def 13;

            hence thesis by A1, A3, RELAT_1:def 13;

          end;

          then y in ( meet (( .: R) .: {_{X1}_})) by A4, SETFAM_1:def 1;

          hence thesis by A4, SETFAM_1:def 9;

        end;

      end;

        suppose (( .: R) .: {_{X2}_}) <> {} ;

        then

         A5: y in ( meet (( .: R) .: {_{X2}_})) by A2, SETFAM_1:def 9;

        per cases ;

          suppose (( .: R) .: {_{X1}_}) = {} ;

          then ( Intersect (( .: R) .: {_{X1}_})) = B by SETFAM_1:def 9;

          hence thesis by A2;

        end;

          suppose

           A6: (( .: R) .: {_{X1}_}) <> {} ;

          (( .: R) .: {_{X1}_}) c= (( .: R) .: {_{X2}_}) by A1, RELAT_1: 123;

          then ( meet (( .: R) .: {_{X2}_})) c= ( meet (( .: R) .: {_{X1}_})) by A6, SETFAM_1: 6;

          then y in ( meet (( .: R) .: {_{X1}_})) by A5;

          hence thesis by A6, SETFAM_1:def 9;

        end;

      end;

    end;

    theorem :: RELSET_2:32

    ((R .:^ X1) \/ (R .:^ X2)) c= (R .:^ (X1 /\ X2))

    proof

      let y be object;

      assume

       A1: y in ((R .:^ X1) \/ (R .:^ X2));



       A2: {_{(X1 /\ X2)}_} = ( {_{X1}_} /\ {_{X2}_}) by Th4;

      then

       A3: (( .: R) .: {_{(X1 /\ X2)}_}) c= ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) by RELAT_1: 121;

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A4: y in (R .:^ X1);

        y in ( Intersect (( .: R) .: {_{(X1 /\ X2)}_}))

        proof

          per cases ;

            suppose

             A5: (( .: R) .: {_{(X1 /\ X2)}_}) <> {} ;



             A6: {_{(X1 /\ X2)}_} = ( {_{X1}_} /\ {_{X2}_}) by Th4;

            then

             A7: (( .: R) .: {_{(X1 /\ X2)}_}) c= ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) by RELAT_1: 121;



             A8: ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) <> {} by A5, A6, RELAT_1: 121, XBOOLE_1: 3;

            (( .: R) .: {_{X1}_}) <> {} by A5, A7;

            then

             A9: y in ( meet (( .: R) .: {_{X1}_})) by A4, SETFAM_1:def 9;

            for Y be set holds Y in ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) implies y in Y

            proof

              let Y be set;

              assume Y in ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}));

              then Y in (( .: R) .: {_{X1}_}) by XBOOLE_0:def 4;

              hence thesis by A9, SETFAM_1:def 1;

            end;

            then y in ( meet ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) by A8, SETFAM_1:def 1;

            then

             A10: y in ( Intersect ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) by A8, SETFAM_1:def 9;

            ( Intersect ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) c= ( Intersect (( .: R) .: ( {_{X1}_} /\ {_{X2}_}))) by RELAT_1: 121, SETFAM_1: 44;

            hence thesis by A2, A10;

          end;

            suppose (( .: R) .: {_{(X1 /\ X2)}_}) = {} ;

            then ( Intersect (( .: R) .: {_{(X1 /\ X2)}_})) = B by SETFAM_1:def 9;

            hence thesis by A4;

          end;

        end;

        hence thesis;

      end;

        suppose

         A11: y in (R .:^ X2);

        y in ( Intersect (( .: R) .: {_{(X1 /\ X2)}_}))

        proof

          per cases ;

            suppose

             A12: (( .: R) .: {_{(X1 /\ X2)}_}) <> {} ;

            then

             A13: ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) <> {} by A2, RELAT_1: 121, XBOOLE_1: 3;

            (( .: R) .: {_{X2}_}) <> {} by A3, A12;

            then

             A14: y in ( meet (( .: R) .: {_{X2}_})) by A11, SETFAM_1:def 9;

            for Y be set holds Y in ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_})) implies y in Y

            proof

              let Y be set;

              assume Y in ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}));

              then Y in (( .: R) .: {_{X2}_}) by XBOOLE_0:def 4;

              hence thesis by A14, SETFAM_1:def 1;

            end;

            then y in ( meet ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) by A13, SETFAM_1:def 1;

            then

             A15: y in ( Intersect ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) by A13, SETFAM_1:def 9;



             A16: {_{(X1 /\ X2)}_} = ( {_{X1}_} /\ {_{X2}_}) by Th4;

            ( Intersect ((( .: R) .: {_{X1}_}) /\ (( .: R) .: {_{X2}_}))) c= ( Intersect (( .: R) .: ( {_{X1}_} /\ {_{X2}_}))) by RELAT_1: 121, SETFAM_1: 44;

            hence thesis by A15, A16;

          end;

            suppose (( .: R) .: {_{(X1 /\ X2)}_}) = {} ;

            then ( Intersect (( .: R) .: {_{(X1 /\ X2)}_})) = B by SETFAM_1:def 9;

            hence thesis by A11;

          end;

        end;

        hence thesis;

      end;

    end;

    theorem :: RELSET_2:33

    ((R1 /\ R2) .:^ X) = ((R1 .:^ X) /\ (R2 .:^ X))

    proof

      thus ((R1 /\ R2) .:^ X) c= ((R1 .:^ X) /\ (R2 .:^ X))

      proof

        let y be object;

        assume

         A1: y in ((R1 /\ R2) .:^ X);

        then

        reconsider B as non empty set;

        reconsider y as Element of B by A1;

        for x be set st x in X holds y in ( Im (R1,x))

        proof

          let x be set;

          assume x in X;

          then y in ( Im ((R1 /\ R2),x)) by A1, Th24;

          then y in (( Im (R1,x)) /\ ( Im (R2,x))) by Th11;

          hence thesis by XBOOLE_0:def 4;

        end;

        then

         A2: y in (R1 .:^ X) by Th25;

        for x be set st x in X holds y in ( Im (R2,x))

        proof

          let x be set;

          assume x in X;

          then y in ( Im ((R1 /\ R2),x)) by A1, Th24;

          then y in (( Im (R1,x)) /\ ( Im (R2,x))) by Th11;

          hence thesis by XBOOLE_0:def 4;

        end;

        then y in (R2 .:^ X) by Th25;

        hence thesis by A2, XBOOLE_0:def 4;

      end;

      let y be object;

      assume

       A3: y in ((R1 .:^ X) /\ (R2 .:^ X));

      then

       A4: y in (R1 .:^ X) by XBOOLE_0:def 4;



       A5: y in (R2 .:^ X) by A3, XBOOLE_0:def 4;

      reconsider B as non empty set by A3;

      reconsider y as Element of B by A3;

      for x be set st x in X holds y in ( Im ((R1 /\ R2),x))

      proof

        let x be set;

        assume

         A6: x in X;

        then

         A7: y in ( Im (R1,x)) by A4, Th25;

        y in ( Im (R2,x)) by A5, A6, Th25;

        then y in (( Im (R1,x)) /\ ( Im (R2,x))) by A7, XBOOLE_0:def 4;

        hence thesis by Th11;

      end;

      hence thesis by Th25;

    end;

    theorem :: RELSET_2:34

    (( union FR) .: X) = ( union { (R .: X) where R be Subset of [:A, B:] : R in FR })

    proof

      thus (( union FR) .: X) c= ( union { (R .: X) where R be Subset of [:A, B:] : R in FR })

      proof

        let a be object;

        assume a in (( union FR) .: X);

        then

        consider x be object such that

         A1: [x, a] in ( union FR) and

         A2: x in X by RELAT_1:def 13;

        consider S be set such that

         A3: [x, a] in S and

         A4: S in FR by A1, TARSKI:def 4;

        reconsider S as Subset of [:A, B:] by A4;

        ex P be set st a in P & P in { (T .: X) where T be Subset of [:A, B:] : T in FR }

        proof

          set P = (S .: X);



           A5: a in P by A2, A3, RELAT_1:def 13;

          P in { (T .: X) where T be Subset of [:A, B:] : T in FR } by A4;

          hence thesis by A5;

        end;

        hence thesis by TARSKI:def 4;

      end;

      let a be object;

      assume a in ( union { (R .: X) where R be Subset of [:A, B:] : R in FR });

      then

      consider P be set such that

       A6: a in P and

       A7: P in { (R .: X) where R be Subset of [:A, B:] : R in FR } by TARSKI:def 4;

      consider R be Subset of [:A, B:] such that

       A8: P = (R .: X) and

       A9: R in FR by A7;

      consider x be object such that

       A10: [x, a] in R and

       A11: x in X by A6, A8, RELAT_1:def 13;

      ex x be set st x in X & [x, a] in ( union FR)

      proof

        take x;

        thus thesis by A9, A10, A11, TARSKI:def 4;

      end;

      hence thesis by RELAT_1:def 13;

    end;

    theorem :: RELSET_2:35

    for FR be Subset-Family of [:A, B:], A,B be set, X be Subset of A holds { (R .:^ X) where R be Subset of [:A, B:] : R in FR } is Subset-Family of B

    proof

      let FR be Subset-Family of [:A, B:], A,B be set, X be Subset of A;

      deffunc F( Subset of [:A, B:]) = ($1 .:^ X);

      defpred P[ set] means $1 in FR;

      set G = { F(R) where R be Subset of [:A, B:] : P[R] };

      thus G is Subset-Family of B from DOMAIN_1:sch 8;

    end;

    theorem :: RELSET_2:36



     Th36: R = {} & X <> {} implies (R .:^ X) = {}

    proof

      assume that

       A1: R = {} and

       A2: X <> {} ;

      (R .:^ X) c= {}

      proof

        let a be object;

        assume

         A3: a in (R .:^ X);

        consider x be object such that

         A4: x in X by A2, XBOOLE_0:def 1;

        a in ( Im (R,x)) by A3, A4, Th24;

        hence thesis by A1;

      end;

      hence thesis;

    end;

    theorem :: RELSET_2:37



     Th37: R = [:A, B:] implies (R .:^ X) = B

    proof

      assume

       A1: R = [:A, B:];

      thus (R .:^ X) c= B;

      thus B c= (R .:^ X)

      proof

        let a be object;

        assume

         A2: a in B;

        then

        reconsider B as non empty set;

        reconsider a as Element of B by A2;

        for x be set st x in X holds a in ( Im (R,x))

        proof

          let x be set;

          assume x in X;

          then [x, a] in R by A1, ZFMISC_1: 87;

          hence thesis by Th9;

        end;

        hence thesis by Th25;

      end;

    end;

    theorem :: RELSET_2:38

    for G be Subset-Family of B st G = { (R .:^ X) where R be Subset of [:A, B:] : R in FR } holds (( Intersect FR) .:^ X) = ( Intersect G)

    proof

      let G be Subset-Family of B;

      assume

       A1: G = { (R .:^ X) where R be Subset of [:A, B:] : R in FR };



       A2: for x be set st G = {x} holds ( Intersect G) = x

      proof

        let x be set;

        assume G = {x};

        then ( Intersect G) = ( meet {x}) by SETFAM_1:def 9;

        hence thesis by SETFAM_1: 10;

      end;

      per cases ;

        suppose

         A3: X = {} ;

        then

         A4: (( Intersect FR) .:^ X) = B by Th29;

        G c= {B}

        proof

          let a be object;

          assume a in G;

          then ex R be Subset of [:A, B:] st (a = (R .:^ X)) & (R in FR) by A1;

          then a = B by A3, Th29;

          hence thesis by TARSKI:def 1;

        end;

        then G = {} or G = {B} by ZFMISC_1: 33;

        hence thesis by A2, A4, SETFAM_1:def 9;

      end;

        suppose

         A5: X <> {} ;

        per cases ;

          suppose

           A6: FR = {} ;

          then ( Intersect FR) = [:A, B:] by SETFAM_1:def 9;

          then

           A7: (( Intersect FR) .:^ X) = B by Th37;

          G c= {B}

          proof

            let a be object;

            assume a in G;

            then ex R be Subset of [:A, B:] st (a = (R .:^ X)) & (R in FR) by A1;

            hence thesis by A6;

          end;

          then G = {} or G = {B} by ZFMISC_1: 33;

          hence thesis by A2, A7, SETFAM_1:def 9;

        end;

          suppose

           A8: FR <> {} ;

          per cases ;

            suppose

             A9: B = {} ;

            then [:A, B:] = {} by ZFMISC_1: 90;

            then FR = {} or FR = { {} } by ZFMISC_1: 1, ZFMISC_1: 33;

            then ( Intersect FR) = ( meet { {} }) by A8, SETFAM_1:def 9;

            then (( Intersect FR) .:^ X) = {} by A5, Th36, SETFAM_1: 10;

            hence thesis by A9;

          end;

            suppose B <> {} ;

            then

            reconsider B as non empty set;

            thus (( Intersect FR) .:^ X) c= ( Intersect G)

            proof

              let a be object;

              assume

               A10: a in (( Intersect FR) .:^ X);

              then

               A11: a in B;

              reconsider a as Element of B by A10;

              G <> {} implies a in ( Intersect G)

              proof

                assume

                 A12: G <> {} ;

                then

                 A13: ( Intersect G) = ( meet G) by SETFAM_1:def 9;

                for Y be set holds Y in G implies a in Y

                proof

                  let Y be set;

                  assume Y in G;

                  then

                  consider R be Subset of [:A, B:] such that

                   A14: Y = (R .:^ X) and

                   A15: R in FR by A1;

                  for x be set st x in X holds a in ( Im (R,x))

                  proof

                    let x be set;

                    assume x in X;

                    then a in ( Im (( Intersect FR),x)) by A10, Th24;

                    then [x, a] in ( Intersect FR) by Th9;

                    then [x, a] in ( meet FR) by A8, SETFAM_1:def 9;

                    then [x, a] in R by A15, SETFAM_1:def 1;

                    hence thesis by Th9;

                  end;

                  hence thesis by A14, Th25;

                end;

                hence thesis by A12, A13, SETFAM_1:def 1;

              end;

              hence thesis by A11, SETFAM_1:def 9;

            end;

            let a be object;

            assume

             A16: a in ( Intersect G);

            then

            reconsider a as Element of B;

            consider R be Subset of [:A, B:] such that

             A17: R in FR by A8, SUBSET_1: 4;

            (R .:^ X) in G by A1, A17;

            then

             A18: a in ( meet G) by A16, SETFAM_1:def 9;

            for x be set st x in X holds a in ( Im (( Intersect FR),x))

            proof

              let x be set such that

               A19: x in X;

              for Y be set holds Y in FR implies [x, a] in Y

              proof

                let P be set;

                assume

                 A20: P in FR;

                then

                reconsider P as Subset of [:A, B:];

                set S = (P .:^ X);

                S in G by A1, A20;

                then a in (P .:^ X) by A18, SETFAM_1:def 1;

                then a in ( Im (P,x)) by A19, Th24;

                hence thesis by Th9;

              end;

              then [x, a] in ( meet FR) by A8, SETFAM_1:def 1;

              then [x, a] in ( Intersect FR) by A8, SETFAM_1:def 9;

              hence thesis by Th9;

            end;

            hence thesis by Th25;

          end;

        end;

      end;

    end;

    theorem :: RELSET_2:39

    R1 c= R2 implies (R1 .:^ X) c= (R2 .:^ X)

    proof

      assume

       A1: R1 c= R2;

      let y be object;

      assume

       A2: y in (R1 .:^ X);

      then

      reconsider B as non empty set;

      reconsider y as Element of B by A2;

      for x be set st x in X holds y in ( Im (R2,x))

      proof

        let x be set;

        assume x in X;

        then y in ( Im (R1,x)) by A2, Th25;

        then [x, y] in R1 by Th9;

        hence thesis by A1, Th9;

      end;

      hence thesis by Th25;

    end;

    theorem :: RELSET_2:40

    ((R1 .:^ X) \/ (R2 .:^ X)) c= ((R1 \/ R2) .:^ X)

    proof

      let y be object;

      assume

       A1: y in ((R1 .:^ X) \/ (R2 .:^ X));

      per cases by A1, XBOOLE_0:def 3;

        suppose

         A2: y in (R1 .:^ X);

        then

        reconsider B as non empty set;

        reconsider y as Element of B by A2;

        for x be set st x in X holds y in ( Im ((R1 \/ R2),x))

        proof

          let x be set;

          assume x in X;

          then y in ( Im (R1,x)) by A2, Th25;

          then y in (( Im (R1,x)) \/ ( Im (R2,x))) by XBOOLE_0:def 3;

          hence thesis by Th10;

        end;

        hence thesis by Th25;

      end;

        suppose

         A3: y in (R2 .:^ X);

        then

        reconsider B as non empty set;

        reconsider y as Element of B by A3;

        for x be set st x in X holds y in ( Im ((R1 \/ R2),x))

        proof

          let x be set;

          assume x in X;

          then y in ( Im (R2,x)) by A3, Th25;

          then y in (( Im (R1,x)) \/ ( Im (R2,x))) by XBOOLE_0:def 3;

          hence thesis by Th10;

        end;

        hence thesis by Th25;

      end;

    end;

    theorem :: RELSET_2:41



     Th41: y in ( Im ((R ` ),x)) iff not [x, y] in R & x in A & y in B

    proof

      thus y in ( Im ((R ` ),x)) implies not [x, y] in R & x in A & y in B

      proof

        assume y in ( Im ((R ` ),x));

        then ex a be object st ( [a, y] in (R ` )) & (a in {x}) by RELAT_1:def 13;

        then [x, y] in ( [:A, B:] \ R) by TARSKI:def 1;

        hence thesis by XBOOLE_0:def 5, ZFMISC_1: 87;

      end;

      assume that

       A1: not [x, y] in R and

       A2: x in A and

       A3: y in B;



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

       [x, y] in [:A, B:] by A2, A3, ZFMISC_1: 87;

      then [x, y] in ( [:A, B:] \ R) by A1, XBOOLE_0:def 5;

      hence thesis by A4, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:42

    X <> {} implies (R .:^ X) c= (R .: X)

    proof

      assume

       A1: X <> {} ;

      let y be object;

      assume

       A2: y in (R .:^ X);

      consider x be object such that

       A3: x in X by A1, XBOOLE_0:def 1;

      y in ( Im (R,x)) by A2, A3, Th24;

      then [x, y] in R by Th9;

      hence thesis by A3, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:43



     Th43: for X,Y be set holds X meets ((R ~ ) .: Y) iff ex x,y be set st x in X & y in Y & x in ( Im ((R ~ ),y))

    proof

      let X,Y be set;

      hereby

        assume X meets ((R ~ ) .: Y);

        then

        consider a be object such that

         A1: a in X and

         A2: a in ((R ~ ) .: Y) by XBOOLE_0: 3;

        consider b be object such that

         A3: [b, a] in (R ~ ) and

         A4: b in Y by A2, RELAT_1:def 13;



         A5: b in {b} by TARSKI:def 1;

        reconsider a, b as set by TARSKI: 1;

        take a, b;

        thus a in X by A1;

        thus b in Y by A4;

        thus a in ( Im ((R ~ ),b)) by A3, A5, RELAT_1:def 13;

      end;

      given x,y be set such that

       A6: x in X and

       A7: y in Y and

       A8: x in ( Im ((R ~ ),y));

      ex a be object st ( [a, x] in (R ~ )) & (a in {y}) by A8, RELAT_1:def 13;

      then [y, x] in (R ~ ) by TARSKI:def 1;

      then x in ((R ~ ) .: Y) by A7, RELAT_1:def 13;

      hence thesis by A6, XBOOLE_0: 3;

    end;

    theorem :: RELSET_2:44



     Th44: for X,Y be set holds (ex x,y be set st x in X & y in Y & x in ( Im ((R ~ ),y))) iff Y meets (R .: X)

    proof

      let X,Y be set;

      thus (ex x,y be set st x in X & y in Y & x in ( Im ((R ~ ),y))) implies Y meets (R .: X)

      proof

        given x,y be set such that

         A1: x in X and

         A2: y in Y and

         A3: x in ( Im ((R ~ ),y));

        consider a be object such that

         A4: [a, x] in (R ~ ) and

         A5: a in {y} by A3, RELAT_1:def 13;

        a = y by A5, TARSKI:def 1;

        then [x, y] in R by A4, RELAT_1:def 7;

        then y in (R .: X) by A1, RELAT_1:def 13;

        hence thesis by A2, XBOOLE_0: 3;

      end;

      assume Y meets (R .: X);

      then

      consider a be object such that

       A6: a in Y and

       A7: a in (R .: X) by XBOOLE_0: 3;

      consider b be object such that

       A8: [b, a] in R and

       A9: b in X by A7, RELAT_1:def 13;



       A10: [a, b] in (R ~ ) by A8, RELAT_1:def 7;



       A11: a in {a} by TARSKI:def 1;

      reconsider a, b as set by TARSKI: 1;

      take b, a;

      thus b in X by A9;

      thus a in Y by A6;

      thus thesis by A10, A11, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:45



     Th45: X misses ((R ~ ) .: Y) iff Y misses (R .: X)

    proof

      X meets ((R ~ ) .: Y) iff ex x,y be set st x in X & y in Y & x in ( Im ((R ~ ),y)) by Th43;

      hence thesis by Th44;

    end;

    theorem :: RELSET_2:46



     Th46: for X be set holds (R .: X) = (R .: (X /\ ( proj1 R)))

    proof

      let X be set;

      thus (R .: X) c= (R .: (X /\ ( proj1 R)))

      proof

        let y be object;

        assume y in (R .: X);

        then

        consider x be object such that

         A1: [x, y] in R and

         A2: x in X by RELAT_1:def 13;

        x in ( proj1 R) by A1, XTUPLE_0:def 12;

        then x in (X /\ ( proj1 R)) by A2, XBOOLE_0:def 4;

        hence thesis by A1, RELAT_1:def 13;

      end;

      let y be object;

      assume y in (R .: (X /\ ( proj1 R)));

      then

      consider x be object such that

       A3: [x, y] in R and

       A4: x in (X /\ ( proj1 R)) by RELAT_1:def 13;

      x in X by A4, XBOOLE_0:def 4;

      hence thesis by A3, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:47



     Th47: for Y be set holds ((R ~ ) .: Y) = ((R ~ ) .: (Y /\ ( proj2 R)))

    proof

      let Y be set;

      thus ((R ~ ) .: Y) c= ((R ~ ) .: (Y /\ ( proj2 R)))

      proof

        let y be object;

        assume y in ((R ~ ) .: Y);

        then

        consider x be object such that

         A1: [x, y] in (R ~ ) and

         A2: x in Y by RELAT_1:def 13;

         [y, x] in R by A1, RELAT_1:def 7;

        then x in ( proj2 R) by XTUPLE_0:def 13;

        then x in (Y /\ ( proj2 R)) by A2, XBOOLE_0:def 4;

        hence thesis by A1, RELAT_1:def 13;

      end;

      let y be object;

      assume y in ((R ~ ) .: (Y /\ ( proj2 R)));

      then

      consider x be object such that

       A3: [x, y] in (R ~ ) and

       A4: x in (Y /\ ( proj2 R)) by RELAT_1:def 13;

      x in Y by A4, XBOOLE_0:def 4;

      hence thesis by A3, RELAT_1:def 13;

    end;

    theorem :: RELSET_2:48



     Th48: ((R .:^ X) ` ) = ((R ` ) .: X)

    proof

      thus ((R .:^ X) ` ) c= ((R ` ) .: X)

      proof

        let a be object;

        assume

         A1: a in ((R .:^ X) ` );

        then not a in (R .:^ X) by XBOOLE_0:def 5;

        then

        consider x be set such that

         A2: x in X and

         A3: not a in ( Im (R,x)) by A1, Th25;



         A4: not [x, a] in R by A3, Th9;

         [x, a] in [:A, B:] by A1, A2, ZFMISC_1: 87;

        then [x, a] in ( [:A, B:] \ R) by A4, XBOOLE_0:def 5;

        hence thesis by A2, RELAT_1:def 13;

      end;

      let a be object;

      assume a in ((R ` ) .: X);

      then

      consider x be object such that

       A5: [x, a] in (R ` ) and

       A6: x in X by RELAT_1:def 13;



       A7: not [x, a] in R by A5, XBOOLE_0:def 5;

      assume not thesis;

      then

       A8: not a in B or a in (R .:^ X) by XBOOLE_0:def 5;

      a in (R .:^ X) implies for x be set st x in X holds [x, a] in R

      proof

        assume

         A9: a in (R .:^ X);

        let x be set;

        assume x in X;

        then a in ( Im (R,x)) by A9, Th24;

        hence thesis by Th9;

      end;

      hence contradiction by A5, A6, A7, A8, ZFMISC_1: 87;

    end;

    reserve R for Relation of A, B;

    reserve S for Relation of B, C;

    definition

      let A,B,C be set;

      let R be Subset of [:A, B:], S be Subset of [:B, C:];

      :: original: *

      redefine

      func R * S -> Relation of A, C ;

      coherence

      proof

        reconsider R as Relation of A, B;

        reconsider S as Relation of B, C;

        (R * S) is Relation of A, C;

        hence thesis;

      end;

    end

    theorem :: RELSET_2:49



     Th49: ((R .: X) ` ) = ((R ` ) .:^ X)

    proof

      thus ((R .: X) ` ) c= ((R ` ) .:^ X)

      proof

        let a be object;

        assume

         A1: a in ((R .: X) ` );

        then

        reconsider B as non empty set;

        reconsider a as Element of B by A1;

        assume not thesis;

        then

        consider x be set such that

         A2: x in X and

         A3: not a in ( Im ((R ` ),x)) by Th25;

         [x, a] in R by A2, A3, Th41;

        then a in (R .: X) by A2, RELAT_1:def 13;

        hence contradiction by A1, XBOOLE_0:def 5;

      end;

      let a be object;

      assume

       A4: a in ((R ` ) .:^ X);



       A5: a in ((R ` ) .:^ X) implies for x be set st x in X holds not [x, a] in R

      proof

        assume a in ((R ` ) .:^ X);

        let x be set;

        assume

         A6: x in X;

        assume

         A7: not thesis;

        a in ( Im ((R ` ),x)) by A4, A6, Th24;

        then ex b be object st ( [b, a] in (R ` )) & (b in {x}) by RELAT_1:def 13;

        then

         A8: [x, a] in (R ` ) by TARSKI:def 1;

        (R ` ) misses R by XBOOLE_1: 79;

        hence contradiction by A7, A8, XBOOLE_0: 3;

      end;

      assume

       A9: not thesis;

      per cases by A9, XBOOLE_0:def 5;

        suppose not a in B;

        hence contradiction by A4;

      end;

        suppose a in (R .: X);

        then ex y be object st ( [y, a] in R) & (y in X) by RELAT_1:def 13;

        hence contradiction by A4, A5;

      end;

    end;

    theorem :: RELSET_2:50



     Th50: ( proj1 R) = ((R ~ ) .: B) & ( proj2 R) = (R .: A)

    proof



      thus ( proj1 R) = ( dom R)

      .= ( rng (R ~ )) by RELAT_1: 20

      .= ((R ~ ) .: B) by RELSET_1: 22;



      thus ( proj2 R) = ( rng R)

      .= (R .: A) by RELSET_1: 22;

    end;

    theorem :: RELSET_2:51

    ( proj1 (R * S)) = ((R ~ ) .: ( proj1 S)) & ( proj1 (R * S)) c= ( proj1 R)

    proof



      thus

       A1: ( proj1 (R * S)) = (((R * S) ~ ) .: C) by Th50

      .= (((S ~ ) * (R ~ )) .: C) by RELAT_1: 35

      .= ((R ~ ) .: ((S ~ ) .: C)) by RELAT_1: 126

      .= ((R ~ ) .: ( proj1 S)) by Th50;

      ( proj1 S) = ( dom S);

      then ( proj1 (R * S)) c= ((R ~ ) .: B) by A1, RELAT_1: 123;

      hence thesis by Th50;

    end;

    theorem :: RELSET_2:52

    ( proj2 (R * S)) = (S .: ( proj2 R)) & ( proj2 (R * S)) c= ( proj2 S)

    proof



      thus

       A1: ( proj2 (R * S)) = ((R * S) .: A) by Th50

      .= (S .: (R .: A)) by RELAT_1: 126

      .= (S .: ( proj2 R)) by Th50;

      ( proj2 R) = ( rng R);

      then (S .: ( proj2 R)) c= (S .: B) by RELAT_1: 123;

      hence thesis by A1, Th50;

    end;

    theorem :: RELSET_2:53

    X c= ( proj1 R) iff X c= ((R * (R ~ )) .: X)

    proof

      thus X c= ( proj1 R) implies X c= ((R * (R ~ )) .: X)

      proof

        assume

         A1: X c= ( proj1 R);

        let x be object;

        assume

         A2: x in X;

        then

        reconsider x as Element of A;

        consider y be object such that

         A3: [x, y] in R by A1, A2, XTUPLE_0:def 12;



         A4: [y, x] in (R ~ ) by A3, RELAT_1:def 7;

        y in {y} by TARSKI:def 1;

        then

         A5: x in ((R ~ ) .: {y}) by A4, RELAT_1:def 13;

        ((R ~ ) .: {y}) c= ((R * (R ~ )) .: X)

        proof

          let a be object;

          assume a in ((R ~ ) .: {y});

          then ex b be object st ( [b, a] in (R ~ )) & (b in {y}) by RELAT_1:def 13;

          then [y, a] in (R ~ ) by TARSKI:def 1;

          then [x, a] in (R * (R ~ )) by A3, RELAT_1:def 8;

          hence thesis by A2, RELAT_1:def 13;

        end;

        hence thesis by A5;

      end;

      assume

       A6: X c= ((R * (R ~ )) .: X);

      let x be object;

      assume x in X;

      then

       A7: x in ((R * (R ~ )) .: X) by A6;



       A8: ((R * (R ~ )) .: X) = ((R ~ ) .: (R .: X)) by RELAT_1: 126;

      ((R ~ ) .: (R .: X)) c= ((R ~ ) .: B) by RELAT_1: 123;

      then ((R * (R ~ )) .: X) c= ( proj1 R) by A8, Th50;

      hence thesis by A7;

    end;

    theorem :: RELSET_2:54

    Y c= ( proj2 R) iff Y c= (((R ~ ) * R) .: Y)

    proof

      thus Y c= ( proj2 R) implies Y c= (((R ~ ) * R) .: Y)

      proof

        assume

         A1: Y c= ( proj2 R);

        let y be object;

        assume

         A2: y in Y;

        then

        consider x be object such that

         A3: [x, y] in R by A1, XTUPLE_0:def 13;



         A4: [y, x] in (R ~ ) by A3, RELAT_1:def 7;



         A5: y in ( Im (R,x)) by A3, Th9;

        (R .: {x}) c= (((R ~ ) * R) .: Y)

        proof

          let a be object;

          assume a in (R .: {x});

          then ex b be object st ( [b, a] in R) & (b in {x}) by RELAT_1:def 13;

          then [x, a] in R by TARSKI:def 1;

          then [y, a] in ((R ~ ) * R) by A4, RELAT_1:def 8;

          hence thesis by A2, RELAT_1:def 13;

        end;

        hence thesis by A5;

      end;

      assume

       A6: Y c= (((R ~ ) * R) .: Y);

      let x be object;

      assume x in Y;

      then

       A7: x in (((R ~ ) * R) .: Y) by A6;



       A8: (((R ~ ) * R) .: Y) = (R .: ((R ~ ) .: Y)) by RELAT_1: 126;

      (R .: ((R ~ ) .: Y)) c= (R .: A) by RELAT_1: 123;

      then (((R ~ ) * R) .: Y) c= ( proj2 R) by A8, Th50;

      hence thesis by A7;

    end;

    theorem :: RELSET_2:55

    ( proj1 R) = ((R ~ ) .: B) & ((R ~ ) .: (R .: A)) = ((R ~ ) .: ( proj2 R)) by Th50;

    theorem :: RELSET_2:56

    ((R ~ ) .: B) = ((R * (R ~ )) .: A)

    proof



       A1: ((R * (R ~ )) .: A) = ((R ~ ) .: (R .: A)) by RELAT_1: 126

      .= ((R ~ ) .: ( proj2 R)) by Th50;

      thus ((R ~ ) .: B) c= ((R * (R ~ )) .: A)

      proof

        let x be object;

        assume

         A2: x in ((R ~ ) .: B);



         A3: ((R ~ ) .: B) = ((R ~ ) .: (B /\ ( proj2 R))) by Th47;

        ((R ~ ) .: (B /\ ( proj2 R))) c= (((R ~ ) .: B) /\ ((R ~ ) .: ( proj2 R))) by RELAT_1: 121;

        hence thesis by A1, A2, A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in ((R * (R ~ )) .: A);

      ( proj2 R) c= ( rng R);

      then ((R ~ ) .: ( proj2 R)) c= ((R ~ ) .: B) by RELAT_1: 123;

      hence thesis by A1, A4;

    end;

    theorem :: RELSET_2:57

    (R .: A) = (((R ~ ) * R) .: B)

    proof



       A1: (((R ~ ) * R) .: B) = (R .: ((R ~ ) .: B)) by RELAT_1: 126

      .= (R .: ( proj1 R)) by Th50;

      thus (R .: A) c= (((R ~ ) * R) .: B)

      proof

        let x be object;

        assume

         A2: x in (R .: A);



         A3: (R .: A) = (R .: (A /\ ( proj1 R))) by Th46;

        (R .: (A /\ ( proj1 R))) c= ((R .: A) /\ (R .: ( proj1 R))) by RELAT_1: 121;

        hence thesis by A1, A2, A3, XBOOLE_0:def 4;

      end;

      let x be object;

      assume

       A4: x in (((R ~ ) * R) .: B);

      ( proj1 R) c= ( dom R);

      then (R .: ( proj1 R)) c= (R .: A) by RELAT_1: 123;

      hence thesis by A1, A4;

    end;

    theorem :: RELSET_2:58

    (S .:^ (R .: X)) = (((R * (S ` )) ` ) .:^ X)

    proof

      ((S .:^ (R .: X)) ` ) = ((S ` ) .: (R .: X)) by Th48

      .= ((R * (S ` )) .: X) by RELAT_1: 126;



      then (S .:^ (R .: X)) = (((R * (S ` )) .: X) ` )

      .= (((R * (S ` )) ` ) .:^ X) by Th49;

      hence thesis;

    end;

    theorem :: RELSET_2:59



     Th59: ((R ` ) ~ ) = ((R ~ ) ` )

    proof

      ((R ` ) ~ ) = (( [:A, B:] ~ ) \ (R ~ )) by RELAT_1: 24

      .= ((R ~ ) ` ) by SYSREL: 5;

      hence thesis;

    end;

    theorem :: RELSET_2:60



     Th60: X c= ((R ~ ) .:^ Y) iff Y c= (R .:^ X)

    proof

      X c= ((R ~ ) .:^ Y) iff X misses (((R ~ ) .:^ Y) ` ) by SUBSET_1: 24;

      then X c= ((R ~ ) .:^ Y) iff X misses (((R ~ ) ` ) .: Y) by Th48;

      then

       A1: X c= ((R ~ ) .:^ Y) iff (X /\ (((R ~ ) ` ) .: Y)) = {} ;

      reconsider S = (R ` ) as Relation of A, B;

      X misses ((S ~ ) .: Y) iff Y misses (S .: X) by Th45;

      then (X /\ ((S ~ ) .: Y)) = {} iff (Y /\ (S .: X)) = {} ;

      then X c= ((R ~ ) .:^ Y) iff (((R .:^ X) ` ) /\ Y) = {} by A1, Th48, Th59;

      then X c= ((R ~ ) .:^ Y) iff ((R .:^ X) ` ) misses Y;

      hence thesis by SUBSET_1: 24;

    end;

    theorem :: RELSET_2:61

    (R .: (X ` )) c= (Y ` ) iff ((R ~ ) .: Y) c= X

    proof

      (X ` ) misses ((R ~ ) .: Y) iff Y misses (R .: (X ` )) by Th45;

      hence thesis by SUBSET_1: 23, SUBSET_1: 24;

    end;

    theorem :: RELSET_2:62

    X c= ((R ~ ) .:^ (R .:^ X)) & Y c= (R .:^ ((R ~ ) .:^ Y)) by Th60;

    theorem :: RELSET_2:63

    (R .:^ X) = (R .:^ ((R ~ ) .:^ (R .:^ X))) & ((R ~ ) .:^ Y) = ((R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y)))

    proof



       A1: (R .:^ X) c= (R .:^ ((R ~ ) .:^ (R .:^ X))) by Th60;

      X c= ((R ~ ) .:^ (R .:^ X)) by Th60;

      then (R .:^ ((R ~ ) .:^ (R .:^ X))) c= (R .:^ X) by Th31;

      hence (R .:^ X) = (R .:^ ((R ~ ) .:^ (R .:^ X))) by A1;

      thus ((R ~ ) .:^ Y) c= ((R ~ ) .:^ (R .:^ ((R ~ ) .:^ Y))) by Th60;

      Y c= (R .:^ ((R ~ ) .:^ Y)) by Th60;

      hence thesis by Th31;

    end;

    theorem :: RELSET_2:64

    (( id A) * R) = (R * ( id B))

    proof

      (( id A) * R) = R by FUNCT_2: 17

      .= (R * ( id B)) by FUNCT_2: 17;

      hence thesis;

    end;