:: RELSET_1 semantic presentation

definition
let c1, c2 be set ;
mode Relation of c1,c2 -> set means :Def1: :: RELSET_1:def 1
a3 c= [:a1,a2:];
existence
ex b1 being set st b1 c= [:c1,c2:] ;
end;

:: deftheorem Def1 defines Relation RELSET_1:def 1 :
for b1, b2 being set
for b3 being set holds
( b3 is Relation of b1,b2 iff b3 c= [:b1,b2:] );

definition
let c1, c2 be set ;
redefine mode Relation as Relation of c1,c2 -> Subset of [:a1,a2:];
coherence
for b1 being Relation of c1,c2 holds b1 is Subset of [:c1,c2:] by Def1;
end;

registration
let c1, c2 be set ;
cluster -> Relation-like Element of bool [:a1,a2:];
coherence
for b1 being Subset of [:c1,c2:] holds b1 is Relation-like
proof end;
end;

theorem Th1: :: RELSET_1:1
canceled;

theorem Th2: :: RELSET_1:2
canceled;

theorem Th3: :: RELSET_1:3
canceled;

theorem Th4: :: RELSET_1:4
for b1, b2, b3 being set
for b4 being Relation of b2,b3 st b1 c= b4 holds
b1 is Relation of b2,b3
proof end;

theorem Th5: :: RELSET_1:5
canceled;

theorem Th6: :: RELSET_1:6
for b1, b2, b3 being set
for b4 being Relation of b1,b2 st b3 in b4 holds
ex b5, b6 being set st
( b3 = [b5,b6] & b5 in b1 & b6 in b2 )
proof end;

theorem Th7: :: RELSET_1:7
canceled;

theorem Th8: :: RELSET_1:8
for b1, b2, b3, b4 being set st b3 in b1 & b4 in b2 holds
{[b3,b4]} is Relation of b1,b2
proof end;

theorem Th9: :: RELSET_1:9
for b1 being set
for b2 being Relation st dom b2 c= b1 holds
b2 is Relation of b1, rng b2
proof end;

theorem Th10: :: RELSET_1:10
for b1 being set
for b2 being Relation st rng b2 c= b1 holds
b2 is Relation of dom b2,b1
proof end;

theorem Th11: :: RELSET_1:11
for b1, b2 being set
for b3 being Relation st dom b3 c= b1 & rng b3 c= b2 holds
b3 is Relation of b1,b2
proof end;

theorem Th12: :: RELSET_1:12
for b1, b2 being set
for b3 being Relation of b1,b2 holds
( dom b3 c= b1 & rng b3 c= b2 )
proof end;

theorem Th13: :: RELSET_1:13
for b1, b2, b3 being set
for b4 being Relation of b1,b3 st dom b4 c= b2 holds
b4 is Relation of b2,b3
proof end;

theorem Th14: :: RELSET_1:14
for b1, b2, b3 being set
for b4 being Relation of b3,b1 st rng b4 c= b2 holds
b4 is Relation of b3,b2
proof end;

theorem Th15: :: RELSET_1:15
for b1, b2, b3 being set
for b4 being Relation of b1,b3 st b1 c= b2 holds
b4 is Relation of b2,b3
proof end;

theorem Th16: :: RELSET_1:16
for b1, b2, b3 being set
for b4 being Relation of b3,b1 st b1 c= b2 holds
b4 is Relation of b3,b2
proof end;

theorem Th17: :: RELSET_1:17
for b1, b2, b3, b4 being set
for b5 being Relation of b1,b3 st b1 c= b2 & b3 c= b4 holds
b5 is Relation of b2,b4
proof end;

definition
let c1, c2 be set ;
let c3, c4 be Relation of c1,c2;
redefine func \/ as c3 \/ c4 -> Relation of a1,a2;
coherence
c3 \/ c4 is Relation of c1,c2
proof end;
redefine func /\ as c3 /\ c4 -> Relation of a1,a2;
coherence
c3 /\ c4 is Relation of c1,c2
proof end;
redefine func \ as c3 \ c4 -> Relation of a1,a2;
coherence
c3 \ c4 is Relation of c1,c2
proof end;
end;

definition
let c1, c2 be set ;
let c3 be Relation of c1,c2;
redefine func dom as dom c3 -> Subset of a1;
coherence
dom c3 is Subset of c1 by Th12;
redefine func rng as rng c3 -> Subset of a2;
coherence
rng c3 is Subset of c2 by Th12;
end;

theorem Th18: :: RELSET_1:18
canceled;

theorem Th19: :: RELSET_1:19
for b1, b2 being set
for b3 being Relation of b1,b2 holds field b3 c= b1 \/ b2
proof end;

theorem Th20: :: RELSET_1:20
canceled;

theorem Th21: :: RELSET_1:21
canceled;

theorem Th22: :: RELSET_1:22
for b1, b2 being set
for b3 being Relation of b2,b1 holds
( ( for b4 being set st b4 in b2 holds
ex b5 being set st [b4,b5] in b3 ) iff dom b3 = b2 )
proof end;

theorem Th23: :: RELSET_1:23
for b1, b2 being set
for b3 being Relation of b1,b2 holds
( ( for b4 being set st b4 in b2 holds
ex b5 being set st [b5,b4] in b3 ) iff rng b3 = b2 )
proof end;

definition
let c1, c2 be set ;
let c3 be Relation of c1,c2;
redefine func ~ as c3 ~ -> Relation of a2,a1;
coherence
c3 ~ is Relation of c2,c1
proof end;
end;

definition
let c1, c2, c3, c4 be set ;
let c5 be Relation of c1,c2;
let c6 be Relation of c3,c4;
redefine func * as c5 * c6 -> Relation of a1,a4;
coherence
c5 * c6 is Relation of c1,c4
proof end;
end;

theorem Th24: :: RELSET_1:24
for b1, b2 being set
for b3 being Relation of b1,b2 holds
( dom (b3 ~ ) = rng b3 & rng (b3 ~ ) = dom b3 )
proof end;

theorem Th25: :: RELSET_1:25
for b1, b2 being set holds {} is Relation of b1,b2
proof end;

theorem Th26: :: RELSET_1:26
for b1, b2 being set
for b3 being Relation of b1,b2 st b3 is Relation of {} ,b2 holds
b3 = {}
proof end;

theorem Th27: :: RELSET_1:27
for b1, b2 being set
for b3 being Relation of b2,b1 st b3 is Relation of b2, {} holds
b3 = {}
proof end;

theorem Th28: :: RELSET_1:28
for b1 being set holds id b1 c= [:b1,b1:]
proof end;

theorem Th29: :: RELSET_1:29
for b1 being set holds id b1 is Relation of b1,b1
proof end;

theorem Th30: :: RELSET_1:30
for b1, b2, b3 being set
for b4 being Relation of b1,b2 st id b3 c= b4 holds
( b3 c= dom b4 & b3 c= rng b4 )
proof end;

theorem Th31: :: RELSET_1:31
for b1, b2 being set
for b3 being Relation of b2,b1 st id b2 c= b3 holds
( b2 = dom b3 & b2 c= rng b3 )
proof end;

theorem Th32: :: RELSET_1:32
for b1, b2 being set
for b3 being Relation of b1,b2 st id b2 c= b3 holds
( b2 c= dom b3 & b2 = rng b3 )
proof end;

definition
let c1, c2 be set ;
let c3 be Relation of c1,c2;
let c4 be set ;
redefine func | as c3 | c4 -> Relation of a1,a2;
coherence
c3 | c4 is Relation of c1,c2
proof end;
end;

definition
let c1, c2, c3 be set ;
let c4 be Relation of c1,c2;
redefine func | as c3 | c4 -> Relation of a1,a2;
coherence
c3 | c4 is Relation of c1,c2
proof end;
end;

theorem Th33: :: RELSET_1:33
for b1, b2, b3 being set
for b4 being Relation of b1,b3 holds b4 | b2 is Relation of b2,b3
proof end;

theorem Th34: :: RELSET_1:34
for b1, b2, b3 being set
for b4 being Relation of b2,b1 st b2 c= b3 holds
b4 | b3 = b4
proof end;

theorem Th35: :: RELSET_1:35
for b1, b2, b3 being set
for b4 being Relation of b3,b1 holds b2 | b4 is Relation of b3,b2
proof end;

theorem Th36: :: RELSET_1:36
for b1, b2, b3 being set
for b4 being Relation of b1,b2 st b2 c= b3 holds
b3 | b4 = b4
proof end;

definition
let c1, c2 be set ;
let c3 be Relation of c1,c2;
let c4 be set ;
redefine func .: as c3 .: c4 -> Subset of a2;
coherence
c3 .: c4 is Subset of c2
proof end;
redefine func " as c3 " c4 -> Subset of a1;
coherence
c3 " c4 is Subset of c1
proof end;
end;

theorem Th37: :: RELSET_1:37
canceled;

theorem Th38: :: RELSET_1:38
for b1, b2 being set
for b3 being Relation of b1,b2 holds
( b3 .: b1 = rng b3 & b3 " b2 = dom b3 )
proof end;

theorem Th39: :: RELSET_1:39
for b1, b2 being set
for b3 being Relation of b2,b1 holds
( b3 .: (b3 " b1) = rng b3 & b3 " (b3 .: b2) = dom b3 )
proof end;

scheme :: RELSET_1:sch 1
s1{ F1() -> set , F2() -> set , P1[ set , set ] } :
ex b1 being Relation of F1(),F2() st
for b2, b3 being set holds
( [b2,b3] in b1 iff ( b2 in F1() & b3 in F2() & P1[b2,b3] ) )
proof end;

definition
let c1 be set ;
mode Relation of a1 is Relation of a1,a1;
end;

theorem Th40: :: RELSET_1:40
canceled;

theorem Th41: :: RELSET_1:41
canceled;

theorem Th42: :: RELSET_1:42
canceled;

theorem Th43: :: RELSET_1:43
canceled;

theorem Th44: :: RELSET_1:44
canceled;

theorem Th45: :: RELSET_1:45
for b1 being set
for b2 being Relation of b1 holds
( b2 * (id b1) = b2 & (id b1) * b2 = b2 )
proof end;

theorem Th46: :: RELSET_1:46
for b1 being non empty set holds id b1 <> {}
proof end;

theorem Th47: :: RELSET_1:47
for b1, b2 being non empty set
for b3 being Relation of b1,b2
for b4 being Element of b1 holds
( b4 in dom b3 iff ex b5 being Element of b2 st [b4,b5] in b3 )
proof end;

theorem Th48: :: RELSET_1:48
for b1, b2 being non empty set
for b3 being Relation of b2,b1
for b4 being Element of b1 holds
( b4 in rng b3 iff ex b5 being Element of b2 st [b5,b4] in b3 )
proof end;

theorem Th49: :: RELSET_1:49
for b1, b2 being non empty set
for b3 being Relation of b1,b2
for b4 being Element of b1 st b4 in dom b3 holds
ex b5 being Element of b2 st b5 in rng b3
proof end;

theorem Th50: :: RELSET_1:50
for b1, b2 being non empty set
for b3 being Relation of b2,b1
for b4 being Element of b1 st b4 in rng b3 holds
ex b5 being Element of b2 st b5 in dom b3
proof end;

theorem Th51: :: RELSET_1:51
for b1, b2, b3 being non empty set
for b4 being Relation of b1,b2
for b5 being Relation of b2,b3
for b6 being Element of b1
for b7 being Element of b3 holds
( [b6,b7] in b4 * b5 iff ex b8 being Element of b2 st
( [b6,b8] in b4 & [b8,b7] in b5 ) )
proof end;

theorem Th52: :: RELSET_1:52
for b1, b2, b3 being non empty set
for b4 being Relation of b3,b1
for b5 being Element of b1 holds
( b5 in b4 .: b2 iff ex b6 being Element of b3 st
( [b6,b5] in b4 & b6 in b2 ) )
proof end;

theorem Th53: :: RELSET_1:53
for b1, b2, b3 being non empty set
for b4 being Relation of b1,b3
for b5 being Element of b1 holds
( b5 in b4 " b2 iff ex b6 being Element of b3 st
( [b5,b6] in b4 & b6 in b2 ) )
proof end;

scheme :: RELSET_1:sch 2
s2{ F1() -> non empty set , F2() -> non empty set , P1[ set , set ] } :
ex b1 being Relation of F1(),F2() st
for b2 being Element of F1()
for b3 being Element of F2() holds
( [b2,b3] in b1 iff P1[b2,b3] )
proof end;