:: RELAT_1 semantic presentation

definition

let c₁ be set ;
attr a₁ is Relation-like means :Def1: :: RELAT_1:def 1
for b₁ being set st b₁ in a₁ holds
ex b₂, b₃ being set st b₁ = [b₂,b₃];

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 Th1: :: RELAT_1:1

canceled;

theorem Th2: :: RELAT_1:2

canceled;

theorem Th3: :: RELAT_1:3

for b₁ being set
for b₂ being Relation st b₁ c= b₂ holds
b₁ is Relation-like

proof end;

theorem Th4: :: RELAT_1:4

for b₁, b₂ being set holds {[b₁,b₂]} is Relation-like

proof end;

theorem Th5: :: RELAT_1:5

for b₁, b₂, b₃, b₄ being set holds {[b₁,b₂],[b₃,b₄]} is Relation-like

proof end;

theorem Th6: :: RELAT_1:6

for b₁, b₂ being set holds [:b₁,b₂:] is Relation-like

proof end;

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

ex b₁ being Relation st
for b₂, b₃ being set holds
( [b₂,b₃] in b₁ iff ( b₂ in F₁() & b₃ in F₂() & P₁[b₂,b₃] ) )

proof end;

Lemma4: for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in b₃ holds
( b₁ in union (union b₃) & b₂ in union (union b₃) )

proof end;

definition

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

proof end;

end;

:: deftheorem Def2 defines = RELAT_1:def 2 :

registration

let c₁, c₂ be Relation;
cluster a₁ /\ a₂ -> Relation-like ;
coherence

proof end;

cluster a₁ \/ a₂ -> Relation-like ;
coherence

proof end;

cluster a₁ \ a₂ -> Relation-like ;
coherence

proof end;

end;

definition

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

proof end;

end;

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

theorem Th7: :: RELAT_1:7

canceled;

theorem Th8: :: RELAT_1:8

canceled;

theorem Th9: :: RELAT_1:9

for b₁ being set
for b₂ being Relation holds b₁ /\ b₂ is Relation

proof end;

theorem Th10: :: RELAT_1:10

for b₁ being set
for b₂ being Relation holds b₂ \ b₁ is Relation

proof end;

definition

let c₁ be Relation;
func dom c₁ -> set means :Def4: :: RELAT_1:def 4
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st [b₁,b₂] in a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines dom RELAT_1:def 4 :

theorem Th11: :: RELAT_1:11

canceled;

theorem Th12: :: RELAT_1:12

canceled;

theorem Th13: :: RELAT_1:13

for b₁, b₂ being Relation holds dom (b₁ \/ b₂) = (dom b₁) \/ (dom b₂)

proof end;

theorem Th14: :: RELAT_1:14

for b₁, b₂ being Relation holds dom (b₁ /\ b₂) c= (dom b₁) /\ (dom b₂)

proof end;

theorem Th15: :: RELAT_1:15

for b₁, b₂ being Relation holds (dom b₁) \ (dom b₂) c= dom (b₁ \ b₂)

proof end;

definition

let c₁ be Relation;
func rng c₁ -> set means :Def5: :: RELAT_1:def 5
for b₁ being set holds
( b₁ in a₂ iff ex b₂ being set st [b₂,b₁] in a₁ );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines rng RELAT_1:def 5 :

theorem Th16: :: RELAT_1:16

canceled;

theorem Th17: :: RELAT_1:17

canceled;

theorem Th18: :: RELAT_1:18

for b₁ being set
for b₂ being Relation st b₁ in dom b₂ holds
ex b₃ being set st b₃ in rng b₂

proof end;

theorem Th19: :: RELAT_1:19

for b₁ being set
for b₂ being Relation st b₁ in rng b₂ holds
ex b₃ being set st b₃ in dom b₂

proof end;

theorem Th20: :: RELAT_1:20

for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in b₃ holds
( b₁ in dom b₃ & b₂ in rng b₃ ) by Def4, Def5;

theorem Th21: :: RELAT_1:21

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

proof end;

theorem Th22: :: RELAT_1:22

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

proof end;

theorem Th23: :: RELAT_1:23

for b₁, b₂ being set
for b₃ being Relation st b₃ = {[b₁,b₂]} holds
( dom b₃ = {b₁} & rng b₃ = {b₂} )

proof end;

theorem Th24: :: RELAT_1:24

for b₁, b₂, b₃, b₄ being set
for b₅ being Relation st b₅ = {[b₁,b₂],[b₃,b₄]} holds
( dom b₅ = {b₁,b₃} & rng b₅ = {b₂,b₄} )

proof end;

theorem Th25: :: RELAT_1:25

for b₁, b₂ being Relation st b₁ c= b₂ holds
( dom b₁ c= dom b₂ & rng b₁ c= rng b₂ )

proof end;

theorem Th26: :: RELAT_1:26

for b₁, b₂ being Relation holds rng (b₁ \/ b₂) = (rng b₁) \/ (rng b₂)

proof end;

theorem Th27: :: RELAT_1:27

for b₁, b₂ being Relation holds rng (b₁ /\ b₂) c= (rng b₁) /\ (rng b₂)

proof end;

theorem Th28: :: RELAT_1:28

for b₁, b₂ being Relation holds (rng b₁) \ (rng b₂) c= rng (b₁ \ b₂)

proof end;

definition

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

end;

:: deftheorem Def6 defines field RELAT_1:def 6 :

theorem Th29: :: RELAT_1:29

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

theorem Th30: :: RELAT_1:30

for b₁, b₂ being set
for b₃ being Relation st [b₁,b₂] in b₃ holds
( b₁ in field b₃ & b₂ in field b₃ )

proof end;

theorem Th31: :: RELAT_1:31

for b₁, b₂ being Relation st b₁ c= b₂ holds
field b₁ c= field b₂

proof end;

theorem Th32: :: RELAT_1:32

for b₁, b₂ being set
for b₃ being Relation st b₃ = {[b₁,b₂]} holds
field b₃ = {b₁,b₂}

proof end;

theorem Th33: :: RELAT_1:33

for b₁, b₂ being Relation holds field (b₁ \/ b₂) = (field b₁) \/ (field b₂)

proof end;

theorem Th34: :: RELAT_1:34

for b₁, b₂ being Relation holds field (b₁ /\ b₂) c= (field b₁) /\ (field b₂)

proof end;

definition

let c₁ be Relation;
func c₁ ~ -> Relation means :Def7: :: RELAT_1:def 7
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff [b₂,b₁] in a₁ );
existence

proof end;

uniqueness

proof end;

involutiveness ;

end;

:: deftheorem Def7 defines ~ RELAT_1:def 7 :

theorem Th35: :: RELAT_1:35

canceled;

theorem Th36: :: RELAT_1:36

canceled;

theorem Th37: :: RELAT_1:37

for b₁ being Relation holds
( rng b₁ = dom (b₁ ~ ) & dom b₁ = rng (b₁ ~ ) )

proof end;

theorem Th38: :: RELAT_1:38

for b₁ being Relation holds field b₁ = field (b₁ ~ )

proof end;

theorem Th39: :: RELAT_1:39

for b₁, b₂ being Relation holds (b₁ /\ b₂) ~ = (b₁ ~ ) /\ (b₂ ~ )

proof end;

theorem Th40: :: RELAT_1:40

for b₁, b₂ being Relation holds (b₁ \/ b₂) ~ = (b₁ ~ ) \/ (b₂ ~ )

proof end;

theorem Th41: :: RELAT_1:41

for b₁, b₂ being Relation holds (b₁ \ b₂) ~ = (b₁ ~ ) \ (b₂ ~ )

proof end;

definition

let c₁, c₂ be Relation;
func c₁ * c₂ -> Relation means :Def8: :: RELAT_1:def 8
for b₁, b₂ being set holds
( [b₁,b₂] in a₃ iff ex b₃ being set st
( [b₁,b₃] in a₁ & [b₃,b₂] in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def8 defines * RELAT_1:def 8 :

theorem Th42: :: RELAT_1:42

canceled;

theorem Th43: :: RELAT_1:43

canceled;

theorem Th44: :: RELAT_1:44

for b₁, b₂ being Relation holds dom (b₁ * b₂) c= dom b₁

proof end;

theorem Th45: :: RELAT_1:45

for b₁, b₂ being Relation holds rng (b₁ * b₂) c= rng b₂

proof end;

theorem Th46: :: RELAT_1:46

for b₁, b₂ being Relation st rng b₁ c= dom b₂ holds
dom (b₁ * b₂) = dom b₁

proof end;

theorem Th47: :: RELAT_1:47

for b₁, b₂ being Relation st dom b₁ c= rng b₂ holds
rng (b₂ * b₁) = rng b₁

proof end;

theorem Th48: :: RELAT_1:48

for b₁, b₂, b₃ being Relation st b₁ c= b₂ holds
b₃ * b₁ c= b₃ * b₂

proof end;

theorem Th49: :: RELAT_1:49

for b₁, b₂, b₃ being Relation st b₁ c= b₂ holds
b₁ * b₃ c= b₂ * b₃

proof end;

theorem Th50: :: RELAT_1:50

for b₁, b₂, b₃, b₄ being Relation st b₁ c= b₂ & b₃ c= b₄ holds
b₁ * b₃ c= b₂ * b₄

proof end;

theorem Th51: :: RELAT_1:51

for b₁, b₂, b₃ being Relation holds b₁ * (b₂ \/ b₃) = (b₁ * b₂) \/ (b₁ * b₃)

proof end;

theorem Th52: :: RELAT_1:52

for b₁, b₂, b₃ being Relation holds b₁ * (b₂ /\ b₃) c= (b₁ * b₂) /\ (b₁ * b₃)

proof end;

theorem Th53: :: RELAT_1:53

for b₁, b₂, b₃ being Relation holds (b₁ * b₂) \ (b₁ * b₃) c= b₁ * (b₂ \ b₃)

proof end;

theorem Th54: :: RELAT_1:54

for b₁, b₂ being Relation holds (b₁ * b₂) ~ = (b₂ ~ ) * (b₁ ~ )

proof end;

theorem Th55: :: RELAT_1:55

for b₁, b₂, b₃ being Relation holds (b₁ * b₂) * b₃ = b₁ * (b₂ * b₃)

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 c₁ be non empty Relation;
cluster dom a₁ -> non empty ;
coherence

proof end;

cluster rng a₁ -> non empty ;
coherence

proof end;

end;

theorem Th56: :: RELAT_1:56

for b₁ being Relation st ( for b₂, b₃ being set holds not [b₂,b₃] in b₁ ) holds
b₁ = {}

proof end;

theorem Th57: :: RELAT_1:57

canceled;

theorem Th58: :: RELAT_1:58

canceled;

theorem Th59: :: RELAT_1:59

canceled;

theorem Th60: :: RELAT_1:60

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

proof end;

theorem Th61: :: RELAT_1:61

canceled;

theorem Th62: :: RELAT_1:62

for b₁ being Relation holds
( {} * b₁ = {} & b₁ * {} = {} )

proof end;

registration

let c₁ be empty set ;
cluster dom a₁ -> empty Relation-like ;
coherence by Th60;
cluster rng a₁ -> empty Relation-like ;
coherence by Th60;
let c₂ be Relation;
cluster a₁ * a₂ -> empty ;
coherence by Th62;
cluster a₂ * a₁ -> empty ;
coherence by Th62;

end;

theorem Th63: :: RELAT_1:63

canceled;

theorem Th64: :: RELAT_1:64

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

proof end;

theorem Th65: :: RELAT_1:65

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

theorem Th66: :: RELAT_1:66

{} ~ = {}

proof end;

registration

let c₁ be empty set ;
cluster a₁ ~ -> empty ;
coherence by Th66;

end;

theorem Th67: :: RELAT_1:67

for b₁, b₂ being Relation st rng b₁ misses dom b₂ holds
b₁ * b₂ = {}

proof end;

definition

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

end;

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

definition

let c₁ be set ;
func id c₁ -> Relation means :Def10: :: RELAT_1:def 10
for b₁, b₂ being set holds
( [b₁,b₂] in a₂ iff ( b₁ in a₁ & b₁ = b₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def10 defines id RELAT_1:def 10 :

theorem Th68: :: RELAT_1:68

canceled;

theorem Th69: :: RELAT_1:69

canceled;

theorem Th70: :: RELAT_1:70

canceled;

theorem Th71: :: RELAT_1:71

for b₁ being set holds
( dom (id b₁) = b₁ & rng (id b₁) = b₁ )

proof end;

theorem Th72: :: RELAT_1:72

for b₁ being set holds (id b₁) ~ = id b₁

proof end;

theorem Th73: :: RELAT_1:73

for b₁ being set
for b₂ being Relation st ( for b₃ being set st b₃ in b₁ holds
[b₃,b₃] in b₂ ) holds
id b₁ c= b₂

proof end;

theorem Th74: :: RELAT_1:74

for b₁, b₂, b₃ being set
for b₄ being Relation holds
( [b₁,b₂] in (id b₃) * b₄ iff ( b₁ in b₃ & [b₁,b₂] in b₄ ) )

proof end;

theorem Th75: :: RELAT_1:75

for b₁, b₂, b₃ being set
for b₄ being Relation holds
( [b₁,b₂] in b₄ * (id b₃) iff ( b₂ in b₃ & [b₁,b₂] in b₄ ) )

proof end;

theorem Th76: :: RELAT_1:76

for b₁ being set
for b₂ being Relation holds
( b₂ * (id b₁) c= b₂ & (id b₁) * b₂ c= b₂ )

proof end;

theorem Th77: :: RELAT_1:77

for b₁ being set
for b₂ being Relation st dom b₂ c= b₁ holds
(id b₁) * b₂ = b₂

proof end;

theorem Th78: :: RELAT_1:78

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

theorem Th79: :: RELAT_1:79

for b₁ being set
for b₂ being Relation st rng b₂ c= b₁ holds
b₂ * (id b₁) = b₂

proof end;

theorem Th80: :: RELAT_1:80

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

theorem Th81: :: RELAT_1:81

id {} = {}

proof end;

theorem Th82: :: RELAT_1:82

for b₁ being set
for b₂, b₃, b₄ being Relation st dom b₂ = b₁ & rng b₃ c= b₁ & b₃ * b₂ = id (dom b₄) & b₂ * b₄ = id b₁ holds
b₄ = b₃

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
func c₁ | c₂ -> Relation means :Def11: :: RELAT_1:def 11
for b₁, b₂ being set holds
( [b₁,b₂] in a₃ iff ( b₁ in a₂ & [b₁,b₂] in a₁ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def11 defines | RELAT_1:def 11 :

theorem Th83: :: RELAT_1:83

canceled;

theorem Th84: :: RELAT_1:84

canceled;

theorem Th85: :: RELAT_1:85

canceled;

theorem Th86: :: RELAT_1:86

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in dom (b₃ | b₂) iff ( b₁ in b₂ & b₁ in dom b₃ ) )

proof end;

theorem Th87: :: RELAT_1:87

for b₁ being set
for b₂ being Relation holds dom (b₂ | b₁) c= b₁

proof end;

theorem Th88: :: RELAT_1:88

for b₁ being set
for b₂ being Relation holds b₂ | b₁ c= b₂

proof end;

theorem Th89: :: RELAT_1:89

for b₁ being set
for b₂ being Relation holds dom (b₂ | b₁) c= dom b₂

proof end;

theorem Th90: :: RELAT_1:90

for b₁ being set
for b₂ being Relation holds dom (b₂ | b₁) = (dom b₂) /\ b₁

proof end;

theorem Th91: :: RELAT_1:91

for b₁ being set
for b₂ being Relation st b₁ c= dom b₂ holds
dom (b₂ | b₁) = b₁

proof end;

theorem Th92: :: RELAT_1:92

for b₁ being set
for b₂, b₃ being Relation holds (b₂ | b₁) * b₃ c= b₂ * b₃

proof end;

theorem Th93: :: RELAT_1:93

for b₁ being set
for b₂, b₃ being Relation holds b₂ * (b₃ | b₁) c= b₂ * b₃

proof end;

theorem Th94: :: RELAT_1:94

for b₁ being set
for b₂ being Relation holds b₂ | b₁ = (id b₁) * b₂

proof end;

theorem Th95: :: RELAT_1:95

for b₁ being set
for b₂ being Relation holds
( b₂ | b₁ = {} iff dom b₂ misses b₁ )

proof end;

theorem Th96: :: RELAT_1:96

for b₁ being set
for b₂ being Relation holds b₂ | b₁ = b₂ /\ [:b₁,(rng b₂):]

proof end;

theorem Th97: :: RELAT_1:97

for b₁ being set
for b₂ being Relation st dom b₂ c= b₁ holds
b₂ | b₁ = b₂

proof end;

theorem Th98: :: RELAT_1:98

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

theorem Th99: :: RELAT_1:99

for b₁ being set
for b₂ being Relation holds rng (b₂ | b₁) c= rng b₂

proof end;

theorem Th100: :: RELAT_1:100

for b₁, b₂ being set
for b₃ being Relation holds (b₃ | b₁) | b₂ = b₃ | (b₁ /\ b₂)

proof end;

theorem Th101: :: RELAT_1:101

for b₁ being set
for b₂ being Relation holds (b₂ | b₁) | b₁ = b₂ | b₁

proof end;

theorem Th102: :: RELAT_1:102

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
(b₃ | b₁) | b₂ = b₃ | b₁

proof end;

theorem Th103: :: RELAT_1:103

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
(b₃ | b₂) | b₁ = b₃ | b₁

proof end;

theorem Th104: :: RELAT_1:104

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₃ | b₁ c= b₃ | b₂

proof end;

theorem Th105: :: RELAT_1:105

for b₁ being set
for b₂, b₃ being Relation st b₂ c= b₃ holds
b₂ | b₁ c= b₃ | b₁

proof end;

theorem Th106: :: RELAT_1:106

for b₁, b₂ being set
for b₃, b₄ being Relation st b₃ c= b₄ & b₁ c= b₂ holds
b₃ | b₁ c= b₄ | b₂

proof end;

theorem Th107: :: RELAT_1:107

for b₁, b₂ being set
for b₃ being Relation holds b₃ | (b₁ \/ b₂) = (b₃ | b₁) \/ (b₃ | b₂)

proof end;

theorem Th108: :: RELAT_1:108

for b₁, b₂ being set
for b₃ being Relation holds b₃ | (b₁ /\ b₂) = (b₃ | b₁) /\ (b₃ | b₂)

proof end;

theorem Th109: :: RELAT_1:109

for b₁, b₂ being set
for b₃ being Relation holds b₃ | (b₁ \ b₂) = (b₃ | b₁) \ (b₃ | b₂)

proof end;

theorem Th110: :: RELAT_1:110

for b₁ being Relation holds b₁ | {} = {}

proof end;

theorem Th111: :: RELAT_1:111

for b₁ being set holds {} | b₁ = {}

proof end;

theorem Th112: :: RELAT_1:112

for b₁ being set
for b₂, b₃ being Relation holds (b₂ * b₃) | b₁ = (b₂ | b₁) * b₃

proof end;

definition

let c₁ be set ;
let c₂ be Relation;
func c₁ | c₂ -> Relation means :Def12: :: RELAT_1:def 12
for b₁, b₂ being set holds
( [b₁,b₂] in a₃ iff ( b₂ in a₁ & [b₁,b₂] in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def12 defines | RELAT_1:def 12 :

theorem Th113: :: RELAT_1:113

canceled;

theorem Th114: :: RELAT_1:114

canceled;

theorem Th115: :: RELAT_1:115

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in rng (b₂ | b₃) iff ( b₁ in b₂ & b₁ in rng b₃ ) )

proof end;

theorem Th116: :: RELAT_1:116

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) c= b₁

proof end;

theorem Th117: :: RELAT_1:117

for b₁ being set
for b₂ being Relation holds b₁ | b₂ c= b₂

proof end;

theorem Th118: :: RELAT_1:118

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) c= rng b₂

proof end;

theorem Th119: :: RELAT_1:119

for b₁ being set
for b₂ being Relation holds rng (b₁ | b₂) = (rng b₂) /\ b₁

proof end;

theorem Th120: :: RELAT_1:120

for b₁ being set
for b₂ being Relation st b₁ c= rng b₂ holds
rng (b₁ | b₂) = b₁

proof end;

theorem Th121: :: RELAT_1:121

for b₁ being set
for b₂, b₃ being Relation holds (b₁ | b₂) * b₃ c= b₂ * b₃

proof end;

theorem Th122: :: RELAT_1:122

for b₁ being set
for b₂, b₃ being Relation holds b₂ * (b₁ | b₃) c= b₂ * b₃

proof end;

theorem Th123: :: RELAT_1:123

for b₁ being set
for b₂ being Relation holds b₁ | b₂ = b₂ * (id b₁)

proof end;

theorem Th124: :: RELAT_1:124

for b₁ being set
for b₂ being Relation holds b₁ | b₂ = b₂ /\ [:(dom b₂),b₁:]

proof end;

theorem Th125: :: RELAT_1:125

for b₁ being set
for b₂ being Relation st rng b₂ c= b₁ holds
b₁ | b₂ = b₂

proof end;

theorem Th126: :: RELAT_1:126

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

theorem Th127: :: RELAT_1:127

for b₁, b₂ being set
for b₃ being Relation holds b₁ | (b₂ | b₃) = (b₁ /\ b₂) | b₃

proof end;

theorem Th128: :: RELAT_1:128

for b₁ being set
for b₂ being Relation holds b₁ | (b₁ | b₂) = b₁ | b₂

proof end;

theorem Th129: :: RELAT_1:129

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₂ | (b₁ | b₃) = b₁ | b₃

proof end;

theorem Th130: :: RELAT_1:130

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₁ | (b₂ | b₃) = b₁ | b₃

proof end;

theorem Th131: :: RELAT_1:131

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₁ | b₃ c= b₂ | b₃

proof end;

theorem Th132: :: RELAT_1:132

for b₁ being set
for b₂, b₃ being Relation st b₂ c= b₃ holds
b₁ | b₂ c= b₁ | b₃

proof end;

theorem Th133: :: RELAT_1:133

for b₁, b₂ being set
for b₃, b₄ being Relation st b₃ c= b₄ & b₁ c= b₂ holds
b₁ | b₃ c= b₂ | b₄

proof end;

theorem Th134: :: RELAT_1:134

for b₁, b₂ being set
for b₃ being Relation holds (b₁ \/ b₂) | b₃ = (b₁ | b₃) \/ (b₂ | b₃)

proof end;

theorem Th135: :: RELAT_1:135

for b₁, b₂ being set
for b₃ being Relation holds (b₁ /\ b₂) | b₃ = (b₁ | b₃) /\ (b₂ | b₃)

proof end;

theorem Th136: :: RELAT_1:136

for b₁, b₂ being set
for b₃ being Relation holds (b₁ \ b₂) | b₃ = (b₁ | b₃) \ (b₂ | b₃)

proof end;

theorem Th137: :: RELAT_1:137

for b₁ being Relation holds {} | b₁ = {}

proof end;

theorem Th138: :: RELAT_1:138

for b₁ being set holds b₁ | {} = {}

proof end;

theorem Th139: :: RELAT_1:139

for b₁ being set
for b₂, b₃ being Relation holds b₁ | (b₂ * b₃) = b₂ * (b₁ | b₃)

proof end;

theorem Th140: :: RELAT_1:140

for b₁, b₂ being set
for b₃ being Relation holds (b₁ | b₃) | b₂ = b₁ | (b₃ | b₂)

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
func c₁ .: c₂ -> set means :Def13: :: RELAT_1:def 13
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set st
( [b₂,b₁] in a₁ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

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

theorem Th141: :: RELAT_1:141

canceled;

theorem Th142: :: RELAT_1:142

canceled;

theorem Th143: :: RELAT_1:143

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ .: b₂ iff ex b₄ being set st
( b₄ in dom b₃ & [b₄,b₁] in b₃ & b₄ in b₂ ) )

proof end;

theorem Th144: :: RELAT_1:144

for b₁ being set
for b₂ being Relation holds b₂ .: b₁ c= rng b₂

proof end;

theorem Th145: :: RELAT_1:145

for b₁ being set
for b₂ being Relation holds b₂ .: b₁ = b₂ .: ((dom b₂) /\ b₁)

proof end;

theorem Th146: :: RELAT_1:146

for b₁ being Relation holds b₁ .: (dom b₁) = rng b₁

proof end;

theorem Th147: :: RELAT_1:147

for b₁ being set
for b₂ being Relation holds b₂ .: b₁ c= b₂ .: (dom b₂)

proof end;

theorem Th148: :: RELAT_1:148

for b₁ being set
for b₂ being Relation holds rng (b₂ | b₁) = b₂ .: b₁

proof end;

theorem Th149: :: RELAT_1:149

for b₁ being Relation holds b₁ .: {} = {}

proof end;

theorem Th150: :: RELAT_1:150

for b₁ being set holds {} .: b₁ = {}

proof end;

theorem Th151: :: RELAT_1:151

for b₁ being set
for b₂ being Relation holds
( b₂ .: b₁ = {} iff dom b₂ misses b₁ )

proof end;

theorem Th152: :: RELAT_1:152

for b₁ being set
for b₂ being Relation st b₁ <> {} & b₁ c= dom b₂ holds
b₂ .: b₁ <> {}

proof end;

theorem Th153: :: RELAT_1:153

for b₁, b₂ being set
for b₃ being Relation holds b₃ .: (b₁ \/ b₂) = (b₃ .: b₁) \/ (b₃ .: b₂)

proof end;

theorem Th154: :: RELAT_1:154

for b₁, b₂ being set
for b₃ being Relation holds b₃ .: (b₁ /\ b₂) c= (b₃ .: b₁) /\ (b₃ .: b₂)

proof end;

theorem Th155: :: RELAT_1:155

for b₁, b₂ being set
for b₃ being Relation holds (b₃ .: b₁) \ (b₃ .: b₂) c= b₃ .: (b₁ \ b₂)

proof end;

theorem Th156: :: RELAT_1:156

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₃ .: b₁ c= b₃ .: b₂

proof end;

theorem Th157: :: RELAT_1:157

for b₁ being set
for b₂, b₃ being Relation st b₂ c= b₃ holds
b₂ .: b₁ c= b₃ .: b₁

proof end;

theorem Th158: :: RELAT_1:158

for b₁, b₂ being set
for b₃, b₄ being Relation st b₃ c= b₄ & b₁ c= b₂ holds
b₃ .: b₁ c= b₄ .: b₂

proof end;

theorem Th159: :: RELAT_1:159

for b₁ being set
for b₂, b₃ being Relation holds (b₂ * b₃) .: b₁ = b₃ .: (b₂ .: b₁)

proof end;

theorem Th160: :: RELAT_1:160

for b₁, b₂ being Relation holds rng (b₁ * b₂) = b₂ .: (rng b₁)

proof end;

theorem Th161: :: RELAT_1:161

for b₁, b₂ being set
for b₃ being Relation holds (b₃ | b₁) .: b₂ c= b₃ .: b₂

proof end;

theorem Th162: :: RELAT_1:162

canceled;

theorem Th163: :: RELAT_1:163

for b₁ being set
for b₂ being Relation holds (dom b₂) /\ b₁ c= (b₂ ~ ) .: (b₂ .: b₁)

proof end;

definition

let c₁ be Relation;
let c₂ be set ;
func c₁ " c₂ -> set means :Def14: :: RELAT_1:def 14
for b₁ being set holds
( b₁ in a₃ iff ex b₂ being set st
( [b₁,b₂] in a₁ & b₂ in a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def14 defines " RELAT_1:def 14 :

theorem Th164: :: RELAT_1:164

canceled;

theorem Th165: :: RELAT_1:165

canceled;

theorem Th166: :: RELAT_1:166

for b₁, b₂ being set
for b₃ being Relation holds
( b₁ in b₃ " b₂ iff ex b₄ being set st
( b₄ in rng b₃ & [b₁,b₄] in b₃ & b₄ in b₂ ) )

proof end;

theorem Th167: :: RELAT_1:167

for b₁ being set
for b₂ being Relation holds b₂ " b₁ c= dom b₂

proof end;

theorem Th168: :: RELAT_1:168

for b₁ being set
for b₂ being Relation holds b₂ " b₁ = b₂ " ((rng b₂) /\ b₁)

proof end;

theorem Th169: :: RELAT_1:169

for b₁ being Relation holds b₁ " (rng b₁) = dom b₁

proof end;

theorem Th170: :: RELAT_1:170

for b₁ being set
for b₂ being Relation holds b₂ " b₁ c= b₂ " (rng b₂)

proof end;

theorem Th171: :: RELAT_1:171

for b₁ being Relation holds b₁ " {} = {}

proof end;

theorem Th172: :: RELAT_1:172

for b₁ being set holds {} " b₁ = {}

proof end;

theorem Th173: :: RELAT_1:173

for b₁ being set
for b₂ being Relation holds
( b₂ " b₁ = {} iff rng b₂ misses b₁ )

proof end;

theorem Th174: :: RELAT_1:174

for b₁ being set
for b₂ being Relation st b₁ <> {} & b₁ c= rng b₂ holds
b₂ " b₁ <> {}

proof end;

theorem Th175: :: RELAT_1:175

for b₁, b₂ being set
for b₃ being Relation holds b₃ " (b₁ \/ b₂) = (b₃ " b₁) \/ (b₃ " b₂)

proof end;

theorem Th176: :: RELAT_1:176

for b₁, b₂ being set
for b₃ being Relation holds b₃ " (b₁ /\ b₂) c= (b₃ " b₁) /\ (b₃ " b₂)

proof end;

theorem Th177: :: RELAT_1:177

for b₁, b₂ being set
for b₃ being Relation holds (b₃ " b₁) \ (b₃ " b₂) c= b₃ " (b₁ \ b₂)

proof end;

theorem Th178: :: RELAT_1:178

for b₁, b₂ being set
for b₃ being Relation st b₁ c= b₂ holds
b₃ " b₁ c= b₃ " b₂

proof end;

theorem Th179: :: RELAT_1:179

for b₁ being set
for b₂, b₃ being Relation st b₂ c= b₃ holds
b₂ " b₁ c= b₃ " b₁

proof end;

theorem Th180: :: RELAT_1:180

for b₁, b₂ being set
for b₃, b₄ being Relation st b₃ c= b₄ & b₁ c= b₂ holds
b₃ " b₁ c= b₄ " b₂

proof end;

theorem Th181: :: RELAT_1:181

for b₁ being set
for b₂, b₃ being Relation holds (b₂ * b₃) " b₁ = b₂ " (b₃ " b₁)

proof end;

theorem Th182: :: RELAT_1:182

for b₁, b₂ being Relation holds dom (b₁ * b₂) = b₁ " (dom b₂)

proof end;

theorem Th183: :: RELAT_1:183

for b₁ being set
for b₂ being Relation holds (rng b₂) /\ b₁ c= (b₂ ~ ) " (b₂ " b₁)

proof end;

definition

let c₁ be Relation;
attr a₁ is empty-yielding means :Def15: :: RELAT_1:def 15
rng a₁ c= {{} };

end;

:: deftheorem Def15 defines empty-yielding RELAT_1:def 15 :

theorem Th184: :: RELAT_1:184

for b₁ being Relation holds
( b₁ is empty-yielding iff for b₂ being set st b₂ in rng b₁ holds
b₂ = {} )

proof end;

theorem Th185: :: RELAT_1:185

for b₁, b₂ being Relation
for b₃, b₄ being set st b₁ | b₃ = b₂ | b₃ & b₁ | b₄ = b₂ | b₄ holds
b₁ | (b₃ \/ b₄) = b₂ | (b₃ \/ b₄)

proof end;

theorem Th186: :: RELAT_1:186

for b₁ being set
for b₂, b₃ being Relation st dom b₃ c= b₁ & b₃ c= b₂ holds
b₃ c= b₂ | b₁

proof end;

theorem Th187: :: RELAT_1:187

for b₁ being Relation
for b₂ being set st b₂ misses dom b₁ holds
b₁ | b₂ = {}

proof end;

theorem Th188: :: RELAT_1:188

for b₁, b₂ being Relation
for b₃, b₄ being set st b₃ c= b₄ & b₁ | b₄ = b₂ | b₄ holds
b₁ | b₃ = b₂ | b₃

proof end;

theorem Th189: :: RELAT_1:189

for b₁, b₂ being Relation holds b₁ | (dom b₂) = b₁ | (dom (b₂ | (dom b₁)))

proof end;

registration

cluster {} -> Relation-like empty-yielding ;
coherence

proof end;

end;

registration

cluster empty-yielding set ;
existence

proof end;

end;

registration

let c₁ be empty-yielding Relation;
let c₂ be set ;
cluster a₁ | a₂ -> empty-yielding ;
coherence

proof end;

end;

theorem Th190: :: RELAT_1:190

for b₁ being set
for b₂ being Relation st not b₂ | b₁ is empty-yielding holds
not b₂ is empty-yielding

proof end;