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;
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)*id(Y)=id X /\ id Y
proof
thus id(X)*id(Y) c= id X /\ id Y
proof
let a,b;
assume [a,b] in id(X)*id(Y);
then consider c such that
c: [a,c] in id(X) & [c,b] in id(Y) by RELATION:def 7;
a in X & a=c & c in Y & c = b by c,RELAT_AB:def 6;
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 ab: [a,b] in id X & [a,b] in id Y by ENUMSET:def 7;
then a=b by RELAT_AB:def 6;
hence [a,b] in id(X)*id(Y) by ab,RELATION:def 7;
end;
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;
::4.33
S is weakly_connected iff S \/ S~ \/ id(A) = [:A,A:]
proof
dr: dom S c= A & rng S c= A by RELAT_AB:def 5;
thus S is weakly_connected implies S \/ S~ \/ id(A) = [:A,A:]
proof
assume s: S is weakly_connected;
thus S \/ S~ \/ id(A) c= [:A,A:]
proof
let x,y;
assume [x,y] in S \/ S~ \/ id(A);
then [x,y] in S \/ S~ or [x,y] in id A by ENUMSET:def 6;
then [x,y] in S or [x,y] in S~ or [x,y] in id(A) by ENUMSET:def 6;
then per cases;
suppose [x,y] in S;
then x in dom S & y in rng S by RELAT_AB:def 1,def 2;
then x in A & y in A by ENUMSET:def 10,dr;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
suppose [x,y] in S~;
then [y,x] in S by RELATION:def 3;
then y in dom S & x in rng S by RELAT_AB:def 1,def 2;
then x in A & y in A by ENUMSET:def 10,dr;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
suppose [x,y] in id(A);
then x in A & x=y by RELAT_AB:def 6;
hence [x,y] in [:A,A:] by RELAT_AB:def 7;
end;
end;
thus [:A,A:] c= S \/ S~ \/ id(A)
proof
let x,y;
assume [x,y] in [:A,A:];
then consider x1,y1 being set such that
xy: x1 in A & y1 in A & [x,y] = [x1,y1] by RELAT_AB:def 7;
xy1: x=x1 & y=y1 by xy,ENUMSET:2;
per cases;
suppose x=y;
then [x,y] in id(A) by xy,xy1,RELAT_AB:def 6;
hence [x,y] in S \/ S~ \/ id(A) by ENUMSET:def 6;
end;
suppose x<>y;
then [x,y] in S or [y,x] in S by xy,xy1,s,RELAT_AB:def 9;
then [x,y] in S or [x,y] in S~ by RELATION:def 3;
then [x,y] in S \/ S~ by ENUMSET:def 6;
hence [x,y] in S \/ S~ \/ id(A) by ENUMSET:def 6;
end;
end;
end;
thus S \/ S~ \/ id(A) = [:A,A:] implies S is weakly_connected
proof
assume e: S \/ S~ \/ id(A) = [:A,A:];
let x,y be set;
assume xy: x in A & y in A & x <> y & not [x,y] in S;
then [x,y] in S \/ S~ \/ id(A) & not [x,y] in id(A) by e,RELAT_AB:def 7,def 6;
then [x,y] in S \/ S~ by ENUMSET:def 6;
then [x,y] in S~ by xy,ENUMSET:def 6;
hence [y,x] in S by RELATION:def 3;
end;
end;