:: Properties of First and Second Order Cutting of Binary Relations
:: by Krzysztof Retel
::
:: Received April 25, 2005
:: Copyright (c) 2005-2026 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, EQREL_1, XBOOLE_0, SUBSET_1, TARSKI, SETFAM_1, ZFMISC_1,
FUNCT_1, RELSET_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1,
FUNCT_1, RELSET_1, FUNCT_2, EQREL_1;
constructors SETFAM_1, FUNCT_2, EQREL_1, RELSET_1, DOMAIN_1, XTUPLE_0;
registrations XBOOLE_0, SUBSET_1, RELAT_1, PARTFUN1, RELSET_1;
requirements SUBSET, BOOLE;
definitions XBOOLE_0, TARSKI, RELAT_1;
equalities EQREL_1, SUBSET_1, RELAT_1;
expansions XBOOLE_0, TARSKI;
theorems RELAT_1, TARSKI, SETFAM_1, ZFMISC_1, XBOOLE_1, SUBSET_1, RELSET_1,
XBOOLE_0, FUNCT_1, FUNCT_2, MSSUBFAM, EQREL_1, SYSREL, ORDERS_1,
XTUPLE_0;
schemes CLASSES1, DOMAIN_1;
begin :: Preliminaries
:: Formalisation of first paragraph from the article:
:: "Relations binaries, fermetures, correspondances de Galois" (1948),
:: Prof. Jacques Riguet,
:: Bulettin de la S.M.F., tome 76 (1948), p.114-155.
reserve x,y for object,X,Y,A,B,C,M for set;
reserve P,Q,R,R1,R2 for Relation;
notation
let X be set;
synonym {_{X}_} for SmallestPartition X;
end;
theorem Th1:
y in {_{X}_} iff ex x st y = {x} & x in X
proof
thus y in {_{X}_} implies ex x st y = {x} & x in X
proof
assume
A1: y in {_{X}_};
per cases;
suppose
A2: X is empty;
ex x being object st x in X & y = Class(id X,x) by A1,EQREL_1:def 3;
hence thesis by A2;
end;
suppose X is non empty;
then reconsider X9 = X as non empty set;
y in the set of all {x} where x is Element of X9 by A1,EQREL_1:37;
then ex x being Element of X9 st ( y = {x});
hence thesis;
end;
end;
given x such that
A3: y = {x} and
A4: x in X;
reconsider X9 = X as non empty set by A4;
y in the set of all {z} where z is Element of X9 by A3,A4;
hence thesis by EQREL_1:37;
end;
theorem Th2:
X = {} iff {_{X}_} = {}
proof
thus X = {} implies {_{X}_} = {}
proof
assume
A1: X = {};
assume not thesis;
then consider y being object such that
A2: y in {_{X}_} by XBOOLE_0:def 1;
ex x being object st ( y = {x})&( x in X) by A2,Th1;
hence contradiction by A1;
end;
assume
A3: {_{X}_} = {};
assume not thesis;
then consider x being object such that
A4: x in X by XBOOLE_0:def 1;
{x} in {_{X}_} by A4,Th1;
hence contradiction by A3;
end;
theorem Th3:
{_{X\/Y}_} = {_{X}_} \/ {_{Y}_}
proof
thus {_{X\/Y}_} c= {_{X}_} \/ {_{Y}_}
proof
let y be object;
assume y in {_{X\/Y}_};
then consider x being object such that
A1: y = {x} and
A2: x in X\/Y by Th1;
x in X or x in Y by A2,XBOOLE_0:def 3;
then y in {_{X}_} or y in {_{Y}_} by A1,Th1;
hence thesis by XBOOLE_0:def 3;
end;
let y be object;
assume
A3: y in {_{X}_} \/ {_{Y}_};
per cases by A3,XBOOLE_0:def 3;
suppose y in {_{X}_};
then consider x being object such that
A4: y = {x} and
A5: x in X by Th1;
x in X\/Y by A5,XBOOLE_0:def 3;
hence thesis by A4,Th1;
end;
suppose y in {_{Y}_};
then consider x being object such that
A6: y = {x} and
A7: x in Y by Th1;
x in X\/Y by A7,XBOOLE_0:def 3;
hence thesis by A6,Th1;
end;
end;
theorem Th4:
{_{X/\Y}_} = {_{X}_} /\ {_{Y}_}
proof
thus {_{X/\Y}_} c= {_{X}_} /\ {_{Y}_}
proof
let y be object;
assume y in {_{X/\Y}_};
then consider x being object such that
A1: y = {x} and
A2: x in X/\Y by Th1;
A3: x in X by A2,XBOOLE_0:def 4;
A4: x in Y by A2,XBOOLE_0:def 4;
A5: y in {_{X}_} by A1,A3,Th1;
y in {_{Y}_} by A1,A4,Th1;
hence thesis by A5,XBOOLE_0:def 4;
end;
let y be object;
assume
A6: y in {_{X}_} /\ {_{Y}_};
then
A7: y in {_{X}_} by XBOOLE_0:def 4;
A8: y in {_{Y}_} by A6,XBOOLE_0:def 4;
consider x being object such that
A9: y = {x} and
A10: x in X by A7,Th1;
consider x1 being object such that
A11: y = {x1} and
A12: x1 in Y by A8,Th1;
x = x1 by A9,A11,ZFMISC_1:3;
then x in X /\ Y by A10,A12,XBOOLE_0:def 4;
hence thesis by A9,Th1;
end;
theorem
{_{X\Y}_} = {_{X}_} \ {_{Y}_}
proof
thus {_{X\Y}_} c= {_{X}_} \ {_{Y}_}
proof
let y be object;
assume y in {_{X\Y}_};
then consider x being object such that
A1: y = {x} and
A2: x in X\Y by Th1;
A3: not x in Y by A2,XBOOLE_0:def 5;
A4: y in {_{X}_} by A1,A2,Th1;
not y in {_{Y}_}
proof
assume not thesis;
then ex x1 being object st ( y = {x1})&( x1 in Y) by Th1;
hence contradiction by A1,A3,ZFMISC_1:3;
end;
hence thesis by A4,XBOOLE_0:def 5;
end;
let y be object;
assume
A5: y in {_{X}_} \ {_{Y}_};
then
A6: y in {_{X}_};
A7: not y in {_{Y}_} by A5,XBOOLE_0:def 5;
consider x being object such that
A8: y = {x} and
A9: x in X by A6,Th1;
not x in Y by A7,A8,Th1;
then x in X\Y by A9,XBOOLE_0:def 5;
hence thesis by A8,Th1;
end;
theorem Th6:
X c= Y iff {_{X}_} c= {_{Y}_}
proof
thus X c= Y implies {_{X}_} c= {_{Y}_}
proof
assume
A1: X c= Y;
let y be object;
assume y in {_{X}_};
then ex x being object st ( y = {x})&( x in X) by Th1;
hence thesis by A1,Th1;
end;
assume
A2: {_{X}_} c= {_{Y}_};
let y be object;
assume y in X;
then {y} in {_{X}_} by Th1;
then ex x1 being object st ( {y} = {x1})&( x1 in Y) by A2,Th1;
hence thesis by ZFMISC_1:3;
end;
theorem
for B1, B2 being Subset-Family of M holds
Intersect(B1) /\ Intersect(B2) c= Intersect(B1 /\ B2)
proof
let B1, B2 be Subset-Family of M;
Intersect(B1 \/ B2) c= Intersect(B1 /\ B2) by SETFAM_1:44,XBOOLE_1:29;
hence thesis by MSSUBFAM:8;
end;
theorem :: (27.2)
(P /\ Q)*R c= (P*R) /\ (Q*R)
proof
let x,y be object;
assume [x,y] in (P /\ Q)*R;
then consider z being object such that
A1: [x,z] in P/\Q and
A2: [z,y] in R by RELAT_1:def 8;
A3: [x,z] in P by A1,XBOOLE_0:def 4;
A4: [x,z] in Q by A1,XBOOLE_0:def 4;
A5: [x,y] in P*R by A2,A3,RELAT_1:def 8;
[x,y] in Q*R by A2,A4,RELAT_1:def 8;
hence thesis by A5,XBOOLE_0:def 4;
end;
begin
theorem Th9:
y in Im(R,x) iff [x,y] in R
proof
thus y in Im(R,x) implies [x,y] in R
proof
assume y in Im(R,x);
then ex a being object st ( [a,y] in R)&( a in {x}) by RELAT_1:def 13;
hence thesis by TARSKI:def 1;
end;
assume
A1: [x,y] in R;
x in {x} by TARSKI:def 1;
hence thesis by A1,RELAT_1:def 13;
end;
theorem Th10:
Im(R1 \/ R2,x) = Im(R1,x) \/ Im(R2,x)
proof
thus Im(R1 \/ R2,x) c= Im(R1,x) \/ Im(R2,x)
proof
let y be object;
assume y in Im(R1 \/ R2,x);
then [x,y] in R1 \/ R2 by Th9;
then [x,y] in R1 or [x,y] in R2 by XBOOLE_0:def 3;
then y in Im(R1,x) or y in Im(R2,x) by Th9;
hence thesis by XBOOLE_0:def 3;
end;
let y be object;
assume
A1: y in Im(R1,x) \/ Im(R2,x);
per cases by A1,XBOOLE_0:def 3;
suppose y in Im(R1,x);
then [x,y] in R1 by Th9;
then [x,y] in R1\/R2 by XBOOLE_0:def 3;
hence thesis by Th9;
end;
suppose y in Im(R2,x);
then [x,y] in R2 by Th9;
then [x,y] in R1\/R2 by XBOOLE_0:def 3;
hence thesis by Th9;
end;
end;
theorem Th11:
Im(R1 /\ R2,x) = Im(R1,x) /\ Im(R2,x)
proof
thus Im(R1 /\ R2,x) c= Im(R1,x) /\ Im(R2,x)
proof
let y be object;
assume y in Im(R1 /\ R2,x);
then
A1: [x,y] in R1/\R2 by Th9;
then
A2: [x,y] in R1 by XBOOLE_0:def 4;
A3: [x,y] in R2 by A1,XBOOLE_0:def 4;
A4: y in Im(R1,x) by A2,Th9;
y in Im(R2,x) by A3,Th9;
hence thesis by A4,XBOOLE_0:def 4;
end;
let y be object;
assume
A5: y in Im(R1,x) /\ Im(R2,x);
then
A6: y in Im(R1,x) by XBOOLE_0:def 4;
A7: y in Im(R2,x) by A5,XBOOLE_0:def 4;
A8: [x,y] in R1 by A6,Th9;
[x,y] in R2 by A7,Th9;
then [x,y] in R1 /\ R2 by A8,XBOOLE_0:def 4;
hence thesis by Th9;
end;
theorem
Im(R1 \ R2,x) = Im(R1,x) \ Im(R2,x)
proof
thus Im(R1\R2,x) c= Im(R1,x) \ Im(R2,x)
proof
let y be object;
assume y in Im(R1\R2,x);
then
A1: [x,y] in R1\R2 by Th9;
then
A2: not [x,y] in R2 by XBOOLE_0:def 5;
A3: y in Im(R1,x) by A1,Th9;
not y in Im(R2,x) by A2,Th9;
hence thesis by A3,XBOOLE_0:def 5;
end;
let y be object;
assume
A4: y in Im(R1,x) \ Im(R2,x);
then
A5: not y in Im(R2,x) by XBOOLE_0:def 5;
A6: [x,y] in R1 by A4,Th9;
not [x,y] in R2 by A5,Th9;
then [x,y] in R1\R2 by A6,XBOOLE_0:def 5;
hence thesis by Th9;
end;
theorem
(R1 /\ R2).:{_{X}_} c= R1.:{_{X}_} /\ R2.:{_{X}_}
proof
let y be object;
assume y in (R1 /\ R2).:{_{X}_};
then consider x being object such that
A1: [x,y] in R1 /\ R2 and
A2: x in {_{X}_} by RELAT_1:def 13;
A3: [x,y] in R1 by A1,XBOOLE_0:def 4;
A4: [x,y] in R2 by A1,XBOOLE_0:def 4;
A5: y in R1.:{_{X}_} by A2,A3,RELAT_1:def 13;
y in R2.:{_{X}_} by A2,A4,RELAT_1:def 13;
hence thesis by A5,XBOOLE_0:def 4;
end;
definition
let X,Y be set;
let R be Relation of X,Y;
let x be object;
redefine func Im(R,x) -> Subset of Y; :: redefines Im (RELAT_1, definition)
coherence
proof
Im(R,x) = R.:{x};
hence thesis;
end;
redefine func Coim(R,x) -> Subset of X; :: redefines Coim (RELAT_1, definition)
coherence
proof
Coim(R,x) = R"{x};
hence thesis;
end;
end;
theorem
for A being set, F being Subset-Family of A, R be Relation holds
R.: union F = union {R.:X where X is Subset of A: X in F} :: (3.1.1)
proof
let A be set, F be Subset-Family of A, R be Relation;
thus R.: union F c= union {R.:f where f is Subset of A: f in F}
proof
let y be object;
assume y in R.:(union F);
then consider x being object such that
A1: [x,y] in R and
A2: x in union F by RELAT_1:def 13;
consider Y being set such that
A3: x in Y and
A4: Y in F by A2,TARSKI:def 4;
set Z = R.:Y;
A5: y in Z by A1,A3,RELAT_1:def 13;
Z in {R.:f where f is Subset of A: f in F} by A4;
hence thesis by A5,TARSKI:def 4;
end;
let y be object;
assume y in union {R.:f where f is Subset of A: f in F};
then consider Y being set such that
A6: y in Y and
A7: Y in {R.:f where f is Subset of A: f in F} by TARSKI:def 4;
consider f being Subset of A such that
A8: Y = R.:f and
A9: f in F by A7;
consider x being object such that
A10: [x,y] in R and
A11: x in f by A6,A8,RELAT_1:def 13;
x in union F by A9,A11,TARSKI:def 4;
hence thesis by A10,RELAT_1:def 13;
end;
:: (3.1.2) - RELAT_1:149
theorem Th15:
for A being set, X being Subset of A holds
X = union {{x} where x is Element of A: x in X}
proof
let A be set, X be Subset of A;
thus X c= union {{x} where x is Element of A: x in X}
proof
let a be object;
assume
A1: a in X;
set Y = {a};
A2: a in Y by TARSKI:def 1;
Y in {{x} where x is Element of A: x in X} by A1;
hence thesis by A2,TARSKI:def 4;
end;
let a be object;
assume a in union {{x} where x is Element of A: x in X};
then consider Y being set such that
A3: a in Y and
A4: Y in {{x} where x is Element of A: x in X} by TARSKI:def 4;
ex x being Element of A st ( Y = {x})&( x in X) by A4;
hence thesis by A3,TARSKI:def 1;
end;
theorem
for A being set, X being Subset of A holds
{{x} where x is Element of A: x in X} is Subset-Family of A
proof
let A be set, X be Subset of A;
{{x} where x is Element of A: x in X} c= bool A
proof
let a be object;
reconsider aa=a as set by TARSKI:1;
assume a in {{x} where x is Element of A: x in X};
then ex x being Element of A st ( a = {x})&( x in X);
then aa c= A by ZFMISC_1:31;
hence thesis;
end;
hence thesis;
end;
theorem :: R(X) - original counterpart. The First Order Cutting.
for A, B being set, X being Subset of A, R being Relation of A,B
holds R.:X = union {Class(R,x) where x is Element of A: x in X}
proof
let A, B be set, X be Subset of A, R be Relation of A,B;
thus R.:X c= union {Class(R,x) where x is Element of A: x in X}
proof
let y be object;
assume y in R.:X;
then consider x1 being object such that
A1: [x1,y] in R and
A2: x1 in X by RELAT_1:def 13;
x1 in union {{x} where x is Element of A: x in X} by A2,Th15;
then consider S being set such that
A3: x1 in S and
A4: S in {{x} where x is Element of A: x in X} by TARSKI:def 4;
consider x being Element of A such that
A5: S = {x} and
A6: x in X by A4;
A7: y in R.:{x} by A1,A3,A5,RELAT_1:def 13;
set Y = R.:{x};
Y = Class(R,x);
then Y in {Class(R,xs) where xs is Element of A: xs in X} by A6;
hence thesis by A7,TARSKI:def 4;
end;
let a be object;
assume a in union {Class(R,x) where x is Element of A: x in X};
then consider Y being set such that
A8: a in Y and
A9: Y in {Class(R,x) where x is Element of A: x in X} by TARSKI:def 4;
consider x being Element of A such that
A10: Y = Class(R,x) and
A11: x in X by A9;
Y c= R.:X
proof
let b be object;
assume b in Y;
then consider x1 being object such that
A12: [x1,b] in R and
A13: x1 in {x} by A10,RELAT_1:def 13;
x1 = x by A13,TARSKI:def 1;
hence thesis by A11,A12,RELAT_1:def 13;
end;
hence thesis by A8;
end;
theorem
for A being non empty set, B being set, X being Subset of A,
R being Relation of A,B holds
{R.:x where x is Element of A: x in X} is Subset-Family of B
proof
let A be non empty set, B be set, X be Subset of A, R be Relation of A,B;
deffunc F(Element of A) = R.:$1;
defpred P[set] means $1 in X;
set Y = { F(x) where x is Element of A: P[x]};
thus Y is Subset-Family of B from DOMAIN_1:sch 8;
end;
definition
let A be set, R be Relation;
func .:(R,A) -> Function means
:Def1:
dom it = bool A & for X being set st X c= A holds it.X = R.:X;
existence
proof
defpred P[object,object] means for X st $1=X holds $2 = R.:X;
A1: for x being object st x in bool A ex y being object st P[x,y]
proof
let x be object such that x in bool A;
reconsider x as set by TARSKI:1;
take R.:x;
thus thesis;
end;
consider g being Function such that
A2: dom g = bool A and
A3: for x be object st x in bool A holds P[x,g.x] from CLASSES1:sch 1(A1);
take g;
thus thesis by A2,A3;
end;
uniqueness
proof
let R1,R2 be Function such that
A4: dom R1 = bool A and
A5: for X st X c= A holds R1.X = R.:X and
A6: dom R2 = bool A and
A7: for X st X c= A holds R2.X = R.:X;
for x being object st x in bool A holds R1.x = R2.x
proof
let x be object;
assume
A8: x in bool A;
reconsider xx=x as set by TARSKI:1;
R1.x = R.:xx by A5,A8;
hence thesis by A7,A8;
end;
hence thesis by A4,A6,FUNCT_1:2;
end;
end;
notation
let B,A be set;
let R be Subset of [:A,B:];
synonym .:R for .:(R,A);
end;
theorem Th19:
for A,B being set, R being Subset of [:A,B:] st
X in dom(.:R) holds (.:R).X = R.:X
proof
let A,B be set;
let R be Subset of [:A,B:];
assume X in dom (.:R);
then X in bool A by Def1;
hence thesis by Def1;
end;
theorem Th20:
for A,B being set, R being Subset of [:A,B:] holds rng(.:R) c= bool rng R
proof
let A,B be set, R be Subset of [:A,B:];
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in rng(.:R);
then consider x be object such that
A1: x in dom(.:R) and
A2: y = (.:R).x by FUNCT_1:def 3;
reconsider x as set by TARSKI:1;
y = R.:x by A1,A2,Th19;
then yy c= rng R by RELAT_1:111;
hence thesis;
end;
theorem Th21:
for A,B being set, R being Subset of [:A,B:] holds
.:R is Function of bool A, bool rng R
proof
let A,B be set, R be Subset of [:A,B:];
A1: dom .:R = bool A by Def1;
rng.:R c= bool rng R by Th20;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
definition
let B,A be set;
let R be Subset of [:A,B:];
redefine func .:R -> Function of bool A, bool B; :: redefines .: (RELSET_2, synonym) → .: (RELSET_2, definition)
correctness
proof
A1: dom .:R = bool A by Def1;
.:R is Function of bool A,bool rng R by Th21;
then
A2: rng .:R c= bool rng R by RELAT_1:def 19;
bool rng R c= bool B by ZFMISC_1:67;
then rng .:R c= bool B by A2;
hence thesis by A1,FUNCT_2:def 1,RELSET_1:4;
end;
end;
theorem :: FUNCT_3:15
for A,B being set, R being Subset of [:A,B:] holds
union((.:R).:A) c= R.:(union A)
proof
let A,B be set, R be Subset of [:A,B:];
let y be object;
assume y in union((.:R).:A);
then consider Z being set such that
A1: y in Z and
A2: Z in (.:R).:A by TARSKI:def 4;
consider X being object such that
A3: X in dom(.:R) and
A4: X in A and
A5: Z = (.:R).X by A2,FUNCT_1:def 6;
reconsider X as set by TARSKI:1;
y in R.:X by A1,A3,A5,Th19;
then consider x being object such that
A6: [x,y] in R and
A7: x in X by RELAT_1:def 13;
x in union A by A4,A7,TARSKI:def 4;
hence thesis by A6,RELAT_1:def 13;
end;
begin :: The second order cutting of binary relation of two sets A,B
:: under a subset of the set A
reserve X,X1,X2 for Subset of A;
reserve Y for Subset of B;
reserve R,R1,R2 for Subset of [:A,B:];
reserve FR for Subset-Family of [:A,B:];
definition
let A,B be set, X be Subset of A, R be Subset of [:A,B:];
func R.:^X -> set equals
Intersect(.:R.:{_{X}_});
:: R[X] - original counterpart. The Second Order Cutting.
correctness;
end;
definition
let A,B be set;
let X be Subset of A;
let R be Subset of [:A,B:];
redefine func R.:^X -> Subset of B; :: redefines .:^ (RELSET_2, definition)
coherence;
end;
theorem Th23:
.:R.:{_{X}_} = {} iff X = {}
proof
thus .:R.:{_{X}_} = {} implies X = {}
proof
assume .:R.:{_{X}_} = {};
then dom .:R misses {_{X}_} by RELAT_1:118;
then
A1: bool A misses {_{X}_} by Def1;
{_{X}_} c= bool A
proof
let y be object;
reconsider yy=y as set by TARSKI:1;
assume y in {_{X}_};
then consider x being object such that
A2: y = {x} and
A3: x in X by Th1;
A4: x in A by A3;
yy c= A
by A2,A4,TARSKI:def 1;
hence thesis;
end;
then
A5: bool A /\ {_{X}_} = {_{X}_} by XBOOLE_1:28;
assume X <> {};
then {_{X}_} <> {} by Th2;
hence thesis by A1,A5;
end;
assume X = {};
then {_{X}_} = {} by Th2;
hence thesis;
end;
theorem Th24:
y in R.:^X implies for x being set st x in X holds y in Im(R,x)
proof
assume
A1: y in R.:^X;
per cases;
suppose .:R.:{_{X}_} = {};
hence thesis by Th23;
end;
suppose .:R.:{_{X}_} <> {};
then
A2: y in meet (.:R.:{_{X}_}) by A1,SETFAM_1:def 9;
for x being set st x in X holds y in R.:{x}
proof
let x be set;
assume
A3: x in X;
then
A4: {x} in {_{X}_} by Th1;
A5: {x} c= A
proof
let a be object;
assume a in {x};
then a = x by TARSKI:def 1;
hence thesis by A3;
end;
then
A6: .:R.{x} = R.:{x} by Def1;
dom .:R = bool A by Def1;
then [{x},R.:{x}] in .:R by A5,A6,FUNCT_1:1;
then R.:{x} in .:R.:{_{X}_} by A4,RELAT_1:def 13;
hence thesis by A2,SETFAM_1:def 1;
end;
hence thesis;
end;
end;
theorem Th25:
for B being non empty set, A being set, X being Subset of A,
y being Element of B, R being Subset of [:A,B:] holds
y in R.:^X iff for x being set st x in X holds y in Im(R,x)
proof
let B be non empty set, A be set, X be Subset of A, y be Element of B,
R be Subset of [:A,B:];
thus
y in R.:^X implies for x being set st x in X holds y in Im(R,x) by Th24;
assume
A1: for x being set st x in X holds y in Im(R,x);
per cases;
suppose .:R.:{_{X}_} = {};
then Intersect(.:R.:{_{X}_}) = B by SETFAM_1:def 9;
hence thesis;
end;
suppose
A2: .:R.:{_{X}_} <> {};
then
A3: Intersect(.:R.:{_{X}_}) = meet (.:R.:{_{X}_}) by SETFAM_1:def 9;
for Y being set holds Y in .:R.:{_{X}_} implies y in Y
proof
let Y be set;
assume Y in .:R.:{_{X}_};
then consider z being object such that
A4: [z,Y] in .:R and
A5: z in {_{X}_} by RELAT_1:def 13;
consider x being object such that
A6: z = {x} and
A7: x in X by A5,Th1;
A8: z in dom .:R by A4,FUNCT_1:1;
Y = .:R.z by A4,FUNCT_1:1;
then Y = Im(R,x) by A6,A8,Def1;
hence thesis by A1,A7;
end;
hence thesis by A2,A3,SETFAM_1:def 1;
end;
end;
theorem
(.:R).:{_{X1}_} = {} implies R.:^(X1\/X2) = R.:^X2
proof
A1: {_{X1\/X2}_} = {_{X1}_} \/ {_{X2}_} by Th3;
assume
A2: (.:R).:{_{X1}_} = {};
R .:^ (X1\/X2) =
Intersect((.:R).:{_{X1}_} \/ ((.:R).:{_{X2}_})) by A1,RELAT_1:120
.= R.:^X2 by A2;
hence thesis;
end;
:: ksiazka S o R = SR a w MML jest to R*S
:: (1) S .:(R.:X) = (S o R).:X
:: w notacji uzytej w MML: S.:(R.:X) = (R*S).:X
theorem :: (2)
R.:^(X1\/X2) = (R.:^X1) /\ (R.:^X2)
proof
R.:^(X1\/X2) = Intersect(.:R.:({_{X1}_} \/ {_{X2}_})) by Th3
.= Intersect(.:R.:{_{X1}_} \/ (.:R.:{_{X2}_})) by RELAT_1:120
.= R.:^X1 /\ (R.:^X2) by MSSUBFAM:8;
hence thesis;
end;
theorem
for A being non empty set, B being set, F being Subset-Family of A,
R being Relation of A,B
holds {R.:^X where X is Subset of A: X in F} is Subset-Family of B
proof
let A be non empty set, B be set, F be Subset-Family of A,
R be Relation of A,B;
deffunc F(Subset of A) = R.:^$1;
defpred P[set] means $1 in F;
set Y = { F(X) where X is Subset of A: P[X]};
thus Y is Subset-Family of B from DOMAIN_1:sch 8;
end;
theorem Th29: :: (3.2.2)
X = {} implies R.:^X = B by Th23,SETFAM_1:def 9;
theorem :: (3.2.1)
for A being set,B being non empty set, R being Relation of A,B,
F being Subset-Family of A, G being Subset-Family of B st
G = {R.:^Y where Y is Subset of A: Y in F} holds R.:^(union F) = Intersect G
proof
let A be set,B be non empty set, R be Relation of A,B,
F be Subset-Family of A, G be Subset-Family of B;
assume
A1: G = {R.:^Y where Y is Subset of A: Y in F};
per cases;
suppose
A2: union F = {};
then
A3: R.:^(union F) = B by Th29;
per cases;
suppose
A4: G <> {};
G c= {B}
proof
let x be object;
assume x in G;
then consider Y being Subset of A such that
A5: x = R.:^Y and
A6: Y in F by A1;
Y = {} by A2,A6,ORDERS_1:6;
then .:R.:{_{Y}_} = {} by Th23;
then Intersect(.:R.:{_{Y}_}) = B by SETFAM_1:def 9;
hence thesis by A5,TARSKI:def 1;
end;
then meet {B} c= meet G by A4,SETFAM_1:6;
then B c= meet G by SETFAM_1:10;
then meet G = B;
hence thesis by A3,SETFAM_1:def 9;
end;
suppose G = {};
hence thesis by A3,SETFAM_1:def 9;
end;
end;
suppose union F <> {};
then consider Z1 being set such that
Z1 <> {} and
A7: Z1 in F by ORDERS_1:6;
reconsider Z1 as Subset of A by A7;
A8: G <> {}
proof
assume not thesis;
then not R.:^Z1 in G;
hence contradiction by A1,A7;
end;
thus R.:^(union F) c= Intersect G
proof
let a be object;
assume
A9: a in R.:^(union F);
for Y being set holds Y in G implies a in Y
proof
let Z2 be set;
assume Z2 in G;
then consider Z3 being Subset of A such that
A10: Z2 = R.:^Z3 and
A11: Z3 in F by A1;
reconsider a as Element of B by A9;
for x being set st x in Z3 holds a in Im(R,x)
proof
let x be set;
assume x in Z3;
then x in union F by A11,TARSKI:def 4;
hence thesis by A9,Th24;
end;
hence thesis by A10,Th25;
end;
then a in meet G by A8,SETFAM_1:def 1;
hence thesis by A8,SETFAM_1:def 9;
end;
let a be object;
assume
A12: a in Intersect G;
then
A13: a in meet G by A8,SETFAM_1:def 9;
reconsider a as Element of B by A12;
for X being set st X in union F holds a in Im(R,X)
proof
let X be set;
assume X in union F;
then consider Z being set such that
A14: X in Z and
A15: Z in F by TARSKI:def 4;
reconsider Z as Subset of A by A15;
set C = R.:^Z;
C in G by A1,A15;
then a in C by A13,SETFAM_1:def 1;
hence thesis by A14,Th24;
end;
hence thesis by Th25;
end;
end;
theorem Th31: :: (4)
X1 c= X2 implies R.:^X2 c= R.:^X1
proof
assume X1 c= X2;
then
A1: {_{X1}_} c= {_{X2}_} by Th6;
let y be object;
assume
A2: y in R.:^X2;
per cases;
suppose
A3: (.:R).:{_{X2}_} = {};
per cases;
suppose (.:R).:{_{X1}_} = {};
then Intersect((.:R).:{_{X1}_}) = B by SETFAM_1:def 9;
hence thesis by A2;
end;
suppose
A4: (.:R).:{_{X1}_} <> {};
for Y being set holds Y in (.:R).:{_{X1}_} implies y in Y
proof
let Y be set;
assume Y in (.:R).:{_{X1}_};
then ex x being object st ( [x,Y] in .:R)&( x in {_{X1}_}) by
RELAT_1:def 13;
hence thesis by A1,A3,RELAT_1:def 13;
end;
then y in meet ((.:R).:{_{X1}_}) by A4,SETFAM_1:def 1;
hence thesis by A4,SETFAM_1:def 9;
end;
end;
suppose (.:R).:{_{X2}_} <> {};
then
A5: y in meet ((.:R).:{_{X2}_}) by A2,SETFAM_1:def 9;
per cases;
suppose (.:R).:{_{X1}_} = {};
then Intersect((.:R).:{_{X1}_}) = B by SETFAM_1:def 9;
hence thesis by A2;
end;
suppose
A6: (.:R).:{_{X1}_} <> {};
(.:R).:{_{X1}_} c= (.:R).:{_{X2}_} by A1,RELAT_1:123;
then meet ((.:R).:{_{X2}_}) c= meet ((.:R).:{_{X1}_}) by A6,SETFAM_1:6;
then y in meet ((.:R).:{_{X1}_}) by A5;
hence thesis by A6,SETFAM_1:def 9;
end;
end;
end;
theorem :: (5)
R.:^X1 \/ R.:^X2 c= R.:^(X1/\X2)
proof
let y be object;
assume
A1: y in R.:^X1 \/ R.:^X2;
A2: {_{X1/\X2}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then
A3: .:R.:({_{X1/\X2}_}) c= .:R.:{_{X1}_} /\ .:R.:{_{X2}_} by RELAT_1:121;
per cases by A1,XBOOLE_0:def 3;
suppose
A4: y in R.:^X1;
y in Intersect((.:R).:({_{X1/\X2}_}))
proof
per cases;
suppose
A5: (.:R).:({_{X1/\X2}_}) <> {};
A6: {_{X1/\X2}_} = {_{X1}_} /\ {_{X2}_} by Th4;
then
A7: (.:R).:({_{X1/\X2}_}) c= (.:R).:{_{X1}_} /\ ((.:R).:{_{X2 }_})
by RELAT_1:121;
A8: (.:R).:{_{X1}_} /\ ((.:R).:{_{X2}_}) <> {} by A5,A6,RELAT_1:121
,XBOOLE_1:3;
(.:R).:{_{X1}_} <> {} by A5,A7;
then
A9: y in meet ((.:R).:{_{X1}_}) by A4,SETFAM_1:def 9;
for Y being set holds
Y in (.:R).:{_{X1}_} /\ (.:R).:{_{X2}_} implies y in Y
proof
let Y be set;
assume Y in (.:R).:{_{X1}_} /\ (.:R).:{_{X2}_};
then Y in (.:R).:{_{X1}_} by XBOOLE_0:def 4;
hence thesis by A9,SETFAM_1:def 1;
end;
then y in meet ((.:R).:{_{X1}_} /\ (.:R).:{_{X2}_}) by A8,SETFAM_1:def 1;
then
A10: y in Intersect ((.:R).:{_{X1}_} /\ (.:R).:{_{X2}_})
by A8,SETFAM_1:def 9;
Intersect(.:R.:{_{X1}_} /\ (.:R.:{_{X2}_})) c=
Intersect(.:R.:({_{X1}_} /\ {_{X2}_})) by RELAT_1:121,SETFAM_1:44;
hence thesis by A2,A10;
end;
suppose (.:R).:({_{X1/\X2}_}) = {};
then Intersect((.:R).:({_{X1/\X2}_})) = B by SETFAM_1:def 9;
hence thesis by A4;
end;
end;
hence thesis;
end;
suppose
A11: y in R.:^X2;
y in Intersect((.:R).:({_{X1/\X2}_}))
proof
per cases;
suppose
A12: (.:R).:({_{X1/\X2}_}) <> {};
then
A13: (.:R).:{_{X1}_} /\ ((.:R).:{_{X2}_}) <> {} by A2,RELAT_1:121,XBOOLE_1:3
;
(.:R).:{_{X2}_} <> {} by A3,A12;
then
A14: y in meet ((.:R).:{_{X2}_}) by A11,SETFAM_1:def 9;
for Y being set holds
Y in (.:R).:{_{X1}_} /\ (.:R).:{_{X2}_} implies y in Y
proof
let Y be set;
assume Y in (.:R).:{_{X1}_} /\ (.:R).:{_{X2}_};
then Y in (.:R).:{_{X2}_} by XBOOLE_0:def 4;
hence thesis by A14,SETFAM_1:def 1;
end;
then y in meet ((.:R).:{_{X1}_} /\ (.:R).:{_{X2}_}) by A13,SETFAM_1:def 1;
then
A15: y in Intersect ((.:R).:{_{X1}_} /\ (.:R).:{_{X2}_})
by A13,SETFAM_1:def 9;
A16: {_{X1/\X2}_} = {_{X1}_} /\ {_{X2}_} by Th4;
Intersect(.:R.:{_{X1}_} /\ (.:R.:{_{X2}_})) c=
Intersect(.:R.:({_{X1}_} /\ {_{X2}_})) by RELAT_1:121,SETFAM_1:44;
hence thesis by A15,A16;
end;
suppose (.:R).:({_{X1/\X2}_}) = {};
then Intersect((.:R).:({_{X1/\X2}_})) = B by SETFAM_1:def 9;
hence thesis by A11;
end;
end;
hence thesis;
end;
end;
theorem :: (6)
(R1 /\ R2).:^X = (R1.:^X) /\ (R2.:^X)
proof
thus (R1 /\ R2).:^X c= (R1.:^X) /\ (R2.:^X)
proof
let y be object;
assume
A1: y in (R1 /\ R2).:^X;
then reconsider B as non empty set;
reconsider y as Element of B by A1;
for x being set st x in X holds y in Im(R1,x)
proof
let x be set;
assume x in X;
then y in Im(R1 /\ R2,x) by A1,Th24;
then y in Im(R1,x) /\ Im(R2,x) by Th11;
hence thesis by XBOOLE_0:def 4;
end;
then
A2: y in R1.:^X by Th25;
for x being set st x in X holds y in Im(R2,x)
proof
let x be set;
assume x in X;
then y in Im(R1 /\ R2,x) by A1,Th24;
then y in Im(R1,x) /\ Im(R2,x) by Th11;
hence thesis by XBOOLE_0:def 4;
end;
then y in R2.:^X by Th25;
hence thesis by A2,XBOOLE_0:def 4;
end;
let y be object;
assume
A3: y in (R1.:^X) /\ (R2.:^X);
then
A4: y in (R1.:^X) by XBOOLE_0:def 4;
A5: y in (R2.:^X) by A3,XBOOLE_0:def 4;
reconsider B as non empty set by A3;
reconsider y as Element of B by A3;
for x being set st x in X holds y in Im(R1/\R2,x)
proof
let x be set;
assume
A6: x in X;
then
A7: y in Im(R1,x) by A4,Th25;
y in Im(R2,x) by A5,A6,Th25;
then y in Im(R1,x) /\ Im(R2,x) by A7,XBOOLE_0:def 4;
hence thesis by Th11;
end;
hence thesis by Th25;
end;
theorem :: (7.1.1)
(union FR).:X = union {R.:X where R is Subset of [:A,B:]: R in FR}
proof
thus
(union FR).:X c= union {R.:X where R is Subset of [:A,B:]: R in FR}
proof
let a be object;
assume a in (union FR).:X;
then consider x being object such that
A1: [x,a] in union FR and
A2: x in X by RELAT_1:def 13;
consider S being set such that
A3: [x,a] in S and
A4: S in FR by A1,TARSKI:def 4;
reconsider S as Subset of [:A,B:] by A4;
ex P being set st
a in P & P in {T.:X where T is Subset of [:A,B:]: T in FR}
proof
set P = S.:X;
A5: a in P by A2,A3,RELAT_1:def 13;
P in {T.:X where T is Subset of [:A,B:]: T in FR} by A4;
hence thesis by A5;
end;
hence thesis by TARSKI:def 4;
end;
let a be object;
assume a in union {R.:X where R is Subset of [:A,B:]: R in FR};
then consider P being set such that
A6: a in P and
A7: P in {R.:X where R is Subset of [:A,B:]: R in FR} by TARSKI:def 4;
consider R being Subset of [:A,B:] such that
A8: P = R.:X and
A9: R in FR by A7;
consider x being object such that
A10: [x,a] in R and
A11: x in X by A6,A8,RELAT_1:def 13;
ex x being set st x in X & [x,a] in union FR
proof
take x;
thus thesis by A9,A10,A11,TARSKI:def 4;
end;
hence thesis by RELAT_1:def 13;
end;
:: (7.1.2) - RELAT_1:150
theorem
for FR being Subset-Family of [:A,B:], A,B being set,
X being Subset of A holds
{R.:^X where R is Subset of [:A,B:]: R in FR} is Subset-Family of B
proof
let FR be Subset-Family of [:A,B:], A,B be set, X be Subset of A;
deffunc F(Subset of [:A,B:]) = $1.:^X;
defpred P[set] means $1 in FR;
set G = { F(R) where R is Subset of [:A,B:]: P[R]};
thus G is Subset-Family of B from DOMAIN_1:sch 8;
end;
:: (11.2) theorem TH40.
theorem Th36: :: (11.1)
R = {} & X <> {} implies R.:^X = {}
proof
assume that
A1: R = {} and
A2: X <> {};
R.:^X c= {}
proof
let a be object;
assume
A3: a in R.:^X;
consider x being object such that
A4: x in X by A2,XBOOLE_0:def 1;
a in Im(R,x) by A3,A4,Th24;
hence thesis by A1;
end;
hence thesis;
end;
theorem Th37: :: (7.2.2)
R = [:A,B:] implies R.:^X = B
proof
assume
A1: R = [:A,B:];
thus R.:^X c= B;
thus B c= R.:^X
proof
let a be object;
assume
A2: a in B;
then reconsider B as non empty set;
reconsider a as Element of B by A2;
for x being set st x in X holds a in Im(R,x)
proof
let x be set;
assume x in X;
then [x,a] in R by A1,ZFMISC_1:87;
hence thesis by Th9;
end;
hence thesis by Th25;
end;
end;
theorem :: (7.2.1)
for G being Subset-Family of B st
G = {R.:^X where R is Subset of [:A,B:]: R in FR} holds
(Intersect FR).:^X = Intersect G
proof
let G be Subset-Family of B;
assume
A1: G = {R.:^X where R is Subset of [:A,B:]: R in FR};
A2: for x being set st G = {x} holds Intersect G = x
proof
let x be set;
assume G = {x};
then Intersect G = meet {x} by SETFAM_1:def 9;
hence thesis by SETFAM_1:10;
end;
per cases;
suppose
A3: X = {};
then
A4: (Intersect FR).:^X = B by Th29;
G c= {B}
proof
let a be object;
assume a in G;
then ex R being Subset of [:A,B:] st ( a = R.:^X)&( R in FR) by A1;
then a = B by A3,Th29;
hence thesis by TARSKI:def 1;
end;
then G = {} or G = {B} by ZFMISC_1:33;
hence thesis by A2,A4,SETFAM_1:def 9;
end;
suppose
A5: X <> {};
per cases;
suppose
A6: FR = {};
then Intersect FR = [:A,B:] by SETFAM_1:def 9;
then
A7: (Intersect FR).:^X = B by Th37;
G c= {B}
proof
let a be object;
assume a in G;
then ex R being Subset of [:A,B:] st ( a = R.:^X)&( R in FR) by A1;
hence thesis by A6;
end;
then G = {} or G = {B} by ZFMISC_1:33;
hence thesis by A2,A7,SETFAM_1:def 9;
end;
suppose
A8: FR <> {};
per cases;
suppose
A9: B = {};
then [:A,B:] = {} by ZFMISC_1:90;
then FR = {} or FR = {{}} by ZFMISC_1:1,33;
then Intersect FR = meet {{}} by A8,SETFAM_1:def 9;
then (Intersect FR).:^X = {} by A5,Th36,SETFAM_1:10;
hence thesis by A9;
end;
suppose B <> {};
then reconsider B as non empty set;
thus (Intersect FR).:^X c= Intersect G
proof
let a be object;
assume
A10: a in (Intersect FR).:^X;
then
A11: a in B;
reconsider a as Element of B by A10;
G <> {} implies a in Intersect G
proof
assume
A12: G <> {};
then
A13: Intersect G = meet G by SETFAM_1:def 9;
for Y being set holds Y in G implies a in Y
proof
let Y be set;
assume Y in G;
then consider R being Subset of [:A,B:] such that
A14: Y = R.:^X and
A15: R in FR by A1;
for x being set st x in X holds a in Im(R,x)
proof
let x be set;
assume x in X;
then a in Im(Intersect FR,x) by A10,Th24;
then [x,a] in Intersect FR by Th9;
then [x,a] in meet FR by A8,SETFAM_1:def 9;
then [x,a] in R by A15,SETFAM_1:def 1;
hence thesis by Th9;
end;
hence thesis by A14,Th25;
end;
hence thesis by A12,A13,SETFAM_1:def 1;
end;
hence thesis by A11,SETFAM_1:def 9;
end;
let a be object;
assume
A16: a in Intersect G;
then reconsider a as Element of B;
consider R being Subset of [:A,B:] such that
A17: R in FR by A8,SUBSET_1:4;
R.:^X in G by A1,A17;
then
A18: a in meet G by A16,SETFAM_1:def 9;
for x being set st x in X holds a in Im(Intersect FR,x)
proof
let x be set such that
A19: x in X;
for Y being set holds Y in FR implies [x,a] in Y
proof
let P be set;
assume
A20: P in FR;
then reconsider P as Subset of [:A,B:];
set S = P.:^X;
S in G by A1,A20;
then a in P.:^X by A18,SETFAM_1:def 1;
then a in Im(P,x) by A19,Th24;
hence thesis by Th9;
end;
then [x,a] in meet FR by A8,SETFAM_1:def 1;
then [x,a] in Intersect FR by A8,SETFAM_1:def 9;
hence thesis by Th9;
end;
hence thesis by Th25;
end;
end;
end;
end;
theorem :: (8)
R1 c= R2 implies R1.:^X c= R2.:^X
proof
assume
A1: R1 c= R2;
let y be object;
assume
A2: y in R1.:^X;
then reconsider B as non empty set;
reconsider y as Element of B by A2;
for x being set st x in X holds y in Im(R2,x)
proof
let x be set;
assume x in X;
then y in Im(R1,x) by A2,Th25;
then [x,y] in R1 by Th9;
hence thesis by A1,Th9;
end;
hence thesis by Th25;
end;
theorem :: (9)
(R1.:^X) \/ (R2.:^X) c= (R1 \/ R2).:^X
proof
let y be object;
assume
A1: y in (R1.:^X) \/ (R2.:^X);
per cases by A1,XBOOLE_0:def 3;
suppose
A2: y in R1.:^X;
then reconsider B as non empty set;
reconsider y as Element of B by A2;
for x being set st x in X holds y in Im(R1 \/ R2,x)
proof
let x be set;
assume x in X;
then y in Im(R1,x) by A2,Th25;
then y in Im(R1,x) \/ Im(R2,x) by XBOOLE_0:def 3;
hence thesis by Th10;
end;
hence thesis by Th25;
end;
suppose
A3: y in R2.:^X;
then reconsider B as non empty set;
reconsider y as Element of B by A3;
for x being set st x in X holds y in Im(R1 \/ R2,x)
proof
let x be set;
assume x in X;
then y in Im(R2,x) by A3,Th25;
then y in Im(R1,x) \/ Im(R2,x) by XBOOLE_0:def 3;
hence thesis by Th10;
end;
hence thesis by Th25;
end;
end;
theorem Th41:
y in Im(R`,x) iff not [x,y] in R & x in A & y in B
proof
thus y in Im(R`,x) implies not [x,y] in R & x in A & y in B
proof
assume y in Im(R`,x);
then ex a being object st ( [a,y] in R`)&( a in {x}) by RELAT_1:def 13;
then [x,y] in [:A,B:] \ R by TARSKI:def 1;
hence thesis by XBOOLE_0:def 5,ZFMISC_1:87;
end;
assume that
A1: not [x,y] in R and
A2: x in A and
A3: y in B;
A4: x in {x} by TARSKI:def 1;
[x,y] in [:A,B:] by A2,A3,ZFMISC_1:87;
then [x,y] in [:A,B:] \ R by A1,XBOOLE_0:def 5;
hence thesis by A4,RELAT_1:def 13;
end;
theorem :: (17)
X <> {} implies R.:^X c= R.:X
proof
assume
A1: X <> {};
let y be object;
assume
A2: y in R.:^X;
consider x being object such that
A3: x in X by A1,XBOOLE_0:def 1;
y in Im(R,x) by A2,A3,Th24;
then [x,y] in R by Th9;
hence thesis by A3,RELAT_1:def 13;
end;
theorem Th43:
for X, Y being set holds
X meets R~.:Y iff ex x,y being set st x in X & y in Y & x in Im(R~,y)
proof
let X, Y be set;
hereby
assume X meets R~.:Y;
then consider a being object such that
A1: a in X and
A2: a in R~.:Y by XBOOLE_0:3;
consider b being object such that
A3: [b,a] in R~ and
A4: b in Y by A2,RELAT_1:def 13;
A5: b in {b} by TARSKI:def 1;
reconsider a,b as set by TARSKI:1;
take a,b;
thus a in X by A1;
thus b in Y by A4;
thus a in Im(R~,b) by A3,A5,RELAT_1:def 13;
end;
given x,y being set such that
A6: x in X and
A7: y in Y and
A8: x in Im(R~,y);
ex a being object st ( [a,x] in R~)&( a in {y}) by A8,RELAT_1:def 13;
then [y,x] in R~ by TARSKI:def 1;
then x in R~.:Y by A7,RELAT_1:def 13;
hence thesis by A6,XBOOLE_0:3;
end;
theorem Th44:
for X, Y being set holds
(ex x,y being set st x in X & y in Y & x in Im(R~,y)) iff Y meets R.:X
proof
let X, Y be set;
thus (ex x,y being set st x in X & y in Y & x in Im(R~,y)) implies
Y meets R.:X
proof
given x,y being set such that
A1: x in X and
A2: y in Y and
A3: x in Im(R~,y);
consider a being object such that
A4: [a,x] in R~ and
A5: a in {y} by A3,RELAT_1:def 13;
a = y by A5,TARSKI:def 1;
then [x,y] in R by A4,RELAT_1:def 7;
then y in R.:X by A1,RELAT_1:def 13;
hence thesis by A2,XBOOLE_0:3;
end;
assume Y meets R.:X;
then consider a being object such that
A6: a in Y and
A7: a in R.:X by XBOOLE_0:3;
consider b being object such that
A8: [b,a] in R and
A9: b in X by A7,RELAT_1:def 13;
A10: [a,b] in R~ by A8,RELAT_1:def 7;
A11: a in {a} by TARSKI:def 1;
reconsider a,b as set by TARSKI:1;
take b,a;
thus b in X by A9;
thus a in Y by A6;
thus thesis by A10,A11,RELAT_1:def 13;
end;
theorem Th45: :: (19)
X misses R~.:Y iff Y misses R.:X
proof
X meets R~.:Y iff ex x,y being set st x in X & y in Y & x in Im(R~,y)
by Th43;
hence thesis by Th44;
end;
theorem Th46: :: (14.1)
for X being set holds R.:X = R.:(X /\ proj1 R)
proof
let X be set;
thus R.:X c= R.:(X /\ proj1 R)
proof
let y be object;
assume y in R.:X;
then consider x being object such that
A1: [x,y] in R and
A2: x in X by RELAT_1:def 13;
x in proj1 R by A1,XTUPLE_0:def 12;
then x in X /\ proj1 R by A2,XBOOLE_0:def 4;
hence thesis by A1,RELAT_1:def 13;
end;
let y be object;
assume y in R.:(X /\ proj1 R);
then consider x being object such that
A3: [x,y] in R and
A4: x in X /\ proj1 R by RELAT_1:def 13;
x in X by A4,XBOOLE_0:def 4;
hence thesis by A3,RELAT_1:def 13;
end;
theorem Th47: :: (14.2)
for Y being set holds (R~).:Y = (R~).:(Y /\ proj2 R)
proof
let Y be set;
thus (R~).:Y c= (R~).:(Y /\ proj2 R)
proof
let y be object;
assume y in (R~).:Y;
then consider x being object such that
A1: [x,y] in R~ and
A2: x in Y by RELAT_1:def 13;
[y,x] in R by A1,RELAT_1:def 7;
then x in proj2 R by XTUPLE_0:def 13;
then x in Y /\ proj2 R by A2,XBOOLE_0:def 4;
hence thesis by A1,RELAT_1:def 13;
end;
let y be object;
assume y in (R~).:(Y /\ proj2 R);
then consider x being object such that
A3: [x,y] in R~ and
A4: x in (Y /\ proj2 R) by RELAT_1:def 13;
x in Y by A4,XBOOLE_0:def 4;
hence thesis by A3,RELAT_1:def 13;
end;
theorem Th48: :: (10.2)
(R.:^X)` = R`.:X
proof
thus (R.:^X)` c= R`.:X
proof
let a be object;
assume
A1: a in (R.:^X)`;
then not a in R.:^X by XBOOLE_0:def 5;
then consider x being set such that
A2: x in X and
A3: not a in Im(R,x) by A1,Th25;
A4: not [x,a] in R by A3,Th9;
[x,a] in [:A,B:] by A1,A2,ZFMISC_1:87;
then [x,a] in [:A,B:] \ R by A4,XBOOLE_0:def 5;
hence thesis by A2,RELAT_1:def 13;
end;
let a be object;
assume a in R`.:X;
then consider x being object such that
A5: [x,a] in R` and
A6: x in X by RELAT_1:def 13;
A7: not [x,a] in R by A5,XBOOLE_0:def 5;
assume not thesis;
then
A8: not a in B or a in R.:^X by XBOOLE_0:def 5;
a in R.:^X implies for x being set st x in X holds [x,a] in R
proof
assume
A9: a in R.:^X;
let x be set;
assume x in X;
then a in Im(R,x) by A9,Th24;
hence thesis by Th9;
end;
hence contradiction by A5,A6,A7,A8,ZFMISC_1:87;
end;
reserve R for Relation of A,B;
reserve S for Relation of B,C;
definition
let A,B,C be set;
let R be Subset of [:A,B:], S be Subset of [:B,C:];
redefine func R*S -> Relation of A,C; :: redefines * (RELAT_1, synonym) → (#) (RELAT_1, definition)
coherence
proof
reconsider R as Relation of A,B;
reconsider S as Relation of B,C;
R*S is Relation of A,C;
hence thesis;
end;
end;
theorem Th49: :: (10.1)
(R.:X)` = (R`).:^X
proof
thus (R.:X)` c= (R`).:^X
proof
let a be object;
assume
A1: a in (R.:X)`;
then reconsider B as non empty set;
reconsider a as Element of B by A1;
assume not thesis;
then consider x being set such that
A2: x in X and
A3: not a in Im(R`,x) by Th25;
[x,a] in R by A2,A3,Th41;
then a in R.:X by A2,RELAT_1:def 13;
hence contradiction by A1,XBOOLE_0:def 5;
end;
let a be object;
assume
A4: a in (R`).:^X;
A5: a in (R`).:^X implies for x being set st x in X holds not [x,a] in R
proof
assume a in (R`).:^X;
let x be set;
assume
A6: x in X;
assume
A7: not thesis;
a in Im(R`,x) by A4,A6,Th24;
then ex b being object st ( [b,a] in R`)&( b in {x}) by RELAT_1:def 13;
then
A8: [x,a] in R` by TARSKI:def 1;
R` misses R by XBOOLE_1:79;
hence contradiction by A7,A8,XBOOLE_0:3;
end;
assume
A9: not thesis;
per cases by A9,XBOOLE_0:def 5;
suppose not a in B;
hence contradiction by A4;
end;
suppose a in R.:X;
then ex y being object st ( [y,a] in R)&( y in X) by RELAT_1:def 13;
hence contradiction by A4,A5;
end;
end;
:: (12) - FUNCT_5:20, RELAT_1:37
theorem Th50:
proj1 R = (R~).:B & proj2 R = R.:A
proof
thus proj1 R = dom R .= rng (R~) by RELAT_1:20
.= (R~).:B by RELSET_1:22;
thus proj2 R = rng R .= R.:A by RELSET_1:22;
end;
theorem :: (13.1)
proj1 (R*S) = (R~).:(proj1 S) & proj1 (R*S) c= proj1 R
proof
thus
A1: proj1 (R*S) = (R*S)~.:C by Th50
.= (S~*R~).:C by RELAT_1:35
.= R~.:(S~.:C) by RELAT_1:126
.= R~.:(proj1 S) by Th50;
proj1 S = dom S;
then proj1 (R*S) c= R~.:B by A1,RELAT_1:123;
hence thesis by Th50;
end;
theorem :: (13.2)
proj2 (R*S) = S.:(proj2 R) & proj2 (R*S) c= proj2 S
proof
thus
A1: proj2 (R*S) = (R*S).:A by Th50
.= S.:(R.:A) by RELAT_1:126
.= S.:(proj2 R) by Th50;
proj2 R = rng R;
then S.:(proj2 R) c= S.:B by RELAT_1:123;
hence thesis by A1,Th50;
end;
theorem :: (15.1)
X c= proj1 R iff X c= (R*(R~)).:X
proof
thus X c= proj1 R implies X c= (R*(R~)).:X
proof
assume
A1: X c= proj1 R;
let x be object;
assume
A2: x in X;
then reconsider x as Element of A;
consider y being object such that
A3: [x,y] in R by A1,A2,XTUPLE_0:def 12;
A4: [y,x] in R~ by A3,RELAT_1:def 7;
y in {y} by TARSKI:def 1;
then
A5: x in (R~).:{y} by A4,RELAT_1:def 13;
(R~).:{y} c= (R*(R~)).:X
proof
let a be object;
assume a in (R~).:{y};
then ex b being object st ( [b,a] in R~)&( b in {y}) by RELAT_1:def 13;
then [y,a] in R~ by TARSKI:def 1;
then [x,a] in R*R~ by A3,RELAT_1:def 8;
hence thesis by A2,RELAT_1:def 13;
end;
hence thesis by A5;
end;
assume
A6: X c= (R*(R~)).:X;
let x be object;
assume x in X;
then
A7: x in (R*(R~)).:X by A6;
A8: (R*R~).:X = (R~).:(R.:X) by RELAT_1:126;
(R~).:(R.:X) c= (R~).:B by RELAT_1:123;
then (R*R~).:X c= proj1 R by A8,Th50;
hence thesis by A7;
end;
theorem :: (15.2)
Y c= proj2 R iff Y c= ((R~)*R).:Y
proof
thus Y c= proj2 R implies Y c= ((R~)*R).:Y
proof
assume
A1: Y c= proj2 R;
let y be object;
assume
A2: y in Y;
then consider x being object such that
A3: [x,y] in R by A1,XTUPLE_0:def 13;
A4: [y,x] in R~ by A3,RELAT_1:def 7;
A5: y in Im(R,x) by A3,Th9;
R.:{x} c= ((R~)*R).:Y
proof
let a be object;
assume a in R.:{x};
then ex b being object st ( [b,a] in R)&( b in {x}) by RELAT_1:def 13;
then [x,a] in R by TARSKI:def 1;
then [y,a] in ((R~)*R) by A4,RELAT_1:def 8;
hence thesis by A2,RELAT_1:def 13;
end;
hence thesis by A5;
end;
assume
A6: Y c= ((R~)*R).:Y;
let x be object;
assume x in Y;
then
A7: x in ((R~)*R).:Y by A6;
A8: ((R~)*R).:Y = R.:((R~).:Y) by RELAT_1:126;
R.:((R~).:Y) c= R.:A by RELAT_1:123;
then ((R~)*R).:Y c= proj2 R by A8,Th50;
hence thesis by A7;
end;
theorem
proj1 R = (R~).:B & (R~).:(R.:A) = (R~).:(proj2 R) by Th50;
theorem :: (16.1)
(R~).:B = (R*(R~)).:A
proof
A1: (R*(R~)).:A = R~.:(R.:A) by RELAT_1:126
.= R~.:(proj2 R) by Th50;
thus (R~).:B c= (R*(R~)).:A
proof
let x be object;
assume
A2: x in (R~).:B;
A3: (R~).:B = (R~).:(B /\ proj2 R) by Th47;
(R~).:(B /\ proj2 R) c= R~.:B /\ R~.:(proj2 R) by RELAT_1:121;
hence thesis by A1,A2,A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (R*(R~)).:A;
proj2 R c= rng R;
then R~.:(proj2 R) c= R~.:B by RELAT_1:123;
hence thesis by A1,A4;
end;
theorem :: (16.2)
R.:A = (R~*R).:B
proof
A1: (R~*R).:B = R.:(R~.:B) by RELAT_1:126
.= R.:(proj1 R) by Th50;
thus R.:A c= (R~*R).:B
proof
let x be object;
assume
A2: x in R.:A;
A3: R.:A = R.:(A /\ proj1 R) by Th46;
R.:(A /\ proj1 R) c= R.:A /\ R.:(proj1 R) by RELAT_1:121;
hence thesis by A1,A2,A3,XBOOLE_0:def 4;
end;
let x be object;
assume
A4: x in (R~*R).:B;
proj1 R c= dom R;
then R.:(proj1 R) c= R.:A by RELAT_1:123;
hence thesis by A1,A4;
end;
theorem :: (18)
S.:^(R.:X) = (R*S`)`.:^X
proof
(S.:^(R.:X))` = S`.:(R.:X) by Th48
.= ((R*(S`)).:X) by RELAT_1:126;
then S.:^(R.:X) = ((R*(S`)).:X)` .= (R*S`)`.:^X by Th49;
hence thesis;
end;
theorem Th59: :: (24.3)
(R`)~ = (R~)`
proof
(R`)~ = ([:A,B:])~ \ R~ by RELAT_1:24
.= (R~)` by SYSREL:5;
hence thesis;
end;
theorem Th60: :: (20)
X c= (R~).:^Y iff Y c= R.:^X
proof
X c= (R~).:^Y iff X misses ((R~).:^Y)` by SUBSET_1:24;
then X c= (R~).:^Y iff X misses (R~)`.:Y by Th48;
then
A1: X c= (R~).:^Y iff X /\ (R~)`.:Y = {};
reconsider S = R` as Relation of A,B;
X misses S~.:Y iff Y misses S.:X by Th45;
then X /\ S~.:Y = {} iff Y /\ S.:X = {};
then X c= (R~).:^Y iff (R.:^X)` /\ Y = {} by A1,Th48,Th59;
then X c= (R~).:^Y iff (R.:^X)` misses Y;
hence thesis by SUBSET_1:24;
end;
theorem :: (21)
R.:(X`) c= Y` iff R~.:Y c= X
proof
X` misses R~.:Y iff Y misses R.:(X`) by Th45;
hence thesis by SUBSET_1:23,24;
end;
theorem :: (22)
X c= (R~).:^(R.:^X) & Y c= R.:^((R~).:^Y) by Th60;
theorem :: (23)
R.:^X = R.:^( R~.:^(R.:^X) ) & R~.:^Y = (R~).:^(R.:^((R~).:^Y))
proof
A1: R.:^X c= R.:^( R~.:^(R.:^X) ) by Th60;
X c= (R~).:^(R.:^X) by Th60;
then
R.:^( R~.:^(R.:^X) ) c= R.:^X by Th31;
hence R.:^X = R.:^( R~.:^(R.:^X) ) by A1;
thus R~.:^Y c= (R~).:^(R.:^((R~).:^Y)) by Th60;
Y c= R.:^((R~).:^Y) by Th60;
hence thesis by Th31;
end;
theorem :: (29.3)
(id A)*R = R*(id B)
proof
(id A)*R = R by FUNCT_2:17
.= R*(id B) by FUNCT_2:17;
hence thesis;
end;
:: (24.1) - RELAT_1:40
:: (24.2) - RELAT_1:39
:: (24.4) - RELAT_1:54
:: (24.5) - R1 c= R2 implies R1~ c= R2~ :: SYSREL:27
:: (24.6) - R~~ = R; atomatically
:: (25.1) - RELAT_1:51
:: (25.2) - (S1 \/ S2)*R = S1*R \/ S2*R :: SYSREL:20
:: (26) - RELAT_1:50
:: (27.1) - RELAT_1:52
:: (28.1) and (28.2) - RELAT_1:62
:: (29.1) and (29.2) - FUNCT_2:23