let X, Y be non empty set ; for f being Function of X,Y holds [:f,f:] " (id Y) is Equivalence_Relation of X
let f be Function of X,Y; [:f,f:] " (id Y) is Equivalence_Relation of X
set ff = [:f,f:] " (id Y);
A1:
dom f = X
by FUNCT_2:def 1;
reconsider R9 = [:f,f:] " (id Y) as Relation of X ;
A2:
dom [:f,f:] = [:(dom f),(dom f):]
by FUNCT_3:def 8;
R9 is_reflexive_in X
proof
let x be
object ;
RELAT_2:def 1 ( not x in X or [x,x] in R9 )
assume A3:
x in X
;
[x,x] in R9
then reconsider x9 =
x as
Element of
X ;
A4:
[(f . x9),(f . x9)] in id Y
by RELAT_1:def 10;
(
[x,x] in dom [:f,f:] &
[(f . x),(f . x)] = [:f,f:] . (
x,
x) )
by A2, A1, A3, FUNCT_3:def 8, ZFMISC_1:def 2;
hence
[x,x] in R9
by A4, FUNCT_1:def 7;
verum
end;
then A5:
( dom R9 = X & field R9 = X )
by ORDERS_1:13;
A6:
R9 is_symmetric_in X
proof
let x,
y be
object ;
RELAT_2:def 3 ( not x in X or not y in X or not [x,y] in R9 or [y,x] in R9 )
assume that A7:
(
x in X &
y in X )
and A8:
[x,y] in R9
;
[y,x] in R9
reconsider x9 =
x,
y9 =
y as
Element of
X by A7;
A9:
(
[y,x] in dom [:f,f:] &
[(f . y),(f . x)] = [:f,f:] . (
y,
x) )
by A2, A1, A7, FUNCT_3:def 8, ZFMISC_1:def 2;
A10:
(
[:f,f:] . [x,y] in id Y &
[(f . x),(f . y)] = [:f,f:] . (
x,
y) )
by A1, A7, A8, FUNCT_1:def 7, FUNCT_3:def 8;
then
f . x9 = f . y9
by RELAT_1:def 10;
hence
[y,x] in R9
by A10, A9, FUNCT_1:def 7;
verum
end;
R9 is_transitive_in X
proof
let x,
y,
z be
object ;
RELAT_2:def 8 ( not x in X or not y in X or not z in X or not [x,y] in R9 or not [y,z] in R9 or [x,z] in R9 )
assume that A11:
x in X
and A12:
y in X
and A13:
z in X
and A14:
[x,y] in R9
and A15:
[y,z] in R9
;
[x,z] in R9
A16:
(
[x,z] in dom [:f,f:] &
[(f . x),(f . z)] = [:f,f:] . (
x,
z) )
by A2, A1, A11, A13, FUNCT_3:def 8, ZFMISC_1:def 2;
reconsider y9 =
y,
z9 =
z as
Element of
X by A12, A13;
(
[:f,f:] . [y,z] in id Y &
[(f . y),(f . z)] = [:f,f:] . (
y,
z) )
by A1, A12, A13, A15, FUNCT_1:def 7, FUNCT_3:def 8;
then A17:
f . y9 = f . z9
by RELAT_1:def 10;
(
[:f,f:] . [x,y] in id Y &
[(f . x),(f . y)] = [:f,f:] . (
x,
y) )
by A1, A11, A12, A14, FUNCT_1:def 7, FUNCT_3:def 8;
hence
[x,z] in R9
by A17, A16, FUNCT_1:def 7;
verum
end;
hence
[:f,f:] " (id Y) is Equivalence_Relation of X
by A5, A6, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16; verum