:: Some Properties of Binary Relations
:: by Waldemar Korczy\'nski
::
:: Received January 17, 1992
:: Copyright (c) 1992-2016 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, XBOOLE_0, ZFMISC_1, TARSKI, SYSREL;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1;
constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1;
requirements BOOLE, SUBSET;
definitions TARSKI, XBOOLE_0, RELAT_1;
expansions TARSKI, XBOOLE_0, RELAT_1;
theorems ZFMISC_1, RELAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XTUPLE_0;
begin
reserve x,y,z,t for object,X,Y,Z,W for set;
reserve R,S,T for Relation;
Lm1: X <> {} & Y <> {} implies dom [:X,Y:] = X & rng [:X,Y:] = Y
by RELAT_1:160;
theorem Th1:
dom (R /\ [:X,Y:]) c= X & rng (R /\ [:X,Y:]) c= Y
proof
per cases;
suppose
X = {} or Y = {};
then R /\ [:X,Y:] = R /\ {} by ZFMISC_1:90
.= {};
hence thesis;
end;
suppose
A1: X <> {} & Y <> {};
rng (R /\ [:X,Y:]) c= rng R /\ rng [:X,Y:] by RELAT_1:13; then
A2: rng (R /\ [:X,Y:]) c= rng R /\ Y by A1,Lm1;
dom (R /\ [:X,Y:]) c= dom R /\ dom [:X,Y:] by XTUPLE_0:24; then
A3: dom (R /\ [:X,Y:]) c= dom R /\ X by A1,Lm1;
dom R /\ X c= X by XBOOLE_1:17;
hence dom (R /\ [:X,Y:]) c= X by A3;
rng R /\ Y c= Y by XBOOLE_1:17;
hence rng (R /\ [:X,Y:]) c= Y by A2;
end;
end;
theorem
X misses Y implies dom (R /\ [:X,Y:]) misses rng (R /\ [:X,Y:])
proof
assume
A1: X /\ Y = {};
dom (R /\ [:X,Y:]) c= X by Th1; then
A2: dom (R /\ [:X,Y:]) /\ rng (R /\ [:X,Y:]) c= X /\ rng (R /\ [:X,Y:]) by
XBOOLE_1:26;
X /\ rng (R /\ [:X,Y:]) c= X /\ Y by Th1,XBOOLE_1:26;
hence dom (R /\ [:X,Y:]) /\ rng (R /\ [:X,Y:]) = {} by A1,A2,XBOOLE_1:1,3;
end;
theorem Th3:
R c= [:X,Y:] implies dom R c= X & rng R c= Y
proof
assume R c= [:X,Y:];
then R /\ [:X,Y:] = R by XBOOLE_1:28;
hence thesis by Th1;
end;
theorem
R c= [:X,Y:] implies R~ c= [:Y,X:]
proof
assume
A1: R c= [:X,Y:];
let z,t be object;
assume [z,t] in R~;
then [t,z] in R by RELAT_1:def 7;
then t in X & z in Y by A1,ZFMISC_1:87;
hence thesis by ZFMISC_1:87;
end;
theorem
[:X,Y:]~ = [:Y,X:]
proof
let x,y be object;
thus [x,y] in [:X,Y:]~ implies [x,y] in [:Y,X:]
proof
assume [x,y] in [:X,Y:]~;
then [y,x] in [:X,Y:] by RELAT_1:def 7;
then y in X & x in Y by ZFMISC_1:87;
hence thesis by ZFMISC_1:87;
end;
assume [x,y] in [:Y,X:];
then y in X & x in Y by ZFMISC_1:87;
then [y,x] in [:X,Y:] by ZFMISC_1:87;
hence thesis by RELAT_1:def 7;
end;
theorem Th6:
(R \/ S) * T = (R * T) \/ (S * T)
proof
thus (R \/ S) * T = (R * T) \/ (S * T)
proof
let x,y be object;
thus [x,y] in (R \/ S) * T implies [x,y] in (R * T) \/ (S * T)
proof
assume [x,y] in (R \/ S) * T;
then consider z being object such that
A1: [x,z] in R \/ S & [z,y] in T by RELAT_1:def 8;
[x,z] in R & [z,y] in T or [x,z] in S & [z,y] in T by A1,XBOOLE_0:def 3;
then [x,y] in R * T or [x,y] in S *T by RELAT_1:def 8;
hence thesis by XBOOLE_0:def 3;
end;
assume A2: [x,y] in (R * T) \/ (S * T);
per cases by A2,XBOOLE_0:def 3;
suppose
[x,y] in S * T;
then consider z being object such that
A3: [x,z] in S and
A4: [z,y] in T by RELAT_1:def 8;
[x,z] in R \/ S by A3,XBOOLE_0:def 3;
hence thesis by A4,RELAT_1:def 8;
end;
suppose [x,y] in R * T;
then consider z being object such that
A5: [x,z] in R and
A6: [z,y] in T by RELAT_1:def 8;
[x,z] in R \/ S by A5,XBOOLE_0:def 3;
hence thesis by A6,RELAT_1:def 8;
end;
end;
end;
theorem
(X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies
not x in Y & not y in X & y in Y) &
(X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies
not y in X & not x in Y & x in X) &
(X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies
not x in X & not y in Y & y in X) &
(X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in X implies
not x in X & not y in Y & x in Y)
proof
thus X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in X implies not
x in Y & not y in X & y in Y
proof
assume that
A1: X misses Y and
A2: R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R and
A3: x in X;
A4: not [x,y] in [:Y,X:]
proof
assume
A5: [x,y] in [:Y,X:];
not x in Y by A1,A3,XBOOLE_0:3;
hence thesis by A5,ZFMISC_1:87;
end;
A6: [x,y] in [:X,Y:] implies thesis
proof
assume [x,y] in [:X,Y:];
then x in X & y in Y by ZFMISC_1:87;
hence thesis by A1,XBOOLE_0:3;
end;
[:X,Y:] misses [:Y,X:] by A1,ZFMISC_1:104;
hence thesis by A2,A6,A4,XBOOLE_0:5;
end;
thus X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & y in Y implies
not y in X & not x in Y & x in X
proof
assume that
A7: X misses Y and
A8: R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R and
A9: y in Y;
A10: not [x,y] in [:Y,X:]
proof
assume
A11: [x,y] in [:Y,X:];
not y in X by A7,A9,XBOOLE_0:3;
hence thesis by A11,ZFMISC_1:87;
end;
[x,y] in [:X,Y:] implies thesis
proof
assume [x,y] in [:X,Y:]; then
x in X & y in Y by ZFMISC_1:87;
hence thesis by A7,XBOOLE_0:3;
end;
hence thesis by A8,A10,XBOOLE_0:def 3;
end;
thus X misses Y & R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R & x in Y implies not
x in X & not y in Y & y in X
proof
assume that
A12: X misses Y and
A13: R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R and
A14: x in Y;
A15: not [x,y] in [:X,Y:]
proof
assume
A16: [x,y] in [:X,Y:];
not x in X by A12,A14,XBOOLE_0:3;
hence thesis by A16,ZFMISC_1:87;
end;
[x,y] in [:Y,X:] & not [x,y] in [:X,Y:] implies thesis
proof
assume [x,y] in [:Y,X:] & not [x,y] in [:X,Y:]; then
x in Y & y in X & not x in X or x in Y & y in X & not y in Y
by ZFMISC_1:87;
hence thesis by A12,XBOOLE_0:3;
end;
hence thesis by A13,A15,XBOOLE_0:def 3;
end;
assume that
A17: X misses Y and
A18: R c= [:X,Y:] \/ [:Y,X:] & [x,y] in R and
A19: y in X;
A20: not [x,y] in [:X,Y:]
proof
assume
A21: [x,y] in [:X,Y:];
not y in Y by A17,A19,XBOOLE_0:3;
hence thesis by A21,ZFMISC_1:87;
end;
[x,y] in [:Y,X:] implies thesis
proof
assume [x,y] in [:Y,X:]; then
x in Y & y in X by ZFMISC_1:87;
hence thesis by A17,XBOOLE_0:3;
end;
hence thesis by A18,A20,XBOOLE_0:def 3;
end;
theorem Th8:
R c= [:X,Y:] implies R|Z = R /\ [:Z,Y:] & (Z|`R) = R /\ [:X,Z:]
proof
assume
A1: R c= [:X,Y:];
thus (R|Z) = R /\ [:Z,Y:]
proof
let x,y be object;
thus [x,y] in (R|Z) implies [x,y] in R /\ [:Z,Y:]
proof
assume
A2: [x,y] in (R|Z); then
A3: x in Z by RELAT_1:def 11;
A4: [x,y] in R by A2,RELAT_1:def 11;
then y in Y by A1,ZFMISC_1:87;
then [x,y] in [:Z,Y:] by A3,ZFMISC_1:87;
hence thesis by A4,XBOOLE_0:def 4;
end;
thus [x,y] in R /\ [:Z,Y:] implies [x,y] in (R|Z)
proof
assume
A5: [x,y] in R /\ [:Z,Y:];
then [x,y] in [:Z,Y:] by XBOOLE_0:def 4; then
A6: x in Z by ZFMISC_1:87;
[x,y] in R by A5,XBOOLE_0:def 4;
hence thesis by A6,RELAT_1:def 11;
end;
end;
let x,y be object;
thus [x,y] in (Z|`R) implies [x,y] in R /\ [:X,Z:]
proof
assume
A7: [x,y] in (Z|`R); then
A8: y in Z by RELAT_1:def 12;
A9: [x,y] in R by A7,RELAT_1:def 12;
then x in X by A1,ZFMISC_1:87;
then [x,y] in [:X,Z:] by A8,ZFMISC_1:87;
hence thesis by A9,XBOOLE_0:def 4;
end;
assume
A10: [x,y] in R /\ [:X,Z:];
then [x,y] in [:X,Z:] by XBOOLE_0:def 4; then
A11: y in Z by ZFMISC_1:87;
[x,y] in R by A10,XBOOLE_0:def 4;
hence thesis by A11,RELAT_1:def 12;
end;
theorem
R c= [:X,Y:] & X = Z \/ W implies R = (R|Z) \/ (R|W)
proof
assume that
A1: R c= [:X,Y:] and
A2: X = Z \/ W;
thus R = R /\ [:X,Y:] by A1,XBOOLE_1:28
.= R /\ ([:Z,Y:] \/ [:W,Y:]) by A2,ZFMISC_1:97
.= (R /\ [:Z,Y:]) \/ (R /\ [:W,Y:]) by XBOOLE_1:23
.= (R|Z) \/ (R /\ [:W,Y:]) by A1,Th8
.= (R|Z) \/ (R|W) by A1,Th8;
end;
theorem
X misses Y & R c= [:X,Y:] \/ [:Y,X:] implies R|X c= [:X,Y:]
proof
assume that
A1: X /\ Y = {} and
A2: R c= [:X,Y:] \/ [:Y,X:];
R|X = R /\ [:X,rng R:] by RELAT_1:67;
then R|X c= ([:X,Y:] \/ [:Y,X:]) /\ [:X,rng R:] by A2,XBOOLE_1:26;
then
A3: R|X c= [:X,Y:] /\ [:X,rng R:] \/ [:Y,X:] /\ [:X,rng R:] by XBOOLE_1:23;
[:Y,X:] /\ [:X,rng R:] = [:X /\ Y, X /\ rng R:] by ZFMISC_1:100
.= {} by A1,ZFMISC_1:90;
hence thesis by A3,XBOOLE_1:18;
end;
theorem
R c= S implies R~ c= S~
proof
assume R c= S;
then R \/ S = S by XBOOLE_1:12;
then (R~) \/ (S~) = S~ by RELAT_1:23;
hence thesis by XBOOLE_1:7;
end;
:: DIAGONAL RELATION
Lm2: id X c= [:X,X:]
proof
let x,y be object;
assume [x,y] in id X;
then x in X & x = y by RELAT_1:def 10;
hence thesis by ZFMISC_1:87;
end;
theorem Th12:
id(X) * id(X) = id X
proof
dom id(X) = X;
hence thesis by RELAT_1:51;
end;
theorem
for x being object holds id({x}) = {[x,x]}
proof let x be object;
x in {x} by TARSKI:def 1;
then [x,x] in id({x}) by RELAT_1:def 10; then
A1: {[x,x]} c= id {x} by ZFMISC_1:31;
[:{x},{x}:] = {[x,x]} by ZFMISC_1:29;
then id({x}) c= {[x,x]} by Lm2;
hence thesis by A1;
end;
theorem Th14:
id(X \/ Y) = id(X) \/ id(Y) & id(X /\ Y) = id(X) /\ id(Y) &
id(X \ Y) = id(X) \ id(Y)
proof
thus id(X \/ Y) = id(X) \/ id(Y)
proof
let x,y be object;
thus [x,y] in id(X \/ Y) implies [x,y] in id(X) \/ id(Y)
proof
assume
A1: [x,y] in id(X \/ Y);
then x in X \/ Y by RELAT_1:def 10;
then
A2: x in X or x in Y by XBOOLE_0:def 3;
x = y by A1,RELAT_1:def 10;
then [x,y] in id(X) or [x,y] in id(Y) by A2,RELAT_1:def 10;
hence thesis by XBOOLE_0:def 3;
end;
assume [x,y] in id(X) \/ id(Y); then
A3: [x,y] in id(X) or [x,y] in id(Y) by XBOOLE_0:def 3;
then x in X or x in Y by RELAT_1:def 10;
then
A4: x in X \/ Y by XBOOLE_0:def 3;
x = y by A3,RELAT_1:def 10;
hence thesis by A4,RELAT_1:def 10;
end;
thus id(X /\ Y) = id(X) /\ id(Y)
proof
let x,y be object;
thus [x,y] in id(X /\ Y) implies [x,y] in id(X) /\ id(Y)
proof
assume
A5: [x,y] in id(X /\ Y); then
A6: x in X /\ Y by RELAT_1:def 10;
A7: x = y by A5,RELAT_1:def 10;
x in Y by A6,XBOOLE_0:def 4; then
A8: [x,y] in id(Y) by A7,RELAT_1:def 10;
x in X by A6,XBOOLE_0:def 4;
then [x,y] in id(X) by A7,RELAT_1:def 10;
hence thesis by A8,XBOOLE_0:def 4;
end;
assume
A9: [x,y] in id(X) /\ id Y; then
A10: [x,y] in id(X) by XBOOLE_0:def 4; then
A11: x = y by RELAT_1:def 10;
[x,y] in id(Y) by A9,XBOOLE_0:def 4; then
A12: x in Y by RELAT_1:def 10;
x in X by A10,RELAT_1:def 10;
then x in X /\ Y by A12,XBOOLE_0:def 4;
hence thesis by A11,RELAT_1:def 10;
end;
let x,y be object;
thus [x,y] in id(X \ Y) implies [x,y] in id(X) \ id(Y)
proof
assume
A13: [x,y] in id(X \ Y); then
A14: x in X \ Y by RELAT_1:def 10;
then not x in Y by XBOOLE_0:def 5; then
A15: not [x,y] in id(Y) by RELAT_1:def 10;
x = y by A13,RELAT_1:def 10;
then [x,y] in id(X) by A14,RELAT_1:def 10;
hence thesis by A15,XBOOLE_0:def 5;
end;
assume
A16: [x,y] in id(X) \ id(Y); then
A17: x = y by RELAT_1:def 10;
not [x,y] in id(Y) by A16,XBOOLE_0:def 5; then
A18: not (x in Y & x = y) by RELAT_1:def 10;
x in X by A16,RELAT_1:def 10;
then x in X \ Y by A16,A18,RELAT_1:def 10,XBOOLE_0:def 5;
hence thesis by A17,RELAT_1:def 10;
end;
theorem Th15:
X c= Y implies id X c= id Y
proof
assume X c= Y;
then X \/ Y = Y by XBOOLE_1:12;
then id(X) \/ id Y = id Y by Th14;
hence thesis by XBOOLE_1:7;
end;
theorem
id(X \ Y) \ id X = {} by Th15,XBOOLE_1:37;
theorem
R c= id dom R implies R = id dom R
proof
assume
A1: R c= id dom R;
let x,y be object;
thus [x,y] in R implies [x,y] in id dom R by A1;
assume
A2: [x,y] in id dom R;
then x in dom R by RELAT_1:def 10; then
A3: ex z being object st [x,z] in R by XTUPLE_0:def 12;
x = y by A2,RELAT_1:def 10;
hence thesis by A1,A3,RELAT_1:def 10;
end;
theorem
id X c= R \/ R~ implies id X c= R & id X c= R~
proof
assume
A1: id X c= R \/ R~;
for x being object holds x in X implies [x,x] in R & [x,x] in R~
proof
let x be object;
assume x in X;
then [x,x] in id(X) by RELAT_1:def 10; then
A2: [x,x] in R or [x,x] in R~ by A1,XBOOLE_0:def 3;
hence [x,x] in R by RELAT_1:def 7;
thus thesis by A2,RELAT_1:def 7;
end; then
(for x being object holds x in X implies [x,x] in R) &
for x being object holds x in X implies [x,x] in R~;
hence thesis by RELAT_1:47;
end;
theorem
id X c= R implies id X c= R~
proof
assume
A1: id X c= R;
for x being object holds x in X implies [x,x] in R~
proof
let x be object;
assume x in X;
then [x,x] in id X by RELAT_1:def 10;
hence thesis by A1,RELAT_1:def 7;
end;
hence thesis by RELAT_1:47;
end;
:: CLOSURE RELATION
theorem
R c= [:X,X:] implies R \ id dom R = R \ id X & R \ id rng R = R \ id X
proof
A1: R \ id dom R c= R \ id X
proof
let x,y be object;
assume
A2: [x,y] in R \ id dom R; then
A3: not [x,y] in id dom R by XBOOLE_0:def 5;
not [x,y] in id X
proof
assume [x,y] in id X; then
A4: x = y by RELAT_1:def 10;
x in dom R by A2,XTUPLE_0:def 12;
hence contradiction by A3,A4,RELAT_1:def 10;
end;
hence thesis by A2,XBOOLE_0:def 5;
end;
A5: R \ id rng R c= R \ id X
proof
let x,y be object;
assume
A6: [x,y] in R \ id rng R; then
A7: not [x,y] in id rng R by XBOOLE_0:def 5;
not [x,y] in id X
proof
assume [x,y] in id X; then
A8: x = y by RELAT_1:def 10;
y in rng R by A6,XTUPLE_0:def 13;
hence contradiction by A7,A8,RELAT_1:def 10;
end;
hence thesis by A6,XBOOLE_0:def 5;
end;
assume
A9: R c= [:X,X:];
then id dom R c= id X by Th3,Th15;
then R \ id X c= R \ id dom R by XBOOLE_1:34;
hence R \ id dom R = R \ id X by A1;
id(rng R) c= id X by A9,Th3,Th15;
then R \ id(X) c= R \ id rng R by XBOOLE_1:34;
hence thesis by A5;
end;
theorem
(id(X) * (R \ id X) = {} implies dom (R \ id X) = dom R \ X) &
((R \ id X) * id X = {} implies rng (R \ id X) = rng R \ X)
proof
thus id(X) * (R \ id X) = {} implies dom (R \ id X) = dom R \ X
proof
assume
A1: id(X) * (R \ id X) = {};
A2: dom (R \ id X) c= dom R \ X
proof
let x be object;
A3: x in dom R & not x in X implies thesis by XBOOLE_0:def 5;
assume x in dom (R \ id X); then
A4: ex y being object st [x,y] in (R \ id X) by XTUPLE_0:def 12;
not x in X
proof
assume x in X;
then [x,x] in id X by RELAT_1:def 10;
hence thesis by A1,A4,RELAT_1:def 8;
end;
hence thesis by A4,A3,XTUPLE_0:def 12;
end;
dom R \ dom id X c= dom (R \ id X) by XTUPLE_0:25;
then dom R \ X c= dom (R \ id X);
hence thesis by A2;
end;
thus (R \ id X) * id(X) = {} implies rng (R \ id X) = rng R \ X
proof
assume
A5: (R \ id X) * id X = {};
A6: rng (R \ id X) c= rng R \ X
proof
let y be object;
A7: y in rng R & not y in X implies thesis by XBOOLE_0:def 5;
assume y in rng(R \ id X); then
A8: ex x being object st [x,y] in R \ id X by XTUPLE_0:def 13;
not y in X
proof
assume y in X;
then [y,y] in id X by RELAT_1:def 10;
hence thesis by A5,A8,RELAT_1:def 8;
end;
hence thesis by A8,A7,XTUPLE_0:def 13;
end;
rng R \ rng id X c= rng (R \ id X) by RELAT_1:14;
then rng R \ X c= rng (R \ id X);
hence thesis by A6;
end;
end;
theorem Th22:
(R c= R * R & R * (R \ id rng R) = {} implies id rng R c= R) &
(R c= R * R & (R \ id dom R) * R = {} implies id dom R c= R)
proof
thus R c= R * R & R * (R \ id rng R) = {} implies id rng R c= R
proof
assume that
A1: R c= R * R and
A2: R * (R \ id rng R) = {};
for y being object holds y in rng R implies [y,y] in R
proof
let y be object;
assume y in rng 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;
z = y
proof
assume z <> y;
then not [z,y] in id rng R by RELAT_1:def 10;
then [z,y] in (R \ id rng R) by A5,XBOOLE_0:def 5;
hence contradiction by A2,A4,RELAT_1:def 8;
end;
hence thesis by A5;
end;
hence thesis by RELAT_1:47;
end;
assume that
A6: R c= R * R and
A7: (R \ id dom R) * R = {};
for x being object holds x in dom R implies [x,x] in R
proof
let x be object;
assume x in dom R;
then consider y being object such that
A8: [x,y] in R by XTUPLE_0:def 12;
consider z being object such that
A9: [x,z] in R and
A10: [z,y] in R by A6,A8,RELAT_1:def 8;
z = x
proof
assume z <> x;
then not [x,z] in id dom R by RELAT_1:def 10;
then [x,z] in R \ id dom R by A9,XBOOLE_0:def 5;
hence contradiction by A7,A10,RELAT_1:def 8;
end;
hence thesis by A9;
end;
hence thesis by RELAT_1:47;
end;
theorem
(R c= R * R & R * (R \ id rng R) = {} implies R /\ (id rng R) = id rng R) &
(R c= R * R & (R \ id dom R) * R = {} implies
R /\ (id dom R) = id dom R) by Th22,XBOOLE_1:28;
theorem
(R * (R \ id X) = {} implies R * (R \ id rng R) = {}) &
((R \ id X) * R = {} implies (R \ id dom R) * R = {})
proof
thus R * (R \ id X) = {} implies R * (R \ id rng R) = {}
proof
assume that
A1: R * (R \ id X) = {} and
A2: R * (R \ id rng R) <> {};
consider x,y being object such that
A3: [x,y] in R * (R \ id rng R) by A2;
consider z being object such that
A4: [x,z] in R and
A5: [z,y] in R \ id rng R by A3,RELAT_1:def 8;
z in rng R & not [z,y] in id rng R
by A4,A5,XBOOLE_0:def 5,XTUPLE_0:def 13;
then z <> y by RELAT_1:def 10;
then not [z,y] in id X by RELAT_1:def 10;
then [z,y] in R \ id X by A5,XBOOLE_0:def 5;
hence contradiction by A1,A4,RELAT_1:def 8;
end;
assume that
A6: (R \ id X) * R = {} and
A7: (R \ id dom R) * R <> {};
consider x,y being object such that
A8: [x,y] in (R \ id dom R) * R by A7;
consider z being object such that
A9: [x,z] in (R \ id dom R) and
A10: [z,y] in R by A8,RELAT_1:def 8;
not [x,z] in id dom R by A9,XBOOLE_0:def 5;
then not z in dom R or x <> z by RELAT_1:def 10;
then not [x,z] in id X by A10,RELAT_1:def 10,XTUPLE_0:def 12;
then [x,z] in R \ id X by A9,XBOOLE_0:def 5;
hence contradiction by A6,A10,RELAT_1:def 8;
end;
:: OPERATION CL
definition
let R;
func CL R -> Relation equals
R /\ id dom R;
correctness;
end;
theorem Th25:
for x,y being object holds [x,y] in CL R implies x in dom CL R & x = y
proof let x,y be object;
assume
A1: [x,y] in CL R;
then [x,y] in id dom R by XBOOLE_0:def 4;
hence thesis by A1,RELAT_1:def 10,XTUPLE_0:def 12;
end;
theorem Th26:
dom CL R = rng CL R
proof
thus dom CL R c= rng CL R
proof
let x be object;
assume x in dom CL R;
then consider y being object such that
A1: [x,y] in CL R by XTUPLE_0:def 12;
[x,y] in id dom R by A1,XBOOLE_0:def 4;
then [x,x] in CL R by A1,RELAT_1:def 10;
hence thesis by XTUPLE_0:def 13;
end;
let x be object;
assume x in rng CL R;
then consider y being object such that
A2: [y,x] in CL R by XTUPLE_0:def 13;
[y,x] in id dom R by A2,XBOOLE_0:def 4;
then [x,x] in CL R by A2,RELAT_1:def 10;
hence thesis by XTUPLE_0:def 12;
end;
theorem Th27:
(x in dom CL R iff x in dom R & [x,x] in R) &
(x in rng CL R iff x in dom R & [x,x] in R) &
(x in rng CL R iff x in rng R & [x,x] in R) &
(x in dom CL R iff x in rng R & [x,x] in R)
proof
A1: x in dom R & [x,x] in R implies x in dom CL R
proof
assume that
A2: x in dom R and
A3: [x,x] in R;
[x,x] in id dom R by A2,RELAT_1:def 10;
then [x,x] in (R /\ id dom R) by A3,XBOOLE_0:def 4;
hence thesis by XTUPLE_0:def 12;
end;
A4: x in dom CL R implies x in dom R & [x,x] in R
proof
assume x in dom CL R;
then consider y being object such that
A5: [x,y] in CL R by XTUPLE_0:def 12;
[x,y] in R & [x,y] in id dom R by A5,XBOOLE_0:def 4;
hence thesis by RELAT_1:def 10;
end;
hence x in dom CL R iff x in dom R & [x,x] in R by A1;
thus x in rng CL R iff x in dom R & [x,x] in R by A4,A1,Th26;
thus x in rng CL R iff x in rng R & [x,x] in R
by A4,A1,Th26,XTUPLE_0:def 12,def 13;
thus thesis by A4,A1,XTUPLE_0:def 12,def 13;
end;
theorem Th28:
CL R = id dom CL R
proof
let x,y be object;
thus [x,y] in CL R implies [x,y] in id dom CL R
proof
assume
A1: [x,y] in CL R;
then [x,y] in id dom R by XBOOLE_0:def 4; then
A2: x = y by RELAT_1:def 10;
x in dom CL R by A1,XTUPLE_0:def 12;
hence thesis by A2,RELAT_1:def 10;
end;
assume
A3: [x,y] in id dom CL R;
then x in dom CL R by RELAT_1:def 10; then
A4: ex z being object st [x,z] in CL R by XTUPLE_0:def 12;
x = y by A3,RELAT_1:def 10;
hence thesis by A4,Th25;
end;
theorem Th29:
(R * R = R & R * (R \ CL R) = {} & [x,y] in R & x <> y implies
x in (dom R \ dom CL R) & y in dom CL R) &
(R * R = R & (R \ CL R) * R = {} & [x,y] in R & x <> y implies
y in (rng R \ dom CL R) & x in dom CL R)
proof
thus R * R = R & R * (R \ CL R) = {} & [x,y] in R & x <> y implies
x in (dom R \ dom CL R) & y in dom CL R
proof
assume that
A1: R * R = R and
A2: R * (R \ CL R) = {} and
A3: [x,y] in R and
A4: x <> y;
A5: y in rng R by A3,XTUPLE_0:def 13;
consider z being object such that
A6: [x,z] in R and
A7: [z,y] in R by A1,A3,RELAT_1:def 8;
A8: z = y
proof
assume z <> y;
then not [z,y] in id dom R by RELAT_1:def 10;
then not [z,y] in R /\ id dom R by XBOOLE_0:def 4;
then [z,y] in R \ CL R by A7,XBOOLE_0:def 5;
hence thesis by A2,A6,RELAT_1:def 8;
end;
not [x,y] in id dom R by A4,RELAT_1:def 10;
then not [x,y] in R /\ id dom R by XBOOLE_0:def 4; then
A9: [x,y] in R \ CL(R) by A3,XBOOLE_0:def 5;
A10: not x in dom CL R
proof
assume x in dom CL R;
then [x,x] in R by Th27;
hence thesis by A2,A9,RELAT_1:def 8;
end;
x in dom R by A6,XTUPLE_0:def 12;
hence thesis by A7,A8,A5,A10,Th27,XBOOLE_0:def 5;
end;
thus R * R = R & (R \ CL R) * R = {} & [x,y] in R & x <> y implies
y in (rng R \ dom CL R) & x in dom CL R
proof
assume that
A11: R * R = R and
A12: (R \ CL R) * R = {} and
A13: [x,y] in R and
A14: x <> y;
A15: x in dom R by A13,XTUPLE_0:def 12;
consider z being object such that
A16: [x,z] in R and
A17: [z,y] in R by A11,A13,RELAT_1:def 8;
A18: z = x
proof
assume z <> x;
then not [x,z] in id dom R by RELAT_1:def 10;
then not [x,z] in R /\ id dom R by XBOOLE_0:def 4;
then [x,z] in R \ CL R by A16,XBOOLE_0:def 5;
hence thesis by A12,A17,RELAT_1:def 8;
end;
not [x,y] in id dom R by A14,RELAT_1:def 10;
then not [x,y] in R /\ id dom R by XBOOLE_0:def 4;
then
A19: [x,y] in R \ CL R by A13,XBOOLE_0:def 5;
A20: not y in dom CL R
proof
assume y in dom CL R;
then [y,y] in R by Th27;
hence thesis by A12,A19,RELAT_1:def 8;
end;
y in rng R by A17,XTUPLE_0:def 13;
hence thesis by A16,A18,A15,A20,Th27,XBOOLE_0:def 5;
end;
end;
theorem
(R * R = R & R * (R \ id dom R) = {} & [x,y] in R & x <> y implies
x in ((dom R) \ dom CL R) & y in dom CL R) &
(R * R = R & (R \ id dom R) * R = {} & [x,y] in R & x <> y implies
y in ((rng R) \ dom CL R) & x in dom CL R)
proof
R \ CL R = R \ id dom R by XBOOLE_1:47;
hence thesis by Th29;
end;
theorem
(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
thus R * R = R & R * (R \ id dom R) = {} implies
dom CL R = rng R & rng CL R = rng R
proof
assume that
A1: R * R = R and
A2: R * (R \ id dom R) = {};
for y being object holds y in rng R implies y in dom CL R
proof
let y be object;
assume y in rng 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
proof
assume z <> y;
then not [z,y] in id dom R by RELAT_1:def 10;
then [z,y] in R \ id dom R by A5,XBOOLE_0:def 5;
hence thesis by A2,A4,RELAT_1:def 8;
end;
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 thesis by A6,XTUPLE_0:def 12;
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 thesis by Th26;
end;
thus R * R = R & (R \ id dom R) * R = {} implies
dom CL R = dom R & rng CL R = dom R
proof
assume that
A8: R * R = R and
A9: (R \ id dom R) * R = {};
for x being object holds x in dom R implies x in dom CL R
proof
let x be object;
assume
A10: x in dom 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
proof
assume z <> x;
then not [x,z] in id dom R by RELAT_1:def 10;
then [x,z] in R \ id dom R by A12,XBOOLE_0:def 5;
hence thesis by A9,A13,RELAT_1:def 8;
end;
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 thesis by A14,Th26;
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 thesis by Th26;
end;
end;
theorem Th32:
dom CL R c= dom R & rng CL R c= rng R & rng CL R c= dom R & dom CL R c= rng R
proof
CL R c= R by XBOOLE_1:17;
hence dom CL R c= dom R & rng CL R c= rng R by RELAT_1:11;
hence thesis by Th26;
end;
theorem
id dom CL R c= id dom R & id rng CL R c= id dom R by Th15,Th32;
theorem Th34:
id dom CL R c= R & id rng CL R c= R
proof
thus id dom CL R c= R
proof
let x,y be object;
assume [x,y] in id dom CL R;
then x in dom CL R & x = y by RELAT_1:def 10;
hence thesis by Th27;
end;
hence thesis by Th26;
end;
theorem Th35:
(id X c= R & id(X) * (R \ id X) = {} implies R|X = id X) &
(id X c= R & (R \ id X) * id X = {} implies X|`R = id X)
proof
thus id X c= R & id(X) * (R \ id X) = {} implies R|X = id X
proof
assume that
A1: id(X) c= R and
A2: id(X) * (R \ id(X)) = {};
R|X = id(X) * R by RELAT_1:65
.= id(X) * (R \/ id(X)) by A1,XBOOLE_1:12
.= id(X) * ((R \ id(X)) \/ id(X)) by XBOOLE_1:39
.= {} \/ id(X) * id(X) by A2,RELAT_1:32
.= id(X) by Th12;
hence thesis;
end;
assume that
A3: id(X) c= R and
A4: (R \ id X) * id X = {};
X|`R = R * id X by RELAT_1:92
.= (R \/ id X) * id X by A3,XBOOLE_1:12
.= ((R \ id X) \/ id X) * id X by XBOOLE_1:39
.= {} \/ id(X) * id X by A4,Th6
.= id X by Th12;
hence thesis;
end;
theorem
(id(dom CL R) * (R \ id(dom CL R)) = {} implies R|(dom CL R) = id dom CL R &
R|(rng CL R) = id dom CL R) &
((R \ id rng CL R) * id(rng CL R) = {} implies
(dom CL R)|`R = id dom CL R &
(rng CL R)|`R = id rng CL R)
proof
thus id(dom CL R) * (R \ id dom CL R) = {} implies
R|(dom CL R) = id(dom CL R) & R|(rng CL R) = id dom CL R
proof
assume
A1: id(dom CL R) * (R \ id dom CL R) = {};
id(dom CL R) c= R by Th34;
then R|(dom CL R) = id dom CL R by A1,Th35;
hence thesis by Th26;
end;
assume
A2: (R \ id rng CL R) * id rng CL R = {};
id rng CL R c= R by Th34;
then (rng CL R)|`R = id rng CL R by A2,Th35;
then (dom CL R)|`R = id rng CL R by Th26;
hence thesis by Th26;
end;
theorem
(R * (R \ id dom R) = {} implies id(dom CL R) * (R \ id dom CL R) = {}) &
((R \ id dom R) * R = {} implies
(R \ id dom CL R) * id dom CL R = {})
proof
thus R * (R \ id dom R) = {} implies id (dom CL R) * (R \ id dom CL R) = {}
proof
A1: id dom CL R c= R by Th34;
assume
A2: R * (R \ id dom R) = {};
R \ id dom R = R \ CL R by XBOOLE_1:47
.= R \ id dom CL R by Th28;
hence thesis by A2,A1,RELAT_1:30,XBOOLE_1:3;
end;
A3: id dom CL R c= R by Th34;
assume
A4: (R \ id dom R) * R = {};
R \ id dom R = R \ CL R by XBOOLE_1:47
.= R \ id dom CL R by Th28;
hence thesis by A4,A3,RELAT_1:29,XBOOLE_1:3;
end;
theorem Th38:
(S * R = S & R * (R \ id dom R) = {} implies S * (R \ id dom R) = {}) &
(R * S = S & (R \ id dom R) * R = {} implies (R \ id dom R) * S = {})
proof
thus S * R = S & R * (R \ id dom R) = {} implies S * (R \ id dom R) = {}
proof
assume S * R = S & R * (R \ id dom R) = {};
then S * (R \ id dom R) = S * {} by RELAT_1:36
.= {};
hence thesis;
end;
assume R * S = S & (R \ id dom R) * R = {};
then (R \ id dom R) * S = {} * S by RELAT_1:36
.= {};
hence thesis;
end;
theorem Th39:
(S * R = S & R * (R \ id dom R) = {} implies CL(S) c= CL(R)) &
(R * S = S & (R \ id dom R) * R = {} implies CL(S) c= CL(R))
proof
thus S * R = S & R * (R \ id dom R) = {} implies CL S c= CL R
proof
assume that
A1: S * R = S and
A2: R * (R \ id dom R) = {};
A3: S * (R \ id dom R) = {} by A1,A2,Th38;
for x,y being object holds [x,y] in CL S implies [x,y] in CL R
proof
let x,y be object;
assume
A4: [x,y] in CL S; then
A5: [x,y] in id dom S by XBOOLE_0:def 4;
[x,y] in S by A4,XBOOLE_0:def 4;
then consider z being object such that
A6: [x,z] in S and
A7: [z,y] in R by A1,RELAT_1:def 8;
A8: z = y
proof
assume z <> y;
then not [z,y] in id dom R by RELAT_1:def 10;
then [z,y] in R \ id dom R by A7,XBOOLE_0:def 5;
hence contradiction by A3,A6,RELAT_1:def 8;
end;
A9: x = y by A5,RELAT_1:def 10;
then x in dom R by A7,A8,XTUPLE_0:def 12;
then
A10: [x,y] in id dom R by A9,RELAT_1:def 10;
[x,y] in R by A5,A7,A8,RELAT_1:def 10;
hence thesis by A10,XBOOLE_0:def 4;
end;
hence thesis;
end;
assume that
A11: R * S = S and
A12: (R \ id dom R) * R = {};
A13: (R \ id dom R) * S = {} by A11,A12,Th38;
for x,y being object holds [x,y] in CL S implies [x,y] in CL R
proof
let x,y be object;
assume
A14: [x,y] in CL S; then
A15: [x,y] in id dom S by XBOOLE_0:def 4; then
A16: x = y by RELAT_1:def 10;
[x,y] in S by A14,XBOOLE_0:def 4;
then consider z being object such that
A17: [x,z] in R and
A18: [z,y] in S by A11,RELAT_1:def 8;
x in dom R by A17,XTUPLE_0:def 12; then
A19: [x,y] in id dom R by A16,RELAT_1:def 10;
z = x
proof
assume z <> x;
then not [x,z] in id dom R by RELAT_1:def 10;
then [x,z] in R \ id dom R by A17,XBOOLE_0:def 5;
hence contradiction by A13,A18,RELAT_1:def 8;
end;
then [x,y] in R by A15,A17,RELAT_1:def 10;
hence thesis by A19,XBOOLE_0:def 4;
end;
hence thesis;
end;
theorem
(S * R = S & R * (R \ id dom R) = {} & R * S = R &
S * (S \ id dom S) = {} implies CL S = CL R) &
(R * S = S & (R \ id dom R) * R = {} & S * R = R &
(S \ id dom S) * S = {} implies CL S = CL R)
by Th39;