let R be Relation; ( ( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) ) & ( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) ) )
thus
( R * R = R & R * (R \ (id (dom R))) = {} implies ( dom (CL R) = rng R & rng (CL R) = rng R ) )
( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) )proof
assume that A1:
R * R = R
and A2:
R * (R \ (id (dom R))) = {}
;
( dom (CL R) = rng R & rng (CL R) = rng R )
for
y being
object st
y in rng R holds
y in dom (CL R)
proof
let y be
object ;
( y in rng R implies y in dom (CL R) )
assume
y in rng R
;
y in dom (CL R)
then consider x being
object such that A3:
[x,y] in R
by XTUPLE_0:def 13;
consider z being
object such that A4:
[x,z] in R
and A5:
[z,y] in R
by A1, A3, RELAT_1:def 8;
A6:
z = y
z in dom R
by A5, XTUPLE_0:def 12;
then
[z,y] in id (dom R)
by A6, RELAT_1:def 10;
then
[z,y] in R /\ (id (dom R))
by A5, XBOOLE_0:def 4;
hence
y in dom (CL R)
by A6, XTUPLE_0:def 12;
verum
end;
then A7:
rng R c= dom (CL R)
;
CL R c= R
by XBOOLE_1:17;
then
rng (CL R) c= rng R
by RELAT_1:11;
then
dom (CL R) c= rng R
by Th26;
then
dom (CL R) = rng R
by A7;
hence
(
dom (CL R) = rng R &
rng (CL R) = rng R )
by Th26;
verum
end;
thus
( R * R = R & (R \ (id (dom R))) * R = {} implies ( dom (CL R) = dom R & rng (CL R) = dom R ) )
verumproof
assume that A8:
R * R = R
and A9:
(R \ (id (dom R))) * R = {}
;
( dom (CL R) = dom R & rng (CL R) = dom R )
for
x being
object st
x in dom R holds
x in dom (CL R)
proof
let x be
object ;
( x in dom R implies x in dom (CL R) )
assume A10:
x in dom R
;
x in dom (CL R)
then consider y being
object such that A11:
[x,y] in R
by XTUPLE_0:def 12;
consider z being
object such that A12:
[x,z] in R
and A13:
[z,y] in R
by A8, A11, RELAT_1:def 8;
A14:
z = x
then
[x,z] in id (dom R)
by A10, RELAT_1:def 10;
then
[x,z] in R /\ (id (dom R))
by A12, XBOOLE_0:def 4;
then
z in rng (CL R)
by XTUPLE_0:def 13;
hence
x in dom (CL R)
by A14, Th26;
verum
end;
then A15:
dom R c= dom (CL R)
;
CL R c= R
by XBOOLE_1:17;
then
dom (CL R) c= dom R
by RELAT_1:11;
then
dom (CL R) = dom R
by A15;
hence
(
dom (CL R) = dom R &
rng (CL R) = dom R )
by Th26;
verum
end;