environ
vocabularies ENUMSET,RELATION,RELAT_AB;
notations ENUMSET,RELATION,RELAT_AB;
constructors ENUMSET,RELATION,RELAT_AB;
definitions ENUMSET,RELATION,RELAT_AB;
equalities ENUMSET,RELATION,RELAT_AB;
theorems ENUMSET,RELATION,RELAT_AB;
begin
reserve A,B,X,Y,Z,V,a,b,c,d,e,x,y,z for set, P,Q,R for Relation,
S for Relation of A,A;
R\R~ is antisymmetric
proof
let x,y;
assume [x,y] in R\R~ & [y,x] in R\R~;
then [x,y] in R & not [x,y] in R~ & [y,x] in R & not [y,x] in R~ by RELATION:def 6;
then contradiction by RELATION:def 3;
hence x=y;
end;
R is transitive implies R~ is transitive
proof
assume r: R is transitive;
let x,y,z;
assume [x,y] in R~ & [y,z] in R~;
then [y,x] in R & [z,y] in R by RELATION:def 3;
then [z,x] in R by r,RELATION:def 12;
hence [x,z] in R~ by RELATION:def 3;
end;
R is symmetric implies R~ c= R
proof
assume s: R is symmetric;
let x,y;
assume [x,y] in R~;
then [y,x] in R by RELATION:def 3;
hence [x,y] in R by s,RELATION:def 11;
end;
R~ c= R implies R is symmetric
proof
assume i: R~ c= R;
let x,y;
assume [x,y] in R;
then [y,x] in R~ by RELATION:def 3;
hence [y,x] in R by i,RELATION:def 9;
end;
:: 4:39
R is transitive iff R*R c= R
proof
thus R is transitive implies R*R c= R
proof
assume t: R is transitive;
let x,y;
assume [x,y] in R*R;
then consider z such that
z: [x,z] in R & [z,y] in R by RELATION:def 7;
thus [x,y] in R by z,t,RELATION:def 12;
end;
thus R*R c= R implies R is transitive
proof
assume r: R*R c= R;
let x,y,z;
assume [x,y] in R & [y,z] in R;
then [x,z] in R*R by RELATION:def 7;
hence [x,z] in R by r,RELATION:def 9;
end;
end;
dom (R~) = rng R
proof
thus dom (R~) c= rng R
proof
let a;
assume a in dom (R~);
then consider b such that
b: [a,b] in R~ by RELAT_AB:def 1;
[b,a] in R by b,RELATION:def 3;
hence a in rng R by RELAT_AB:def 2;
end;
thus rng R c= dom (R~)
proof
let a;
assume a in rng R;
then consider b such that
b: [b,a] in R by RELAT_AB:def 2;
[a,b] in R~ by b,RELATION:def 3;
hence a in dom (R~) by RELAT_AB:def 1;
end;
end;
rng R c= R.:dom R
proof
let a;
assume a in rng R;
then consider b such that
b: [b,a] in R by RELAT_AB:def 2;
b in dom R by b,RELAT_AB:def 1;
hence a in R.:dom R by b,RELAT_AB:def 3;
end;
(P*R).:X c= R.:(P.:X)
proof
let a;
assume a in (P*R).:X;
then consider b such that
b: [b,a] in P*R & b in X by RELAT_AB:def 3;
consider c such that
c: [b,c] in P & [c,a] in R by RELATION:def 7,b;
c in (P.:X) by b,c,RELAT_AB:def 3;
hence a in R.:(P.:X) by c,RELAT_AB:def 3;
end;
R"(X\/Y) c= (R"X) \/ (R"Y)
proof
let a;
assume a in R"(X\/Y);
then consider b such that
b: [a,b] in R & b in X \/ Y by RELAT_AB:def 4;
b in X or b in Y by ENUMSET:def 6,b;
then a in R"X or a in R"Y by b,RELAT_AB:def 4;
hence a in (R"X) \/ (R"Y) by ENUMSET:def 6;
end;
:: 4.40
id (X/\Y)=id X /\ id Y
proof
thus id (X/\Y) c= id X /\ id Y
proof
let a,b;
assume [a,b] in id (X/\Y);
then a in X/\Y & a=b by RELAT_AB:def 6;
then a in X & a in Y & a=b by ENUMSET:def 7;
then [a,b] in id X & [a,b] in id Y by RELAT_AB:def 6;
hence [a,b] in id X /\ id Y by ENUMSET:def 7;
end;
let a,b;
assume [a,b] in id X /\ id Y;
then [a,b] in id X & [a,b] in id Y by ENUMSET:def 7;
then a in X & a=b & a in Y by RELAT_AB:def 6;
then a in X /\ Y & a=b by ENUMSET:def 7;
hence [a,b] in id (X/\Y) by RELAT_AB:def 6;
end;
[:X,Y:]*[:Y,Z:] c= [:X,Z:]
proof
let a,b;
assume [a,b] in [:X,Y:]*[:Y,Z:];
then consider c such that
c: [a,c] in [:X,Y:] & [c,b] in [:Y,Z:] by RELATION:def 7;
consider ac1,ac2 being set such that
a: ac1 in X & ac2 in Y & [ac1,ac2] = [a,c] by c,RELAT_AB:def 7;
consider cb1,cb2 being set such that
b: cb1 in Y & cb2 in Z & [cb1,cb2] = [c,b] by c,RELAT_AB:def 7;
a = ac1 & c = ac2 & c = cb1 & b = cb2 by a,b,ENUMSET:2;
hence [a,b] in [:X,Z:] by a,b,RELAT_AB:def 7;
end;
:: 4:41
P*(Q*R) = (P*Q)*R
proof
thus P*(Q*R) c= (P*Q)*R
proof
let x,y;
assume [x,y] in P*(Q*R);
then consider z such that
z: [x,z] in P & [z,y] in Q*R by RELATION:def 7;
consider a such that
a: [z,a] in Q & [a,y] in R by z,RELATION:def 7;
[x,a] in P*Q by z,a,RELATION:def 7;
hence [x,y] in (P*Q)*R by a,RELATION:def 7;
end;
thus (P*Q)*R c= P*(Q*R)
proof
let x,y;
assume [x,y] in (P*Q)*R;
then consider z such that
z: [x,z] in P*Q & [z,y] in R by RELATION:def 7;
consider b such that
b: [x,b] in P & [b,z] in Q by z,RELATION:def 7;
[b,y] in Q*R by z,b,RELATION:def 7;
hence [x,y] in P*(Q*R) by b,RELATION:def 7;
end;
end;
:: 4.42
(P*Q)~ = Q~ * P~
proof
thus (P*Q)~ c= Q~ * P~
proof
let x,y;
assume [x,y] in (P*Q)~;
then [y,x] in P*Q by RELATION:def 3;
then consider z such that
z: [y,z] in P & [z,x] in Q by RELATION:def 7;
[z,y] in P~ & [x,z] in Q~ by z,RELATION:def 3;
hence [x,y] in Q~ * P~ by RELATION:def 7;
end;
thus Q~ * P~ c= (P*Q)~
proof
let x,y;
assume [x,y] in Q~ * P~;
then consider z such that
z: [x,z] in Q~ & [z,y] in P~ by RELATION:def 7;
[z,x] in Q & [y,z] in P by z,RELATION:def 3;
then [y,x] in P*Q by RELATION:def 7;
hence [x,y] in (P*Q)~ by RELATION:def 3;
end;
end;