:: Relations and Their Basic Properties
:: by Edmund Woronowicz
::
:: Received March 15, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users

definition

let IT be set ;

attr IT is Relation-like means :Def1: :: RELAT_1:def 1
for x being object st x in IT holds
ex y, z being object st x = [y,z];

end;

:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :
for IT being set holds
( IT is Relation-like iff for x being object st x in IT holds
ex y, z being object st x = [y,z] );

registration

cluster empty -> Relation-like for set ;

coherence
for b₁ being set st b₁ is empty holds
b₁ is Relation-like ;

end;

definition

mode Relation is Relation-like set ;

end;

registration

let R be Relation;

cluster -> Relation-like for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is Relation-like by Def1;

end;

scheme :: RELAT_1:sch 1
RelExistence{ F₁() -> set , F₂() -> set , P₁[ object , object ] } :

ex R being Relation st
for x, y being object holds
( [x,y] in R iff ( x in F₁() & y in F₂() & P₁[x,y] ) )

proof end;

definition

let P, R be Relation;

redefine pred P = R means :: RELAT_1:def 2
for a, b being object holds
( [a,b] in P iff [a,b] in R );

compatibility
( P = R iff for a, b being object holds
( [a,b] in P iff [a,b] in R ) )

proof end;

end;

:: deftheorem defines = RELAT_1:def 2 :
for P, R being Relation holds
( P = R iff for a, b being object holds
( [a,b] in P iff [a,b] in R ) );

registration

let P be Relation;
let X be set ;

cluster P /\ X -> Relation-like ;

coherence
P /\ X is Relation-like

proof end;

cluster P \ X -> Relation-like ;

coherence
P \ X is Relation-like ;

end;

registration

let P, R be Relation;

cluster P \/ R -> Relation-like ;

coherence
P \/ R is Relation-like

proof end;

end;

registration

let R, S be Relation;

cluster R \+\ S -> Relation-like ;

coherence
R \+\ S is Relation-like ;

end;

registration

let a, b be object ;

cluster {[a,b]} -> Relation-like ;

coherence
{[a,b]} is Relation-like

proof end;

end;

registration

let a, b be set ;

cluster [:a,b:] -> Relation-like ;

coherence
[:a,b:] is Relation-like

proof end;

end;

registration

let a, b, c, d be object ;

cluster {[a,b],[c,d]} -> Relation-like ;

coherence
{[a,b],[c,d]} is Relation-like

proof end;

end;

definition

let P be Relation;
let A be set ;

redefine pred P c= A means :: RELAT_1:def 3
for a, b being object st [a,b] in P holds
[a,b] in A;

compatibility
( P c= A iff for a, b being object st [a,b] in P holds
[a,b] in A )

proof end;

end;

:: deftheorem defines c= RELAT_1:def 3 :
for P being Relation
for A being set holds
( P c= A iff for a, b being object st [a,b] in P holds
[a,b] in A );

notation

let R be Relation;
synonym dom R for proj1 R;

end;

notation

let R be Relation;
synonym rng R for proj2 R;

end;

theorem :: RELAT_1:1

canceled;

theorem :: RELAT_1:2

canceled;

theorem :: RELAT_1:3

canceled;

theorem :: RELAT_1:4

canceled;

theorem :: RELAT_1:5

canceled;

theorem :: RELAT_1:6

canceled;

::$CT 6

theorem Th1: :: RELAT_1:7

for R being Relation holds R c= [:(dom R),(rng R):]

proof end;

theorem :: RELAT_1:8

for R being Relation holds R /\ [:(dom R),(rng R):] = R by Th1, XBOOLE_1:28;

theorem Th3: :: RELAT_1:9

for x, y being object holds
( dom {[x,y]} = {x} & rng {[x,y]} = {y} )

proof end;

theorem :: RELAT_1:10

for a, b, x, y being object holds
( dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y} )

proof end;

theorem :: RELAT_1:11

for P, R being Relation st P c= R holds
( dom P c= dom R & rng P c= rng R ) by XTUPLE_0:8, XTUPLE_0:9;

theorem :: RELAT_1:12

for P, R being Relation holds rng (P \/ R) = (rng P) \/ (rng R) by XTUPLE_0:27;

theorem :: RELAT_1:13

for P, R being Relation holds rng (P /\ R) c= (rng P) /\ (rng R) by XTUPLE_0:28;

theorem :: RELAT_1:14

for P, R being Relation holds (rng P) \ (rng R) c= rng (P \ R) by XTUPLE_0:29;

:: FIELD OF RELATION

definition

let R be Relation;

func field R -> set equals :: RELAT_1:def 6
(dom R) \/ (rng R);

coherence
(dom R) \/ (rng R) is set ;

end;

:: deftheorem RELAT_1:def 4 :
canceled;

:: deftheorem RELAT_1:def 5 :
canceled;

:: deftheorem defines field RELAT_1:def 6 :
for R being Relation holds field R = (dom R) \/ (rng R);

theorem :: RELAT_1:15

for a, b being object
for R being Relation st [a,b] in R holds
( a in field R & b in field R )

proof end;

theorem :: RELAT_1:16

for P, R being Relation st P c= R holds
field P c= field R

proof end;

theorem Th11: :: RELAT_1:17

for x, y being object holds field {[x,y]} = {x,y}

proof end;

theorem :: RELAT_1:18

for P, R being Relation holds field (P \/ R) = (field P) \/ (field R)

proof end;

theorem :: RELAT_1:19

for P, R being Relation holds field (P /\ R) c= (field P) /\ (field R)

proof end;

:: CONVERSE RELATION

definition

let R be Relation;

func R ~ -> Relation means :Def5: :: RELAT_1:def 7
for x, y being object holds
( [x,y] in it iff [y,x] in R );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff [y,x] in R )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff [y,x] in R ) ) & ( for x, y being object holds
( [x,y] in b₂ iff [y,x] in R ) ) holds
b₁ = b₂

proof end;

involutiveness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff [y,x] in b₂ ) ) holds
for x, y being object holds
( [x,y] in b₂ iff [y,x] in b₁ ) ;

end;

:: deftheorem Def5 defines ~ RELAT_1:def 7 :
for R, b₂ being Relation holds
( b₂ = R ~ iff for x, y being object holds
( [x,y] in b₂ iff [y,x] in R ) );

theorem Th14: :: RELAT_1:20

for R being Relation holds
( rng R = dom (R ~) & dom R = rng (R ~) )

proof end;

theorem :: RELAT_1:21

for R being Relation holds field R = field (R ~)

proof end;

theorem :: RELAT_1:22

for P, R being Relation holds (P /\ R) ~ = (P ~) /\ (R ~)

proof end;

theorem :: RELAT_1:23

for P, R being Relation holds (P \/ R) ~ = (P ~) \/ (R ~)

proof end;

theorem :: RELAT_1:24

for P, R being Relation holds (P \ R) ~ = (P ~) \ (R ~)

proof end;

:: COMPOSITION OF RELATIONS

definition

let P, R be set ;

func P (#) R -> Relation means :Def6: :: RELAT_1:def 8
for x, y being object holds
( [x,y] in it iff ex z being object st
( [x,z] in P & [z,y] in R ) );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff ex z being object st
( [x,z] in P & [z,y] in R ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff ex z being object st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ex z being object st
( [x,z] in P & [z,y] in R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines (#) RELAT_1:def 8 :
for P, R being set
for b₃ being Relation holds
( b₃ = P (#) R iff for x, y being object holds
( [x,y] in b₃ iff ex z being object st
( [x,z] in P & [z,y] in R ) ) );

notation

let P, R be Relation;
synonym P * R for P (#) R;

end;

theorem Th19: :: RELAT_1:25

for P, R being Relation holds dom (P * R) c= dom P

proof end;

theorem Th20: :: RELAT_1:26

for P, R being Relation holds rng (P * R) c= rng R

proof end;

theorem :: RELAT_1:27

for P, R being Relation st rng R c= dom P holds
dom (R * P) = dom R

proof end;

theorem :: RELAT_1:28

for P, R being Relation st dom P c= rng R holds
rng (R * P) = rng P

proof end;

theorem Th23: :: RELAT_1:29

for P, Q, R being Relation st P c= R holds
Q * P c= Q * R

proof end;

theorem Th24: :: RELAT_1:30

for P, Q, R being Relation st P c= Q holds
P * R c= Q * R

proof end;

theorem :: RELAT_1:31

for P, Q, R, S being Relation st P c= R & Q c= S holds
P * Q c= R * S

proof end;

theorem :: RELAT_1:32

for P, Q, R being Relation holds P * (R \/ Q) = (P * R) \/ (P * Q)

proof end;

theorem :: RELAT_1:33

for P, Q, R being Relation holds P * (R /\ Q) c= (P * R) /\ (P * Q)

proof end;

theorem :: RELAT_1:34

for P, Q, R being Relation holds (P * R) \ (P * Q) c= P * (R \ Q)

proof end;

theorem :: RELAT_1:35

for P, R being Relation holds (P * R) ~ = (R ~) * (P ~)

proof end;

theorem Th30: :: RELAT_1:36

for P, Q, R being Relation holds (P * R) * Q = P * (R * Q)

proof end;

:: EMPTY RELATION

registration

cluster non empty Relation-like for set ;

existence
not for b₁ being Relation holds b₁ is empty

proof end;

end;

registration

let f be non empty Relation;

cluster dom f -> non empty ;

coherence
not dom f is empty

proof end;

cluster rng f -> non empty ;

coherence
not rng f is empty

proof end;

end;

theorem Th31: :: RELAT_1:37

for R being Relation st ( for x, y being object holds not [x,y] in R ) holds
R = {} ;

theorem Th32: :: RELAT_1:38

( dom {} = {} & rng {} = {} ) ;

theorem Th33: :: RELAT_1:39

for R being Relation holds
( {} * R = {} & R * {} = {} )

proof end;

registration

let X be empty set ;

cluster dom X -> empty ;

coherence
dom X is empty ;

cluster rng X -> empty ;

coherence
rng X is empty ;
let R be Relation;

cluster X (#) R -> empty ;

coherence
X * R is empty by Th33;

cluster R (#) X -> empty ;

coherence
R * X is empty by Th33;

end;

theorem :: RELAT_1:40

field {} = {} ;

theorem Th35: :: RELAT_1:41

for R being Relation st ( dom R = {} or rng R = {} ) holds
R = {} ;

theorem :: RELAT_1:42

for R being Relation holds
( dom R = {} iff rng R = {} ) by Th32, Th35;

registration

let X be empty set ;

cluster X ~ -> empty ;

coherence
X ~ is empty

proof end;

end;

theorem :: RELAT_1:43

{} ~ = {} ;

theorem :: RELAT_1:44

for P, R being Relation st rng R misses dom P holds
R * P = {}

proof end;

definition

let R be Relation;

attr R is non-empty means :Def7: :: RELAT_1:def 9
not {} in rng R;

end;

:: deftheorem Def7 defines non-empty RELAT_1:def 9 :
for R being Relation holds
( R is non-empty iff not {} in rng R );

registration

cluster Relation-like non-empty for set ;

existence
ex b₁ being Relation st b₁ is non-empty

proof end;

end;

registration

let R be Relation;
let S be non-empty Relation;

cluster R (#) S -> non-empty ;

coherence
R * S is non-empty

proof end;

end;

:: IDENTITY RELATION

definition

let X be set ;

func id X -> Relation means :Def8: :: RELAT_1:def 10
for x, y being object holds
( [x,y] in it iff ( x in X & x = y ) );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff ( x in X & x = y ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff ( x in X & x = y ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( x in X & x = y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines id RELAT_1:def 10 :
for X being set
for b₂ being Relation holds
( b₂ = id X iff for x, y being object holds
( [x,y] in b₂ iff ( x in X & x = y ) ) );

registration

let X be set ;

reduce dom (id X) to X;

reducibility
dom (id X) = X

proof end;

reduce rng (id X) to X;

reducibility
rng (id X) = X

proof end;

end;

theorem :: RELAT_1:45

for X being set holds
( dom (id X) = X & rng (id X) = X ) ;

registration

let X be set ;

reduce (id X) ~ to id X;

reducibility
(id X) ~ = id X

proof end;

end;

theorem :: RELAT_1:46

for X being set holds (id X) ~ = id X ;

theorem :: RELAT_1:47

for X being set
for R being Relation st ( for x being object st x in X holds
[x,x] in R ) holds
id X c= R

proof end;

theorem Th42: :: RELAT_1:48

for X being set
for x, y being object
for R being Relation holds
( [x,y] in (id X) * R iff ( x in X & [x,y] in R ) )

proof end;

theorem Th43: :: RELAT_1:49

for Y being set
for x, y being object
for R being Relation holds
( [x,y] in R * (id Y) iff ( y in Y & [x,y] in R ) )

proof end;

theorem Th44: :: RELAT_1:50

for X being set
for R being Relation holds
( R * (id X) c= R & (id X) * R c= R )

proof end;

theorem Th45: :: RELAT_1:51

for X being set
for R being Relation st dom R c= X holds
(id X) * R = R

proof end;

theorem :: RELAT_1:52

for R being Relation holds (id (dom R)) * R = R by Th45;

theorem Th47: :: RELAT_1:53

for Y being set
for R being Relation st rng R c= Y holds
R * (id Y) = R

proof end;

theorem :: RELAT_1:54

for R being Relation holds R * (id (rng R)) = R by Th47;

theorem :: RELAT_1:55

id {} = {}

proof end;

theorem :: RELAT_1:56

for X being set
for P1, P2, R being Relation st rng P2 c= X & P2 * R = id (dom P1) & R * P1 = id X holds
P1 = P2

proof end;

definition

let R be Relation;
let X be set ;

func R | X -> Relation means :Def9: :: RELAT_1:def 11
for x, y being object holds
( [x,y] in it iff ( x in X & [x,y] in R ) );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff ( x in X & [x,y] in R ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff ( x in X & [x,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( x in X & [x,y] in R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines | RELAT_1:def 11 :
for R being Relation
for X being set
for b₃ being Relation holds
( b₃ = R | X iff for x, y being object holds
( [x,y] in b₃ iff ( x in X & [x,y] in R ) ) );

registration

let R be Relation;
let X be empty set ;

cluster R | X -> empty ;

coherence
R | X is empty

proof end;

end;

theorem Th51: :: RELAT_1:57

for X being set
for x being object
for R being Relation holds
( x in dom (R | X) iff ( x in X & x in dom R ) )

proof end;

theorem :: RELAT_1:58

for X being set
for R being Relation holds dom (R | X) c= X by Th51;

theorem Th53: :: RELAT_1:59

for X being set
for R being Relation holds R | X c= R by Def9;

theorem :: RELAT_1:60

for X being set
for R being Relation holds dom (R | X) c= dom R by Th51;

theorem Th55: :: RELAT_1:61

for X being set
for R being Relation holds dom (R | X) = (dom R) /\ X

proof end;

theorem :: RELAT_1:62

for X being set
for R being Relation st X c= dom R holds
dom (R | X) = X

proof end;

theorem :: RELAT_1:63

for X being set
for P, R being Relation holds (R | X) * P c= R * P by Th24, Th53;

theorem :: RELAT_1:64

for X being set
for P, R being Relation holds P * (R | X) c= P * R by Th23, Th53;

theorem :: RELAT_1:65

for X being set
for R being Relation holds R | X = (id X) * R

proof end;

theorem :: RELAT_1:66

for X being set
for R being Relation holds
( R | X = {} iff dom R misses X )

proof end;

theorem Th61: :: RELAT_1:67

for X being set
for R being Relation holds R | X = R /\ [:X,(rng R):]

proof end;

theorem Th62: :: RELAT_1:68

for X being set
for R being Relation st dom R c= X holds
R | X = R

proof end;

registration

let R be Relation;

reduce R | (dom R) to R;

reducibility
R | (dom R) = R by Th62;

end;

theorem :: RELAT_1:69

for R being Relation holds R | (dom R) = R ;

theorem :: RELAT_1:70

for X being set
for R being Relation holds rng (R | X) c= rng R by Th53, XTUPLE_0:9;

theorem Th65: :: RELAT_1:71

for X, Y being set
for R being Relation holds (R | X) | Y = R | (X /\ Y)

proof end;

registration

let R be Relation;
let X be set ;

reduce (R | X) | X to R | X;

reducibility
(R | X) | X = R | X

proof end;

end;

theorem :: RELAT_1:72

for X being set
for R being Relation holds (R | X) | X = R | X ;

theorem :: RELAT_1:73

for X, Y being set
for R being Relation st X c= Y holds
(R | X) | Y = R | X

proof end;

theorem :: RELAT_1:74

for X, Y being set
for R being Relation st Y c= X holds
(R | X) | Y = R | Y

proof end;

theorem Th69: :: RELAT_1:75

for X, Y being set
for R being Relation st X c= Y holds
R | X c= R | Y

proof end;

theorem Th70: :: RELAT_1:76

for X being set
for P, R being Relation st P c= R holds
P | X c= R | X

proof end;

theorem Th71: :: RELAT_1:77

for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P | X c= R | Y

proof end;

theorem Th72: :: RELAT_1:78

for X, Y being set
for R being Relation holds R | (X \/ Y) = (R | X) \/ (R | Y)

proof end;

theorem :: RELAT_1:79

for X, Y being set
for R being Relation holds R | (X /\ Y) = (R | X) /\ (R | Y)

proof end;

theorem Th74: :: RELAT_1:80

for X, Y being set
for R being Relation holds R | (X \ Y) = (R | X) \ (R | Y)

proof end;

registration

let R be empty Relation;
let X be set ;

cluster R | X -> empty ;

coherence
R | X is empty

proof end;

end;

theorem :: RELAT_1:81

for R being Relation holds R | {} = {} ;

theorem :: RELAT_1:82

for X being set holds {} | X = {} ;

theorem :: RELAT_1:83

for X being set
for P, R being Relation holds (P * R) | X = (P | X) * R

proof end;

definition

let Y be set ;
let R be Relation;

func Y |` R -> Relation means :Def10: :: RELAT_1:def 12
for x, y being object holds
( [x,y] in it iff ( y in Y & [x,y] in R ) );

existence
ex b₁ being Relation st
for x, y being object holds
( [x,y] in b₁ iff ( y in Y & [x,y] in R ) )

proof end;

uniqueness
for b₁, b₂ being Relation st ( for x, y being object holds
( [x,y] in b₁ iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being object holds
( [x,y] in b₂ iff ( y in Y & [x,y] in R ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines |` RELAT_1:def 12 :
for Y being set
for R, b<sub>3</sub> being Relation holds
( b<sub>3</sub> = Y |` R iff for x, y being object holds
( [x,y] in b₃ iff ( y in Y & [x,y] in R ) ) );

registration

let R be Relation;
let X be empty set ;

cluster X |` R -> empty ;

coherence
X |` R is empty

proof end;

end;

theorem Th78: :: RELAT_1:84

for Y being set
for y being object
for R being Relation holds
( y in rng (Y |` R) iff ( y in Y & y in rng R ) )

proof end;

theorem :: RELAT_1:85

for Y being set
for R being Relation holds rng (Y |` R) c= Y by Th78;

theorem Th80: :: RELAT_1:86

for Y being set
for R being Relation holds Y |` R c= R by Def10;

theorem :: RELAT_1:87

for Y being set
for R being Relation holds rng (Y |` R) c= rng R by Th80, XTUPLE_0:9;

theorem Th82: :: RELAT_1:88

for Y being set
for R being Relation holds rng (Y |` R) = (rng R) /\ Y

proof end;

theorem :: RELAT_1:89

for Y being set
for R being Relation st Y c= rng R holds
rng (Y |` R) = Y

proof end;

theorem :: RELAT_1:90

for Y being set
for P, R being Relation holds (Y |` R) * P c= R * P by Th24, Th80;

theorem :: RELAT_1:91

for Y being set
for P, R being Relation holds P * (Y |` R) c= P * R by Th23, Th80;

theorem :: RELAT_1:92

for Y being set
for R being Relation holds Y |` R = R * (id Y)

proof end;

theorem Th87: :: RELAT_1:93

for Y being set
for R being Relation holds Y |` R = R /\ [:(dom R),Y:]

proof end;

theorem Th88: :: RELAT_1:94

for Y being set
for R being Relation st rng R c= Y holds
Y |` R = R

proof end;

registration

let R be Relation;

reduce (rng R) |` R to R;

reducibility
(rng R) |` R = R by Th88;

end;

theorem :: RELAT_1:95

for R being Relation holds (rng R) |` R = R ;

theorem Th90: :: RELAT_1:96

for X, Y being set
for R being Relation holds Y |` (X |` R) = (Y /\ X) |` R

proof end;

registration

let Y be set ;
let R be Relation;

reduce Y |` (Y |` R) to Y |` R;

reducibility
Y |` (Y |` R) = Y |` R

proof end;

end;

theorem :: RELAT_1:97

for Y being set
for R being Relation holds Y |` (Y |` R) = Y |` R ;

theorem :: RELAT_1:98

for X, Y being set
for R being Relation st X c= Y holds
Y |` (X |` R) = X |` R

proof end;

theorem :: RELAT_1:99

for X, Y being set
for R being Relation st Y c= X holds
Y |` (X |` R) = Y |` R

proof end;

theorem Th94: :: RELAT_1:100

for X, Y being set
for R being Relation st X c= Y holds
X |` R c= Y |` R

proof end;

theorem Th95: :: RELAT_1:101

for Y being set
for P1, P2 being Relation st P1 c= P2 holds
Y |` P1 c= Y |` P2

proof end;

theorem :: RELAT_1:102

for Y1, Y2 being set
for P1, P2 being Relation st P1 c= P2 & Y1 c= Y2 holds
Y1 |` P1 c= Y2 |` P2

proof end;

theorem :: RELAT_1:103

for X, Y being set
for R being Relation holds (X \/ Y) |` R = (X |` R) \/ (Y |` R)

proof end;

theorem :: RELAT_1:104

for X, Y being set
for R being Relation holds (X /\ Y) |` R = (X |` R) /\ (Y |` R)

proof end;

theorem :: RELAT_1:105

for X, Y being set
for R being Relation holds (X \ Y) |` R = (X |` R) \ (Y |` R)

proof end;

theorem :: RELAT_1:106

for R being Relation holds {} |` R = {} ;

theorem :: RELAT_1:107

for Y being set holds Y |` {} = {} by Def10;

theorem :: RELAT_1:108

for Y being set
for P, R being Relation holds Y |` (P * R) = P * (Y |` R)

proof end;

theorem :: RELAT_1:109

for X, Y being set
for R being Relation holds (Y |` R) | X = Y |` (R | X)

proof end;

:: IMAGE OF SET IN RELATION

definition

let R be Relation;
let X be set ;

func R .: X -> set means :Def11: :: RELAT_1:def 13
for y being object holds
( y in it iff ex x being object st
( [x,y] in R & x in X ) );

existence
ex b₁ being set st
for y being object holds
( y in b₁ iff ex x being object st
( [x,y] in R & x in X ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for y being object holds
( y in b₁ iff ex x being object st
( [x,y] in R & x in X ) ) ) & ( for y being object holds
( y in b₂ iff ex x being object st
( [x,y] in R & x in X ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def11 defines .: RELAT_1:def 13 :
for R being Relation
for X, b₃ being set holds
( b₃ = R .: X iff for y being object holds
( y in b₃ iff ex x being object st
( [x,y] in R & x in X ) ) );

theorem Th104: :: RELAT_1:110

for X being set
for y being object
for R being Relation holds
( y in R .: X iff ex x being object st
( x in dom R & [x,y] in R & x in X ) )

proof end;

theorem Th105: :: RELAT_1:111

for X being set
for R being Relation holds R .: X c= rng R

proof end;

theorem :: RELAT_1:112

for X being set
for R being Relation holds R .: X = R .: ((dom R) /\ X)

proof end;

theorem Th107: :: RELAT_1:113

for R being Relation holds R .: (dom R) = rng R

proof end;

theorem :: RELAT_1:114

for X being set
for R being Relation holds R .: X c= R .: (dom R)

proof end;

theorem :: RELAT_1:115

for X being set
for R being Relation holds rng (R | X) = R .: X

proof end;

registration

let R be Relation;
let X be empty set ;

cluster R .: X -> empty ;

coherence
R .: X is empty

proof end;

end;

registration

let R be empty Relation;
let X be set ;

cluster R .: X -> empty ;

coherence
R .: X is empty

proof end;

end;

theorem :: RELAT_1:116

canceled;

theorem :: RELAT_1:117

canceled;

::$CT 2

theorem :: RELAT_1:118

for X being set
for R being Relation holds
( R .: X = {} iff dom R misses X )

proof end;

theorem :: RELAT_1:119

for X being set
for R being Relation st X <> {} & X c= dom R holds
R .: X <> {}

proof end;

theorem :: RELAT_1:120

for X, Y being set
for R being Relation holds R .: (X \/ Y) = (R .: X) \/ (R .: Y)

proof end;

theorem :: RELAT_1:121

for X, Y being set
for R being Relation holds R .: (X /\ Y) c= (R .: X) /\ (R .: Y)

proof end;

theorem :: RELAT_1:122

for X, Y being set
for R being Relation holds (R .: X) \ (R .: Y) c= R .: (X \ Y)

proof end;

theorem Th115: :: RELAT_1:123

for X, Y being set
for R being Relation st X c= Y holds
R .: X c= R .: Y

proof end;

theorem Th116: :: RELAT_1:124

for X being set
for P, R being Relation st P c= R holds
P .: X c= R .: X

proof end;

theorem :: RELAT_1:125

for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P .: X c= R .: Y

proof end;

theorem :: RELAT_1:126

for X being set
for P, R being Relation holds (P * R) .: X = R .: (P .: X)

proof end;

theorem Th119: :: RELAT_1:127

for P, R being Relation holds rng (P * R) = R .: (rng P)

proof end;

theorem :: RELAT_1:128

for X, Y being set
for R being Relation holds (R | X) .: Y c= R .: Y by Th53, Th116;

theorem Th121: :: RELAT_1:129

for R being Relation
for X, Y being set st X c= Y holds
(R | Y) .: X = R .: X

proof end;

theorem :: RELAT_1:130

for X being set
for R being Relation holds (dom R) /\ X c= (R ~) .: (R .: X)

proof end;

:: INVERSE IMAGE OF SET IN RELATION

definition

let R be Relation;
let Y be set ;

func R " Y -> set means :Def12: :: RELAT_1:def 14
for x being object holds
( x in it iff ex y being object st
( [x,y] in R & y in Y ) );

existence
ex b₁ being set st
for x being object holds
( x in b₁ iff ex y being object st
( [x,y] in R & y in Y ) )

proof end;

uniqueness
for b₁, b₂ being set st ( for x being object holds
( x in b₁ iff ex y being object st
( [x,y] in R & y in Y ) ) ) & ( for x being object holds
( x in b₂ iff ex y being object st
( [x,y] in R & y in Y ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines " RELAT_1:def 14 :
for R being Relation
for Y, b₃ being set holds
( b₃ = R " Y iff for x being object holds
( x in b₃ iff ex y being object st
( [x,y] in R & y in Y ) ) );

theorem Th123: :: RELAT_1:131

for Y being set
for x being object
for R being Relation holds
( x in R " Y iff ex y being object st
( y in rng R & [x,y] in R & y in Y ) )

proof end;

theorem Th124: :: RELAT_1:132

for Y being set
for R being Relation holds R " Y c= dom R

proof end;

theorem :: RELAT_1:133

for Y being set
for R being Relation holds R " Y = R " ((rng R) /\ Y)

proof end;

theorem Th126: :: RELAT_1:134

for R being Relation holds R " (rng R) = dom R

proof end;

theorem :: RELAT_1:135

for Y being set
for R being Relation holds R " Y c= R " (rng R)

proof end;

registration

let R be Relation;
let Y be empty set ;

cluster R " Y -> empty ;

coherence
R " Y is empty

proof end;

end;

registration

let R be empty Relation;
let Y be set ;

cluster R " Y -> empty ;

coherence
R " Y is empty

proof end;

end;

theorem :: RELAT_1:136

canceled;

theorem :: RELAT_1:137

canceled;

::$CT 2

theorem :: RELAT_1:138

for Y being set
for R being Relation holds
( R " Y = {} iff rng R misses Y )

proof end;

theorem :: RELAT_1:139

for Y being set
for R being Relation st Y <> {} & Y c= rng R holds
R " Y <> {}

proof end;

theorem :: RELAT_1:140

for X, Y being set
for R being Relation holds R " (X \/ Y) = (R " X) \/ (R " Y)

proof end;

theorem :: RELAT_1:141

for X, Y being set
for R being Relation holds R " (X /\ Y) c= (R " X) /\ (R " Y)

proof end;

theorem :: RELAT_1:142

for X, Y being set
for R being Relation holds (R " X) \ (R " Y) c= R " (X \ Y)

proof end;

theorem Th133: :: RELAT_1:143

for X, Y being set
for R being Relation st X c= Y holds
R " X c= R " Y

proof end;

theorem Th134: :: RELAT_1:144

for Y being set
for P, R being Relation st P c= R holds
P " Y c= R " Y

proof end;

theorem :: RELAT_1:145

for X, Y being set
for P, R being Relation st P c= R & X c= Y holds
P " X c= R " Y

proof end;

theorem :: RELAT_1:146

for Y being set
for P, R being Relation holds (P * R) " Y = P " (R " Y)

proof end;

theorem Th137: :: RELAT_1:147

for P, R being Relation holds dom (P * R) = P " (dom R)

proof end;

theorem :: RELAT_1:148

for Y being set
for R being Relation holds (rng R) /\ Y c= (R ~) " (R " Y)

proof end;

definition

let R be Relation;

attr R is empty-yielding means :Def13: :: RELAT_1:def 15
rng R c= {{}};

end;

:: deftheorem Def13 defines empty-yielding RELAT_1:def 15 :
for R being Relation holds
( R is empty-yielding iff rng R c= {{}} );

theorem :: RELAT_1:149

for R being Relation holds
( R is empty-yielding iff for X being set st X in rng R holds
X = {} )

proof end;

:: from AMI_3

theorem :: RELAT_1:150

for f, g being Relation
for A, B being set st f | A = g | A & f | B = g | B holds
f | (A \/ B) = g | (A \/ B)

proof end;

theorem :: RELAT_1:151

for X being set
for f, g being Relation st dom g c= X & g c= f holds
g c= f | X

proof end;

theorem :: RELAT_1:152

for f being Relation
for X being set st X misses dom f holds
f | X = {}

proof end;

:: from AMI_5

theorem :: RELAT_1:153

for f, g being Relation
for A, B being set st A c= B & f | B = g | B holds
f | A = g | A

proof end;

:: missing, 2005.07.11, A.T.

theorem :: RELAT_1:154

for R, S being Relation holds R | (dom S) = R | (dom (S | (dom R)))

proof end;

:: missing, 2005.11.13, A.T.

registration

cluster empty Relation-like -> empty-yielding for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is empty-yielding

proof end;

end;

registration

let R be empty-yielding Relation;
let X be set ;

cluster R | X -> empty-yielding ;

coherence
R | X is empty-yielding

proof end;

end;

theorem :: RELAT_1:155

for X being set
for R being Relation st not R | X is empty-yielding holds
not R is empty-yielding ;

:: from EQREL_1 (Class), 2007.02.06

definition

let R be Relation;
let x be object ;

func Im (R,x) -> set equals :: RELAT_1:def 16
R .: {x};

correctness
coherence
R .: {x} is set ;
;

end;

:: deftheorem defines Im RELAT_1:def 16 :
for R being Relation
for x being object holds Im (R,x) = R .: {x};

:: from YELLOW_3, 2007.06.13, A.T.

scheme :: RELAT_1:sch 2
ExtensionalityR{ F₁() -> Relation, F₂() -> Relation, P₁[ object , object ] } :

F₁() = F₂()

provided

A1: for a, b being object holds
( [a,b] in F₁() iff P₁[a,b] ) and
A2: for a, b being object holds
( [a,b] in F₂() iff P₁[a,b] )

proof end;

:: from SCMFSA6A, 2007.07.23, A.T.

theorem :: RELAT_1:156

for X being set
for R being Relation holds dom (R | ((dom R) \ X)) = (dom R) \ X

proof end;

theorem :: RELAT_1:157

for X being set
for R being Relation holds R | X = R | ((dom R) /\ X)

proof end;

:: missing, 2007.11.07, A.T.

theorem :: RELAT_1:158

for X, Y being set holds dom [:X,Y:] c= X

proof end;

theorem :: RELAT_1:159

for X, Y being set holds rng [:X,Y:] c= Y

proof end;

:: from FUNCOP_1, 2008.02.19, A.T.

theorem :: RELAT_1:160

for X, Y being set st X <> {} & Y <> {} holds
( dom [:X,Y:] = X & rng [:X,Y:] = Y )

proof end;

theorem :: RELAT_1:161

for Q, R being Relation st dom R = {} & dom Q = {} holds
R = Q ;

theorem :: RELAT_1:162

for Q, R being Relation st rng R = {} & rng Q = {} holds
R = Q ;

theorem :: RELAT_1:163

for Q, R, S being Relation st dom R = dom Q holds
dom (S * R) = dom (S * Q)

proof end;

theorem :: RELAT_1:164

for Q, R, S being Relation st rng R = rng Q holds
rng (R * S) = rng (Q * S)

proof end;

:: from RELSET_2 (R"x, generalized), 2008.07.16, A.T.

definition

let R be Relation;
let x be object ;

func Coim (R,x) -> set equals :: RELAT_1:def 17
R " {x};

coherence
R " {x} is set ;

end;

:: deftheorem defines Coim RELAT_1:def 17 :
for R being Relation
for x being object holds Coim (R,x) = R " {x};

:: from NECKLACE, 2008.07.25, A.T.

registration

let R be trivial Relation;

cluster dom R -> trivial ;

coherence
dom R is trivial

proof end;

end;

registration

let R be trivial Relation;

cluster rng R -> trivial ;

coherence
rng R is trivial

proof end;

end;

:: comp. RFUNCT_2:34, CFCONT_1:31, 2008.08.07, A.T.

theorem :: RELAT_1:165

for X being set
for R, S being Relation st rng R c= dom (S | X) holds
R * (S | X) = R * S

proof end;

:: from LATTICE2, 2008.09.14, A.T.

theorem :: RELAT_1:166

for A being set
for Q, R being Relation st Q | A = R | A holds
Q .: A = R .: A

proof end;

:: new, 2009.01.21, A.T

definition

let X be set ;
let R be Relation;

attr R is X -defined means :Def16: :: RELAT_1:def 18
dom R c= X;

attr R is X -valued means :Def17: :: RELAT_1:def 19
rng R c= X;

end;

:: deftheorem Def16 defines -defined RELAT_1:def 18 :
for X being set
for R being Relation holds
( R is X -defined iff dom R c= X );

:: deftheorem Def17 defines -valued RELAT_1:def 19 :
for X being set
for R being Relation holds
( R is X -valued iff rng R c= X );

Lm1: for X, Y being set holds
( {} is X -defined & {} is Y -valued )

proof end;

registration

let X, Y be set ;

cluster Relation-like X -defined Y -valued for set ;

existence
ex b₁ being Relation st
( b₁ is X -defined & b₁ is Y -valued )

proof end;

end;

:: from QC_LANG4, 2009.01.23, A.T

theorem :: RELAT_1:167

for D being set
for R being b₁ -valued Relation
for y being object st y in rng R holds
y in D

proof end;

:: new, 2009.02.07, A.T.

registration

let X, A be set ;
let R be A -valued Relation;

cluster R | X -> A -valued ;

coherence
R | X is A -valued

proof end;

end;

registration

let X, A be set ;
let R be A -defined Relation;

cluster R | X -> X -defined A -defined ;

coherence
( R | X is A -defined & R | X is X -defined )

proof end;

end;

registration

let X be set ;

cluster id X -> X -defined X -valued ;

coherence
( id X is X -defined & id X is X -valued ) ;

end;

:: 2009.02.16, A.T.

registration

let A be set ;
let R be A -valued Relation;
let S be Relation;

cluster S (#) R -> A -valued ;

coherence
S * R is A -valued

proof end;

end;

registration

let A be set ;
let R be A -defined Relation;
let S be Relation;

cluster R (#) S -> A -defined ;

coherence
R * S is A -defined

proof end;

end;

:: 2009.02.16, A.T.

theorem :: RELAT_1:168

for X, Y being set
for x being object st x in X holds
Im ([:X,Y:],x) = Y

proof end;

theorem Th159: :: RELAT_1:169

for x, y being object
for R being Relation holds
( [x,y] in R iff y in Im (R,x) )

proof end;

theorem :: RELAT_1:170

for x being object
for R being Relation holds
( x in dom R iff Im (R,x) <> {} )

proof end;

theorem :: RELAT_1:171

for X, Y being set holds
( {} is X -defined & {} is Y -valued ) by Lm1;

:: 2009.10.02, A.T.

registration

cluster empty Relation-like -> non-empty for set ;

coherence
for b₁ being Relation st b₁ is empty holds
b₁ is non-empty ;

end;

registration

let X be set ;
let R be X -defined Relation;

cluster -> X -defined for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is X -defined

proof end;

end;

registration

let X be set ;
let R be X -valued Relation;

cluster -> X -valued for Element of bool R;

coherence
for b₁ being Subset of R holds b₁ is X -valued

proof end;

end;

:: missing, 2010.01.02, A.T

theorem :: RELAT_1:172

for X, Y being set
for R being Relation st X misses Y holds
(R | X) | Y = {}

proof end;

:: from AMISTD_3, 2010.01.10, A.T.

theorem :: RELAT_1:173

for x being object holds field {[x,x]} = {x}

proof end;

registration

let X be set ;
let R be X -defined Relation;

reduce R | X to R;

reducibility
R | X = R

proof end;

end;

registration

let Y be set ;
let R be Y -valued Relation;

reduce Y |` R to R;

reducibility
Y |` R = R

proof end;

end;

theorem :: RELAT_1:174

for X being set
for R being b₁ -defined Relation holds R = R | X ;

theorem :: RELAT_1:175

for X being set
for S being Relation
for R being b₁ -defined Relation st R c= S holds
R c= S | X

proof end;

:: missing, 2010.04.07, A.T.

theorem Th166: :: RELAT_1:176

for A, X being set
for R being Relation st dom R c= X holds
R \ (R | A) = R | (X \ A)

proof end;

theorem Th167: :: RELAT_1:177

for A being set
for R being Relation holds dom (R \ (R | A)) = (dom R) \ A

proof end;

theorem :: RELAT_1:178

for A being set
for R being Relation holds (dom R) \ (dom (R | A)) = dom (R \ (R | A))

proof end;

theorem Th169: :: RELAT_1:179

for R, S being Relation st dom R misses dom S holds
R misses S

proof end;

theorem :: RELAT_1:180

for R, S being Relation st rng R misses rng S holds
R misses S

proof end;

theorem :: RELAT_1:181

for X, Y being set
for R being Relation st X c= Y holds
(R \ (R | Y)) | X = {}

proof end;

theorem :: RELAT_1:182

for X, Y being set st X c= Y holds
for R being b₁ -defined Relation holds R is Y -defined

proof end;

theorem :: RELAT_1:183

for X, Y being set st X c= Y holds
for R being b₁ -valued Relation holds R is Y -valued

proof end;

theorem :: RELAT_1:184

for R, S being Relation holds
( R c= S iff R c= S | (dom R) )

proof end;

theorem Th175: :: RELAT_1:185

for X, Y being set
for R being b₁ -defined b₂ -valued Relation holds R c= [:X,Y:]

proof end;

:: new, 20011.06.11, A.T.

theorem :: RELAT_1:186

for X being set
for R being Relation holds dom (X |` R) c= dom R by Th80, XTUPLE_0:8;

registration

let A, X be set ;
let R be A -defined Relation;

cluster X |` R -> A -defined ;

coherence
X |` R is A -defined

proof end;

end;

registration

let X, A be set ;
let R be A -valued Relation;

cluster X |` R -> X -valued A -valued ;

coherence
( X |` R is A -valued & X |` R is X -valued )

proof end;

end;

registration

let X be empty set ;

cluster Relation-like X -defined -> empty X -defined for set ;

coherence
for b₁ being X -defined Relation holds b₁ is empty

proof end;

cluster Relation-like X -valued -> empty X -valued for set ;

coherence
for b₁ being X -valued Relation holds b₁ is empty

proof end;

end;

:: from PNPROC_1, 2012.02.20, A.T.

theorem :: RELAT_1:187

for X, Y being set
for P, R being Relation st X misses Y holds
P | X misses R | Y

proof end;

theorem :: RELAT_1:188

for Y being set
for R being Relation holds Y |` R c= R | (R " Y)

proof end;

theorem :: RELAT_1:189

for f being Relation
for x, y being object st dom f = {x} & rng f = {y} holds
f = {[x,y]}

proof end;

registration

let X, Y be set ;
let a₁ be set , a₂ be set ;
a₁ -defined a₂ -valued Relation ex b₁ being set st
for b₂ being X -defined Y -valued Relation holds b₂ in b₁

proof end;

end;