:: Some Properties of Binary Relations
::  by Waldemar Korczy\'nski
::
:: Received January 17, 1992
:: Copyright (c) 1992-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SYSREL;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
 constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
 registrations XBOOLE_0, RELAT_1;
 requirements BOOLE, SUBSET;


begin

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

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

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

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

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

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

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

theorem :: SYSREL:7
  (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);

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

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

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

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

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

theorem :: SYSREL:13
 for x being object holds  id({x}) = {[x,x]};

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

theorem :: SYSREL:15
  X c= Y implies id X c= id Y;

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

theorem :: SYSREL:17
  R c= id dom R implies R = id dom R;

theorem :: SYSREL:18
  id X c= R \/ R~ implies id X c= R & id X c= R~;

theorem :: SYSREL:19
  id X c= R implies id X c= R~;

:: CLOSURE RELATION

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

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

theorem :: SYSREL:22
  (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:23
  (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:24
  (R * (R \ id X) = {} implies R * (R \ id rng R) = {}) &
  ((R \ id X) * R = {} 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:25
  for x,y being object holds [x,y] in CL R implies x in dom CL R & x = y;

theorem :: SYSREL:26
  dom CL R = rng CL R;

theorem :: SYSREL:27
  (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:28
  CL R = id dom CL R;

theorem :: SYSREL:29
  (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:30
  (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:31
  (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:32
  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:33
  id dom CL R c= id dom R & id rng CL R c= id dom R;

theorem :: SYSREL:34
  id dom CL R c= R & id rng CL R c= R;

theorem :: SYSREL:35
  (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:36
  (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:37
  (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:38
  (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:39
  (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:40
  (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);