environ
vocabularies ENUMSET,RELATION,RELAT_AB,EQREL;
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;
definition
let X be set;
mode Equivalence_Relation of X -> Relation of X,X means :ER:
it is reflexive & it is symmetric & it is transitive;
existence
proof
take id X;
thus id X is reflexive
proof
let x;
assume x in X;
hence [x,x] in id X by RELAT_AB:def 6;
end;
thus id X is symmetric
proof
let x,y;
assume xy: [x,y] in id X;
then x in X & x = y by RELAT_AB:def 6;
hence [y,x] in id X by xy;
end;
thus id X is transitive
proof
let x,y,z;
assume [x,y] in id X;
then x: x in X & x=y by RELAT_AB:def 6;
assume [y,z] in id X;
then y: y in X & y=z by RELAT_AB:def 6;
thus [x,z] in id X by x,y,RELAT_AB:def 6;
end;
end;
end;
definition
let X,x be set;
let R be Relation of X,X;
func EqClass(x,R) -> set equals R.:({x});
correctness;
end;
reserve R for Relation of X,X;
dom R = X & R is symmetric & R is transitive implies R is reflexive
proof
assume d: dom R = X;
assume s: R is symmetric;
assume t: R is transitive;
let x;
assume x in X;
then consider y such that y:
[x,y] in R by d,RELAT_AB:def 1;
[y,x] in R by y,s,RELATION:def 11;
hence [x,x] in R by y,t,RELATION:def 12;
end;
L0:
y in EqClass(x,R) iff [x,y] in R
proof
thus y in EqClass(x,R) implies [x,y] in R
proof
assume y in EqClass(x,R);
then y in R.:({x});
then consider z such that
z: [z,y] in R & z in {x} by RELAT_AB:def 3;
z=x by z,ENUMSET:def 3;
hence [x,y] in R by z;
end;
thus [x,y] in R implies y in EqClass(x,R)
proof
assume a: [x,y] in R;
x in {x} by ENUMSET:def 3;
then y in R.:({x}) by a,RELAT_AB:def 3;
hence y in EqClass(x,R);
end;
end;
reserve R for Equivalence_Relation of X;
x in X implies x in EqClass(x,R)
proof
assume x: x in X;
R is reflexive by ER;
then [x,x] in R by RELAT_AB:def 8,x;
hence x in EqClass(x,R) by L0;
end;
y in EqClass(x,R) implies EqClass(y,R)=EqClass(x,R)
proof
assume y in EqClass(x,R);
then y: [x,y] in R by L0;
t: R is transitive by ER;
s: R is symmetric by ER;
thus EqClass(y,R) c= EqClass(x,R)
proof
let a;
assume a in EqClass(y,R);
then [y,a] in R by L0;
then [x,a] in R by y,t,RELATION:def 12;
hence a in EqClass(x,R) by L0;
end;
thus EqClass(x,R) c= EqClass(y,R)
proof
let a;
assume a in EqClass(x,R);
then [x,a] in R by L0;
then [a,x] in R by s,RELATION:def 11;
then [a,y] in R by y,t,RELATION:def 12;
then [y,a] in R by s,RELATION:def 11;
hence a in EqClass(y,R) by L0;
end;
end;
EqClass(x,R) meets EqClass(y,R) implies EqClass(x,R) = EqClass(y,R)
proof
s: R is symmetric by ER;
t: R is transitive by ER;
assume EqClass(x,R) meets EqClass(y,R);
then EqClass(x,R) /\ EqClass(y,R) <> {} by ENUMSET:def 12;
then consider b such that
b: b in EqClass(x,R) /\ EqClass(y,R) by ENUMSET:def 1;
b in EqClass(x,R) & b in EqClass(y,R) by b,ENUMSET:def 7;
then bb: [x,b] in R & [y,b] in R by L0;
thus EqClass(x,R) c= EqClass(y,R)
proof
let a;
assume a in EqClass(x,R);
then [x,a] in R by L0;
then [a,x] in R by s,RELATION:def 11;
then [a,b] in R by bb,t,RELATION:def 12;
then [b,a] in R by s,RELATION:def 11;
then [y,a] in R by bb,t,RELATION:def 12;
hence a in EqClass(y,R) by L0;
end;
thus EqClass(y,R) c= EqClass(x,R)
proof
let a;
assume a in EqClass(y,R);
then [y,a] in R by L0;
then [a,y] in R by s,RELATION:def 11;
then [a,b] in R by bb,t,RELATION:def 12;
then [b,a] in R by s,RELATION:def 11;
then [x,a] in R by bb,t,RELATION:def 12;
hence a in EqClass(x,R) by L0;
end;
end;
for A st (for B holds B in A iff ex x st B=EqClass(x,R) & x in X)
holds union A = X
proof
let A;
assume b: for B holds B in A iff ex x st B=EqClass(x,R) & x in X;
thus union A c= X
proof
let a;
assume a in union A;
then consider B such that
B: a in B & B in A by ENUMSET:def 13;
consider x such that
x: B=EqClass(x,R) & x in X by b,B;
[x,a] in R by L0,x,B;
then r: a in rng R by RELAT_AB:def 2;
rng R c= X by RELAT_AB:def 5;
hence a in X by r,ENUMSET:def 10;
end;
thus X c= union A
proof
let a;
r: R is reflexive by ER;
assume a: a in X;
then [a,a] in R by r,RELAT_AB:def 8;
then ae: a in EqClass(a,R) by L0;
EqClass(a,R) in A by a,b;
hence a in union A by ae,ENUMSET:def 13;
end;
end;