:: Relations Defined on Sets
:: by Edmund Woronowicz
::
:: Received April 14, 1989
:: Copyright (c) 1990-2012 Association of Mizar Users


begin

::
:: RELATION AS A SUBSET OF CARTESIAN PRODUCT OF TWO SETS
:: _____________________________________________________
definition
let X, Y be set ;
mode Relation of X,Y is Subset of [:X,Y:];
end;

registration
let X, Y be set ;
cluster  ->  Relation-like for Element of bool [:X,Y:];
coherence
 for b1 being Subset of [:X,Y:] holds b1 is Relation-like ;
end;

registration
let X, Y be set ;
cluster  -> X -defined Y -valued for Element of bool [:X,Y:];
coherence
 for b1 being Relation of X,Y holds
( b1 is X -defined & b1 is Y -valued )
proofend;
end;

definition
let X, Y be set ;
let R be Relation of X,Y;
let Z be set ;
:: original:c=
redefine predR c= Z means :: RELSET_1:def 1
 for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z;
compatibility
 ( R c= Z iff for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z )
proofend;
end;

:: deftheorem  defines c= RELSET_1:def_1_:_
 for X, Y being set
for R being Relation of X,Y
for Z being set holds
( R c= Z iff for x being Element of X
for y being Element of Y st [x,y] in R holds
[x,y] in Z );

definition
let X, Y be set ;
let P, R be Relation of X,Y;
:: original:=
redefine predP = R means :: RELSET_1:def 2
 for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R );
compatibility
 ( P = R iff for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) )
proofend;
end;

:: deftheorem  defines = RELSET_1:def_2_:_
 for X, Y being set
for P, R being Relation of X,Y holds
( P = R iff for x being Element of X
for y being Element of Y holds
( [x,y] in P iff [x,y] in R ) );

theorem :: RELSET_1:1
for A, X, Y being set
for R being Relation of X,Y st A c= R holds
A is Relation of X,Y by XBOOLE_1:1;

theorem :: RELSET_1:2
for a, X, Y being set
for R being Relation of X,Y st a in R holds
ex x, y being set st
( a = [x,y] & x in X & y in Y )
proofend;

theorem :: RELSET_1:3
for x, X, y, Y being set st x in X & y in Y holds
{[x,y]} is Relation of X,Y
proofend;

theorem :: RELSET_1:4
for X, Y being set
for R being Relation st dom R c= X & rng R c= Y holds
R is Relation of X,Y
proofend;

theorem :: RELSET_1:5
for X, X1, Y being set
for R being Relation of X,Y st dom R c= X1 holds
R is Relation of X1,Y
proofend;

theorem :: RELSET_1:6
for Y, Y1, X being set
for R being Relation of X,Y st rng R c= Y1 holds
R is Relation of X,Y1
proofend;

theorem :: RELSET_1:7
for X, X1, Y, Y1 being set
for R being Relation of X,Y st X c= X1 & Y c= Y1 holds
R is Relation of X1,Y1
proofend;

registration
let X be set ;
let R, S be X -defined Relation;
clusterR \/ S -> X -defined ;
coherence
 R \/ S is X -defined
proofend;
end;

registration
let X be set ;
let R be X -defined Relation;
let S be Relation;
clusterR /\ S -> X -defined ;
coherence
 R /\ S is X -defined
proofend;
clusterR \ S -> X -defined ;
coherence
 R \ S is X -defined ;
end;

registration
let X be set ;
let R, S be X -valued Relation;
clusterR \/ S -> X -valued ;
coherence
 R \/ S is X -valued
proofend;
end;

registration
let X be set ;
let R be X -valued Relation;
let S be Relation;
clusterR /\ S -> X -valued ;
coherence
 R /\ S is X -valued
proofend;
clusterR \ S -> X -valued ;
coherence
 R \ S is X -valued ;
end;

definition
let X be set ;
let R be X -defined Relation;
:: original:dom
redefine func dom R ->  Subset of X;
coherence
 dom R is Subset of X by RELAT_1:def_18;
end;

definition
let X be set ;
let R be X -valued Relation;
:: original:rng
redefine func rng R ->  Subset of X;
coherence
 rng R is Subset of X by RELAT_1:def_19;
end;

theorem :: RELSET_1:8
for X, Y being set
for R being Relation of X,Y holds field R c= X \/ Y
proofend;

theorem :: RELSET_1:9
for Y, X being set
for R being Relation of X,Y holds
( ( for x being set st x in X holds
ex y being set st [x,y] in R ) iff dom R = X )
proofend;

theorem :: RELSET_1:10
for X, Y being set
for R being Relation of X,Y holds
( ( for y being set st y in Y holds
ex x being set st [x,y] in R ) iff rng R = Y )
proofend;

definition
let X, Y be set ;
let R be Relation of X,Y;
:: original:~
redefine funcR ~  ->  Relation of Y,X;
coherence
 R ~ is Relation of Y,X
proofend;
end;

definition
let X, Y1, Y2, Z be set ;
let P be Relation of X,Y1;
let R be Relation of Y2,Z;
:: original:*
redefine funcP * R ->  Relation of X,Z;
coherence
 P * R is Relation of X,Z
proofend;
end;

theorem :: RELSET_1:11
for X, Y being set
for R being Relation of X,Y holds
( dom (R ~) = rng R & rng (R ~) = dom R )
proofend;

theorem :: RELSET_1:12
for X, Y being set holds {} is Relation of X,Y by XBOOLE_1:2;

registration
let A be empty set ;
let B be set ;
cluster  ->  empty for Element of bool [:A,B:];
coherence
 for b1 being Relation of A,B holds b1 is empty ;
cluster  ->  empty for Element of bool [:B,A:];
coherence
 for b1 being Relation of B,A holds b1 is empty ;
end;

theorem Th13: :: RELSET_1:13
for X being set holds id X c= [:X,X:]
proofend;

theorem :: RELSET_1:14
for X being set holds id X is Relation of X,X by Th13;

theorem Th15: :: RELSET_1:15
for X, Y, A being set
for R being Relation of X,Y st id A c= R holds
( A c= dom R & A c= rng R )
proofend;

theorem :: RELSET_1:16
for Y, X being set
for R being Relation of X,Y st id X c= R holds
( X = dom R & X c= rng R )
proofend;

theorem :: RELSET_1:17
for X, Y being set
for R being Relation of X,Y st id Y c= R holds
( Y c= dom R & Y = rng R )
proofend;

definition
let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original:|
redefine funcR | A ->  Relation of X,Y;
coherence
 R | A is Relation of X,Y
proofend;
end;

definition
let X, Y, B be set ;
let R be Relation of X,Y;
:: original:|`
redefine funcB |` R ->  Relation of X,Y;
coherence
 B |` R is Relation of X,Y
proofend;
end;

theorem :: RELSET_1:18
for X, X1, Y being set
for R being Relation of X,Y holds R | X1 is Relation of X1,Y
proofend;

theorem :: RELSET_1:19
for Y, X, X1 being set
for R being Relation of X,Y st X c= X1 holds
R | X1 = R
proofend;

theorem :: RELSET_1:20
for Y, Y1, X being set
for R being Relation of X,Y holds Y1 |` R is Relation of X,Y1
proofend;

theorem :: RELSET_1:21
for X, Y, Y1 being set
for R being Relation of X,Y st Y c= Y1 holds
Y1 |` R = R
proofend;

definition
let X, Y be set ;
let R be Relation of X,Y;
let A be set ;
:: original:.:
redefine funcR .: A ->  Subset of Y;
coherence
 R .: A is Subset of Y
proofend;
:: original:"
redefine funcR " A ->  Subset of X;
coherence
 R " A is Subset of X
proofend;
end;

theorem Th22: :: RELSET_1:22
for X, Y being set
for R being Relation of X,Y holds
( R .: X = rng R & R " Y = dom R )
proofend;

theorem :: RELSET_1:23
for Y, X being set
for R being Relation of X,Y holds
( R .: (R " Y) = rng R & R " (R .: X) = dom R )
proofend;

scheme :: RELSET_1:sch 1
RelOnSetEx{ F1() ->  set , F2() ->  set , P1[ set , set ] } :
 ex R being Relation of F1(),F2() st
for x, y being set holds
( [x,y] in R iff ( x in F1() & y in F2() & P1[x,y] ) )
proofend;

:: Relation on a set
definition
let X be set ;
mode Relation of X is Relation of X,X;
end;

registration
let D be non empty set ;
cluster id D ->  non empty ;
coherence
 not id D is empty
proofend;
end;

theorem :: RELSET_1:24
for D, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in dom R iff ex y being Element of E st [x,y] in R )
proofend;

theorem :: RELSET_1:25
for E, D being non empty set
for R being Relation of D,E
for y being set holds
( y in rng R iff ex x being Element of D st [x,y] in R )
proofend;

theorem :: RELSET_1:26
for D, E being non empty set
for R being Relation of D,E st dom R <> {} holds
ex y being Element of E st y in rng R
proofend;

theorem :: RELSET_1:27
for E, D being non empty set
for R being Relation of D,E st rng R <> {} holds
ex x being Element of D st x in dom R
proofend;

theorem :: RELSET_1:28
for D, E, F being non empty set
for P being Relation of D,E
for R being Relation of E,F
for x, z being set holds
( [x,z] in P * R iff ex y being Element of E st
( [x,y] in P &amp; [y,z] in R ) )
proofend;

theorem :: RELSET_1:29
for E, D1, D being non empty set
for R being Relation of D,E
for y being Element of E holds
( y in R .: D1 iff ex x being Element of D st
( [x,y] in R &amp; x in D1 ) )
proofend;

theorem :: RELSET_1:30
for D, D2, E being non empty set
for R being Relation of D,E
for x being Element of D holds
( x in R " D2 iff ex y being Element of E st
( [x,y] in R &amp; y in D2 ) )
proofend;

scheme :: RELSET_1:sch 2
RelOnDomEx{ F1() ->  non empty set , F2() ->  non empty set , P1[ set , set ] } :
 ex R being Relation of F1(),F2() st
for x being Element of F1()
for y being Element of F2() holds
( [x,y] in R iff P1[x,y] )
proofend;

begin

scheme :: RELSET_1:sch 3
Sch3{ F1() ->  set , F2() ->  Subset of F1(), F3( set ) ->  set } :
 ex R being Relation of F2() st
for i being Element of F1() st i in F2() holds
Im (R,i) = F3(i)
provided
A1: for i being Element of F1() st i in F2() holds
F3(i) c= F2()
proofend;

theorem :: RELSET_1:31
for N being set
for R, S being Relation of N st ( for i being set st i in N holds
Im (R,i) = Im (S,i) ) holds
R = S
proofend;

scheme :: RELSET_1:sch 4
Sch4{ F1() ->  set , F2() ->  set , P1[ set , set ], F3() ->  Relation of F1(),F2(), F4() ->  Relation of F1(),F2() } :
 F3() = F4()
provided
A1: for p being Element of F1()
for q being Element of F2() holds
( [p,q] in F3() iff P1[p,q] ) and
A2: for p being Element of F1()
for q being Element of F2() holds
( [p,q] in F4() iff P1[p,q] )
proofend;

:: missing, 2007.06.14, A.T.
registration
let X, Y, Z be set ;
let f be Relation of [:X,Y:],Z;
cluster dom f ->  Relation-like ;
coherence
 dom f is Relation-like ;
end;

registration
let X, Y, Z be set ;
let f be Relation of X,[:Y,Z:];
cluster rng f ->  Relation-like ;
coherence
 rng f is Relation-like ;
end;

:: missing, 2008.04.30, A.T.
theorem :: RELSET_1:32
for Y, A, X being set
for P being Relation of X,Y st A misses X holds
P | A = {}
proofend;

:: missing, 2008.09.15, A.T.
registration
let R be non empty Relation;
let Y be non empty Subset of (dom R);
clusterR | Y ->  non empty ;
coherence
 not R | Y is empty
proofend;
end;

registration
let R be non empty Relation;
let Y be non empty Subset of (dom R);
clusterR .: Y ->  non empty ;
coherence
 not R .: Y is empty
proofend;
end;

:: missing, 2008.11.29 A.T.
registration
let X, Y be set ;
cluster empty Relation-like X -defined Y -valued for Element of bool [:X,Y:];
existence
 ex b1 being Relation of X,Y st b1 is empty
proofend;
end;