The abstract of the Mizar article:

Some Properties of Binary Relations

by

Waldemar Korczynski

Received January 17, 1992

MML identifier: SYSREL

[ Mizar article, MML identifier index ]

environ

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


begin
 reserve x,y,z,t,X,Y,Z,W for set;
 reserve R,S,T for Relation;

definition let X,Y;
 cluster [:X,Y:] -> Relation-like;
end;

canceled 11;

theorem :: SYSREL:12
  X <> {} & Y <> {} implies dom [:X,Y:] = X & rng [:X,Y:] = Y;

theorem :: SYSREL:13
  dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y;

theorem :: SYSREL:14
    X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:]) &
                    dom (R~ /\ [:X,Y:]) misses rng (R~ /\ [:X,Y:]);

theorem :: SYSREL:15
  R c= [:X,Y:] implies dom R c= X & rng R c= Y;

theorem :: SYSREL:16
    R c= [:X,Y:] implies R~ c= [:Y,X:];

canceled;

theorem :: SYSREL:18
    [:X,Y:]~ = [:Y,X:];

canceled;

theorem :: SYSREL:20
  (R \/ S) * T = (R * T) \/ (S * T) & R * (S \/ T) = (R * S) \/ (R * T);

canceled;

theorem :: SYSREL:22
  (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X
                  implies not x in Y & not y in X & y in Y) &
      (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y
                  implies not y in X & not x in Y & x in X) &
      (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y
                  implies not x in X & not y in Y & y in X) &
      (X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X
                  implies not x in X & not y in Y & x in Y);

canceled;

theorem :: SYSREL:24
  (R c= [:X,Y:] & Z c= X implies (R|Z) = R /\ [:Z,Y:]) &
        (R c= [:X,Y:] & Z c= Y implies (Z|R) = R /\ [:X,Z:]);

theorem :: SYSREL:25
    R c= [:X,Y:] & X = Z \/ W implies R = (R|Z) \/ (R|W);

theorem :: SYSREL:26
    X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R|X c= [:X,Y:];

theorem :: SYSREL:27
    R c= S implies R~ c= S~;

canceled;

theorem :: SYSREL:29
  id(X) * id(X) = id(X);

theorem :: SYSREL:30
    id({x}) = {[x,x]};

theorem :: SYSREL:31
    [x,y] in id(X) iff [y,x] in id(X);

theorem :: SYSREL:32
  id(X \/ Y) = id(X) \/ id(Y) &
        id(X /\ Y) = id(X) /\ id(Y) &
        id(X \ Y) = id(X) \ id(Y);

theorem :: SYSREL:33
  X c= Y implies id(X) c= id(Y);

theorem :: SYSREL:34
    id(X \ Y) \ id(X) = {};

theorem :: SYSREL:35
    R c= id(dom R) implies R = id(dom R);

theorem :: SYSREL:36
    id(X) c= R \/ R~ implies id(X) c= R & id(X) c= R~;

theorem :: SYSREL:37
    id(X) c= R implies id(X) c= R~;

:: CLOSURE RELATION

theorem :: SYSREL:38
    R c= [:X,X:] implies R \ id(dom R) = R \ id(X) &
                               R \ id(rng R) = R \ id(X);

theorem :: SYSREL:39
    (id(X) * (R \ id(X)) = {} implies
     dom (R \ id(X)) = dom R \ dom (id(X))) &
     ((R \ id(X)) * id(X) = {} implies
                   rng (R \ id(X)) = rng R \ rng (id(X)));

theorem :: SYSREL:40
  (R c= R * R & R * (R \ id(rng(R))) = {} implies
                                            id(rng(R)) c= R) &
      (R c= R * R & (R \ id(dom(R))) * R = {} implies
                                            id(dom(R)) c= R);

theorem :: SYSREL:41
    (R c= R * R & R * (R \ id(rng(R))) = {} implies
                 R /\ (id(rng(R))) = id(rng(R))) &
      (R c= R * R & (R \ id(dom(R))) * R = {} implies
                 R /\ (id(dom(R))) = id(dom(R)));

theorem :: SYSREL:42
    (R * (R \ id(X)) = {} & rng R c= X implies
           R * (R \ id(rng R)) = {}) &
          ((R \ id(X)) * R = {} & dom R c= X implies
           (R \ id(dom R)) * R = {});

:: OPERATION CL

definition let R;
 func CL(R) -> Relation equals
:: SYSREL:def 1
 R /\ id(dom R);
end;

theorem :: SYSREL:43
  CL(R) c= R & CL(R) c= id(dom R);

theorem :: SYSREL:44
  [x,y] in CL(R) implies x in dom( CL(R)) & x = y;

theorem :: SYSREL:45
  dom(CL(R)) = rng(CL(R));

theorem :: SYSREL:46
  (x in dom(CL(R)) iff x in dom R & [x,x] in R) &
        (x in rng(CL(R)) iff x in dom R & [x,x] in R) &
          (x in rng(CL(R)) iff x in rng R & [x,x] in R) &
           (x in dom(CL(R)) iff x in rng R & [x,x] in R);

theorem :: SYSREL:47
  CL(R) = id(dom CL(R));

theorem :: SYSREL:48
  (R * R = R & R * (R \ CL(R)) = {} & [x,y] in R & x <> y implies
              x in (dom R \ dom(CL(R))) & y in dom(CL(R))) &
     (R * R = R & (R \ CL(R)) * R = {} & [x,y] in R & x <> y implies
              y in (rng R \ dom(CL(R))) & x in dom(CL(R)));

theorem :: SYSREL:49
    (R * R = R & R * (R \ id(dom R)) = {} & [x,y] in R & x <> y
       implies x in ((dom R) \ dom(CL(R))) & y in dom(CL(R))) &
     (R * R = R & (R \ id(dom R)) * R = {} & [x,y] in R & x <> y
       implies y in ((rng R) \ dom(CL(R))) & x in dom(CL(R)));

theorem :: SYSREL:50
    (R * R = R & R * (R \ id(dom R)) = {}
                  implies dom(CL(R)) = rng(R) & rng(CL(R)) = rng(R)) &
        (R * R = R & (R \ id(dom R)) * R = {}
                  implies dom(CL(R)) = dom(R) & rng(CL(R)) = dom(R));

theorem :: SYSREL:51
  dom(CL(R)) c= dom R & rng(CL(R)) c= rng R &
       rng(CL(R)) c= dom R & dom(CL(R)) c= rng R;

theorem :: SYSREL:52
    id(dom(CL(R))) c= id(dom R) &
        id(rng(CL(R))) c= id(dom R);

theorem :: SYSREL:53
  id(dom(CL(R))) c= R & id(rng(CL(R))) c= R;

theorem :: SYSREL:54
  (id(X) c= R & id(X) * (R \ id(X)) = {}
                          implies R|X = id(X)) &
       (id(X) c= R & (R \ id(X)) * id(X) = {}
                          implies X|R = id(X));

theorem :: SYSREL:55
    (id(dom(CL(R))) * (R \ id(dom(CL(R)))) = {} implies
         R|(dom(CL(R))) = id(dom(CL(R))) &
              R|(rng(CL(R))) = id(dom(CL(R)))) &
 ((R \ id(rng(CL(R)))) * id(rng(CL(R))) = {} implies
                     (dom(CL(R)))|R = id(dom(CL(R))) &
                        (rng(CL(R)))|R = id(rng(CL(R))));

theorem :: SYSREL:56
    (R * (R \ id(dom R)) = {} implies
       id(dom(CL(R))) * (R \ id(dom(CL(R)))) = {}) &
       ((R \ id(dom R)) * R = {} implies
       (R \ id(dom(CL(R)))) * id(dom(CL(R))) = {});

theorem :: SYSREL:57
  (S * R = S & R * (R \ id(dom R)) = {} implies
                    S * (R \ id(dom R)) = {}) &
      (R * S = S & (R \ id(dom R)) * R = {} implies
                    (R \ id(dom R)) * S = {});

theorem :: SYSREL:58
  (S * R = S & R * (R \ id(dom R)) = {} implies CL(S) c= CL(R)) &
        (R * S = S & (R \ id(dom R)) * R = {} implies
                                                 CL(S) c= CL(R));

theorem :: SYSREL:59
    (S * R = S & R * (R \ id(dom R)) = {} &
        R * S = R & S * (S \ id(dom S)) = {} implies
   CL(S) = CL(R)) & (R * S = S & (R \ id(dom R)) * R = {} &
    S * R = R & (S \ id(dom S)) * S = {} implies CL(S) = CL(R));