environ
vocabularies ENUMSET,RELATION;
notations ENUMSET,RELATION;
constructors ENUMSET,RELATION;
definitions ENUMSET,RELATION;
equalities ENUMSET,RELATION;
theorems ENUMSET,RELATION;
begin
reserve x,y,z,A,B,C for set, P,Q,R,S,T for Relation;
{} is irreflexive
proof
let x;
thus not [x,x] in {} by RELATION:def 2;
end;
ls:
{} is symmetric
proof
let x,y;
assume [x,y] in {};
hence [y,x] in {} by RELATION:def 2;
end;
{} is antisymmetric
proof
let x,y;
assume [x,y] in {} & [y,x] in {};
hence x=y by RELATION:def 2;
end;
{} is asymmetric
proof
let x,y;
assume [x,y] in {};
hence not [y,x] in {} by RELATION:def 2;
end;
{} is asymmetric
proof
let x,y;
assume [x,y] in {};
hence not [y,x] in {} by RELATION:def 2;
end;
{} is transitive
proof
let x,y,z;
assume [x,y] in {} & [y,z] in {};
hence [x,z] in {} by RELATION:def 2;
end;
R is transitive & S is transitive implies R /\ S is transitive
proof
assume t: R is transitive & S is transitive;
thus R /\ S is transitive
proof
let x,y,z;
assume [x,y] in R /\ S & [y,z] in R /\ S;
then [x,y] in R & [x,y] in S & [y,z] in R & [y,z] in S by RELATION:def 5;
then [x,z] in R & [x,z] in S by t,RELATION:def 12;
hence [x,z] in R /\ S by RELATION:def 5;
end;
end;
ex R,S st R is transitive & S is transitive & not R \/ S is transitive
proof
reconsider R={[1,2]} as Relation by RELATION:1;
reconsider S={[2,3]} as Relation by RELATION:1;
take R,S;
thus R is transitive
proof
let x,y,z;
assume [x,y] in R & [y,z] in R;
then [x,y]=[1,2] & [y,z]=[1,2] by ENUMSET:def 3;
then x=1 & y=2 & y=1 & z=2 by ENUMSET:2;
hence [x,z] in R;
end;
thus S is transitive
proof
let x,y,z;
assume [x,y] in S & [y,z] in S;
then [x,y]=[2,3] & [y,z]=[2,3] by ENUMSET:def 3;
then x=2 & y=3 & y=2 & z=3 by ENUMSET:2;
hence [x,z] in S;
end;
rs: R\/S={[1,2],[2,3]}
proof
thus R \/ S c= {[1,2],[2,3]}
proof
let a be set;
assume a in R \/ S;
then a in R or a in S by ENUMSET:def 6;
then a = [1,2] or a = [2,3] by ENUMSET:def 3;
hence a in {[1,2],[2,3]} by ENUMSET:def 4;
end;
thus {[1,2],[2,3]} c= R \/ S
proof
let a be set;
assume a in {[1,2],[2,3]};
then a = [1,2] or a = [2,3] by ENUMSET:def 4;
then a in R or a in S by ENUMSET:def 3;
hence a in R \/ S by ENUMSET:def 6;
end;
end;
[1,2] in R & [2,3] in S by ENUMSET:def 3;
then s: [1,2] in R \/ S & [2,3] in R \/ S by RELATION:def 4;
[1,3] <> [1,2] & [1,3] <> [2,3] by ENUMSET:2;
then not [1,3] in R \/ S by rs,ENUMSET:def 4;
hence not R\/S is transitive by s,RELATION:def 12;
end;
P c= R & R is irreflexive implies P is irreflexive
proof
assume p: P c= R;
assume i: R is irreflexive;
thus P is irreflexive
proof
let x;
not [x,x] in R by i,RELATION:def 15;
hence not [x,x] in P by p,RELATION:def 9;
end;
end;
ex P,R st P c= R & R is symmetric & not P is symmetric
proof
reconsider P={[1,2]} as Relation by RELATION:1;
reconsider R={[1,2],[2,1]} as Relation by RELATION:2;
take P,R;
thus P c= R
proof
let x,y;
assume [x,y] in P;
then [x,y]=[1,2] by ENUMSET:def 3;
hence [x,y] in R by ENUMSET:def 4;
end;
thus R is symmetric
proof
let x,y;
assume [x,y] in R;
then [x,y] = [1,2] or [x,y] = [2,1] by ENUMSET:def 4;
then (x=1 & y=2) or (x=2 & y=1) by ENUMSET:2;
then [y,x]=[1,2] or [y,x]=[2,1] by ENUMSET:2;
hence [y,x] in R by ENUMSET:def 4;
end;
thus not P is symmetric
proof
j: [1,2] in P by ENUMSET:def 3;
[1,2] <> [2,1] by ENUMSET:2;
then not [2,1] in P by ENUMSET:def 3;
hence thesis by j,RELATION:def 11;
end;
end;
ex P,R st P c= R & P is symmetric & not R is symmetric
proof
take P={};
reconsider R={[1,2]} as Relation by RELATION:1;
take R;
thus P c= R
proof
let x,y;
assume [x,y] in P;
hence [x,y] in R by RELATION:def 2;
end;
thus P is symmetric by ls;
thus not R is symmetric
proof
j: [1,2] in R by ENUMSET:def 3;
[1,2] <> [2,1] by ENUMSET:2;
then not [2,1] in R by ENUMSET:def 3;
hence thesis by j,RELATION:def 11;
end;
end;