:: RELAT_1 semantic presentation

definition

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

end;

:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :

registration

cluster empty Relation-like set ;
existence

proof end;

end;

definition

mode Relation is Relation-like set ;

end;

theorem :: RELAT_1:1

canceled;

theorem :: RELAT_1:2

canceled;

theorem Th3: :: RELAT_1:3

for A being set
for R being Relation st A c= R holds
A is Relation-like

proof end;

theorem Th4: :: RELAT_1:4

for x, y being set holds {[x,y]} is Relation-like

proof end;

theorem :: RELAT_1:5

for a, b, c, d being set holds {[a,b],[c,d]} is Relation-like

proof end;

theorem :: RELAT_1:6

for X, Y being set holds [:X,Y:] is Relation-like

proof end;

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

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

proof end;

Lm1: for x, y being set
for R being Relation st [x,y] in R holds
( x in union (union R) & y in union (union R) )

proof end;

definition

let P, R be Relation;
redefine pred P = R means :Def2: :: RELAT_1:def 2
for a, b being set holds
( [a,b] in P iff [a,b] in R );
compatibility

proof end;

end;

:: deftheorem Def2 defines = RELAT_1:def 2 :

registration

let P, R be Relation;
cluster P /\ R -> Relation-like ;
coherence

proof end;

cluster P \/ R -> Relation-like ;
coherence

proof end;

cluster P \ R -> Relation-like ;
coherence

proof end;

end;

definition

let P, R be Relation;
redefine pred P c= R means :Def3: :: RELAT_1:def 3
for a, b being set st [a,b] in P holds
[a,b] in R;
compatibility

proof end;

end;

:: deftheorem Def3 defines c= RELAT_1:def 3 :

theorem :: RELAT_1:7

canceled;

theorem :: RELAT_1:8

canceled;

theorem Th9: :: RELAT_1:9

for X being set
for R being Relation holds X /\ R is Relation

proof end;

theorem :: RELAT_1:10

for X being set
for R being Relation holds R \ X is Relation

proof end;

definition

let R be Relation;
func dom R -> set means :Def4: :: RELAT_1:def 4
for x being set holds
( x in it iff ex y being set st [x,y] in R );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines dom RELAT_1:def 4 :

theorem :: RELAT_1:11

canceled;

theorem :: RELAT_1:12

canceled;

theorem Th13: :: RELAT_1:13

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

proof end;

theorem Th14: :: RELAT_1:14

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

proof end;

theorem :: RELAT_1:15

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

proof end;

definition

let R be Relation;
func rng R -> set means :Def5: :: RELAT_1:def 5
for y being set holds
( y in it iff ex x being set st [x,y] in R );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines rng RELAT_1:def 5 :

theorem :: RELAT_1:16

canceled;

theorem :: RELAT_1:17

canceled;

theorem :: RELAT_1:18

for x being set
for R being Relation st x in dom R holds
ex y being set st y in rng R

proof end;

theorem :: RELAT_1:19

for y being set
for R being Relation st y in rng R holds
ex x being set st x in dom R

proof end;

theorem :: RELAT_1:20

for x, y being set
for R being Relation st [x,y] in R holds
( x in dom R & y in rng R ) by Def4, Def5;

theorem Th21: :: RELAT_1:21

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

proof end;

theorem :: RELAT_1:22

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

proof end;

theorem Th23: :: RELAT_1:23

for x, y being set
for R being Relation st R = {[x,y]} holds
( dom R = {x} & rng R = {y} )

proof end;

theorem :: RELAT_1:24

for a, b, x, y being set
for R being Relation st R = {[a,b],[x,y]} holds
( dom R = {a,x} & rng R = {b,y} )

proof end;

theorem Th25: :: RELAT_1:25

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

proof end;

theorem Th26: :: RELAT_1:26

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

proof end;

theorem Th27: :: RELAT_1:27

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

proof end;

theorem :: RELAT_1:28

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

proof end;

definition

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

end;

:: deftheorem defines field RELAT_1:def 6 :

theorem :: RELAT_1:29

for R being Relation holds
( dom R c= field R & rng R c= field R ) by XBOOLE_1:7;

theorem :: RELAT_1:30

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

proof end;

theorem :: RELAT_1:31

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

proof end;

theorem :: RELAT_1:32

for x, y being set
for R being Relation st R = {[x,y]} holds
field R = {x,y}

proof end;

theorem :: RELAT_1:33

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

proof end;

theorem :: RELAT_1:34

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

proof end;

definition

let R be Relation;
func R ~ -> Relation means :Def7: :: RELAT_1:def 7
for x, y being set holds
( [x,y] in it iff [y,x] in R );
existence

proof end;

uniqueness

proof end;

involutiveness ;

end;

:: deftheorem Def7 defines ~ RELAT_1:def 7 :

theorem :: RELAT_1:35

canceled;

theorem :: RELAT_1:36

canceled;

theorem Th37: :: RELAT_1:37

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

proof end;

theorem :: RELAT_1:38

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

proof end;

theorem :: RELAT_1:39

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

proof end;

theorem :: RELAT_1:40

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

proof end;

theorem :: RELAT_1:41

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

proof end;

definition

let P, R be Relation;
func P * R -> Relation means :Def8: :: RELAT_1:def 8
for x, y being set holds
( [x,y] in it iff ex z being set st
( [x,z] in P & [z,y] in R ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines * RELAT_1:def 8 :

theorem :: RELAT_1:42

canceled;

theorem :: RELAT_1:43

canceled;

theorem Th44: :: RELAT_1:44

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

proof end;

theorem Th45: :: RELAT_1:45

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

proof end;

theorem :: RELAT_1:46

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

proof end;

theorem :: RELAT_1:47

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

proof end;

theorem Th48: :: RELAT_1:48

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

proof end;

theorem Th49: :: RELAT_1:49

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

proof end;

theorem :: RELAT_1:50

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

proof end;

theorem :: RELAT_1:51

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

proof end;

theorem :: RELAT_1:52

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

proof end;

theorem :: RELAT_1:53

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

proof end;

theorem :: RELAT_1:54

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

proof end;

theorem Th55: :: RELAT_1:55

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

proof end;

registration

cluster empty -> Relation-like set ;
coherence

proof end;

end;

registration

cluster {} -> Relation-like ;
coherence ;

end;

registration

cluster non empty set ;
existence

proof end;

end;

registration

let f be non empty Relation;
cluster dom f -> non empty ;
coherence

proof end;

cluster rng f -> non empty ;
coherence

proof end;

end;

theorem Th56: :: RELAT_1:56

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

proof end;

theorem :: RELAT_1:57

canceled;

theorem :: RELAT_1:58

canceled;

theorem :: RELAT_1:59

canceled;

theorem Th60: :: RELAT_1:60

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

proof end;

theorem :: RELAT_1:61

canceled;

theorem Th62: :: RELAT_1:62

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

proof end;

registration

let X be empty set ;
cluster dom X -> empty Relation-like ;
coherence by Th60;
cluster rng X -> empty Relation-like ;
coherence by Th60;
let R be Relation;
cluster X * R -> empty ;
coherence by Th62;
cluster R * X -> empty ;
coherence by Th62;

end;

theorem :: RELAT_1:63

canceled;

theorem Th64: :: RELAT_1:64

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

proof end;

theorem :: RELAT_1:65

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

theorem Th66: :: RELAT_1:66

{} ~ = {}

proof end;

registration

let X be empty set ;
cluster X ~ -> empty ;
coherence by Th66;

end;

theorem :: RELAT_1:67

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

proof end;

definition

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

end;

:: deftheorem defines non-empty RELAT_1:def 9 :

definition

let X be set ;
func id X -> Relation means :Def10: :: RELAT_1:def 10
for x, y being set holds
( [x,y] in it iff ( x in X & x = y ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines id RELAT_1:def 10 :

theorem :: RELAT_1:68

canceled;

theorem :: RELAT_1:69

canceled;

theorem :: RELAT_1:70

canceled;

theorem Th71: :: RELAT_1:71

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

proof end;

theorem :: RELAT_1:72

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

proof end;

theorem :: RELAT_1:73

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

proof end;

theorem Th74: :: RELAT_1:74

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

proof end;

theorem Th75: :: RELAT_1:75

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

proof end;

theorem Th76: :: RELAT_1:76

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

proof end;

theorem Th77: :: RELAT_1:77

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

proof end;

theorem :: RELAT_1:78

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

theorem Th79: :: RELAT_1:79

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

proof end;

theorem :: RELAT_1:80

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

theorem :: RELAT_1:81

id {} = {}

proof end;

theorem :: RELAT_1:82

for X being set
for R, P2, P1 being Relation st dom R = X & 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 :Def11: :: RELAT_1:def 11
for x, y being set holds
( [x,y] in it iff ( x in X & [x,y] in R ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines | RELAT_1:def 11 :

theorem :: RELAT_1:83

canceled;

theorem :: RELAT_1:84

canceled;

theorem :: RELAT_1:85

canceled;

theorem Th86: :: RELAT_1:86

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

proof end;

theorem :: RELAT_1:87

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

proof end;

theorem Th88: :: RELAT_1:88

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

proof end;

theorem :: RELAT_1:89

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

proof end;

theorem Th90: :: RELAT_1:90

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

proof end;

theorem :: RELAT_1:91

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

proof end;

theorem :: RELAT_1:92

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

proof end;

theorem :: RELAT_1:93

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

proof end;

theorem :: RELAT_1:94

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

proof end;

theorem :: RELAT_1:95

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

proof end;

theorem Th96: :: RELAT_1:96

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

proof end;

theorem Th97: :: RELAT_1:97

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

proof end;

theorem :: RELAT_1:98

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

theorem Th99: :: RELAT_1:99

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

proof end;

theorem Th100: :: RELAT_1:100

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

proof end;

theorem :: RELAT_1:101

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

proof end;

theorem :: RELAT_1:102

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

proof end;

theorem :: RELAT_1:103

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

proof end;

theorem Th104: :: RELAT_1:104

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

proof end;

theorem Th105: :: RELAT_1:105

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

proof end;

theorem Th106: :: RELAT_1:106

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 Th107: :: RELAT_1:107

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

proof end;

theorem :: RELAT_1:108

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

proof end;

theorem :: RELAT_1:109

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

proof end;

theorem Th110: :: RELAT_1:110

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

proof end;

theorem :: RELAT_1:111

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

proof end;

theorem :: RELAT_1:112

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 :Def12: :: RELAT_1:def 12
for x, y being set holds
( [x,y] in it iff ( y in Y & [x,y] in R ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines | RELAT_1:def 12 :

theorem :: RELAT_1:113

canceled;

theorem :: RELAT_1:114

canceled;

theorem Th115: :: RELAT_1:115

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

proof end;

theorem Th116: :: RELAT_1:116

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

proof end;

theorem Th117: :: RELAT_1:117

for Y being set
for R being Relation holds Y | R c= R

proof end;

theorem Th118: :: RELAT_1:118

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

proof end;

theorem Th119: :: RELAT_1:119

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

proof end;

theorem :: RELAT_1:120

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

proof end;

theorem :: RELAT_1:121

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

proof end;

theorem :: RELAT_1:122

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

proof end;

theorem :: RELAT_1:123

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

proof end;

theorem Th124: :: RELAT_1:124

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

proof end;

theorem Th125: :: RELAT_1:125

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

proof end;

theorem :: RELAT_1:126

for R being Relation holds (rng R) | R = R by Th125;

theorem Th127: :: RELAT_1:127

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

proof end;

theorem :: RELAT_1:128

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

proof end;

theorem :: RELAT_1:129

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

proof end;

theorem :: RELAT_1:130

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

proof end;

theorem Th131: :: RELAT_1:131

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

proof end;

theorem Th132: :: RELAT_1:132

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

proof end;

theorem :: RELAT_1:133

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:134

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

proof end;

theorem :: RELAT_1:135

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

proof end;

theorem :: RELAT_1:136

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

proof end;

theorem :: RELAT_1:137

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

proof end;

theorem :: RELAT_1:138

for Y being set holds Y | {} = {}

proof end;

theorem :: RELAT_1:139

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

proof end;

theorem :: RELAT_1:140

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

proof end;

definition

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

proof end;

uniqueness

proof end;

end;

:: deftheorem Def13 defines .: RELAT_1:def 13 :

theorem :: RELAT_1:141

canceled;

theorem :: RELAT_1:142

canceled;

theorem Th143: :: RELAT_1:143

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

proof end;

theorem Th144: :: RELAT_1:144

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

proof end;

theorem :: RELAT_1:145

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

proof end;

theorem Th146: :: RELAT_1:146

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

proof end;

theorem :: RELAT_1:147

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

proof end;

theorem :: RELAT_1:148

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

proof end;

theorem :: RELAT_1:149

for R being Relation holds R .: {} = {}

proof end;

theorem :: RELAT_1:150

for X being set holds {} .: X = {}

proof end;

theorem :: RELAT_1:151

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

proof end;

theorem :: RELAT_1:152

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

proof end;

theorem :: RELAT_1:153

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

proof end;

theorem :: RELAT_1:154

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

proof end;

theorem :: RELAT_1:155

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

proof end;

theorem Th156: :: RELAT_1:156

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

proof end;

theorem Th157: :: RELAT_1:157

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

proof end;

theorem :: RELAT_1:158

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:159

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

proof end;

theorem :: RELAT_1:160

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

proof end;

theorem :: RELAT_1:161

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

proof end;

theorem :: RELAT_1:162

canceled;

theorem :: RELAT_1:163

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

proof end;

definition

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

proof end;