:: Relations and Their Basic Properties
:: by Edmund Woronowicz
::
:: Received March 15, 1989
:: Copyright (c) 1990-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 XBOOLE_0, TARSKI, ZFMISC_1, SUBSET_1, RELAT_1, VALUED_1;
notations TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, SUBSET_1;
constructors TARSKI, SUBSET_1, ZFMISC_1, XTUPLE_0, XBOOLE_0;
registrations XBOOLE_0, ZFMISC_1, XTUPLE_0;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0, ZFMISC_1;
equalities TARSKI, XBOOLE_0;
expansions TARSKI, XBOOLE_0;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XBOOLE_1, XTUPLE_0;
schemes XBOOLE_0;
begin
reserve A,X,X1,X2,Y,Y1,Y2 for set, a,b,c,d,x,y,z for object;
definition
let IT be set;
attr IT is Relation-like means
:Def1:
x in IT implies ex y,z st x = [y,z];
end;
registration
cluster empty -> Relation-like for set;
coherence;
end;
definition
mode Relation is Relation-like set;
end;
reserve P,P1,P2,Q,R,S for Relation;
registration
let R be Relation;
cluster -> Relation-like for Subset of R;
coherence
by Def1;
end;
scheme
RelExistence{A,B() -> set, P[object,object]}:
ex R being Relation st for x,y holds
[x,y] in R iff x in A() & y in B() & P[x,y]
proof
ex R being Relation st
for p being object holds p in R iff p in [:A(),B():]
& ex x,y st p=[x,y] & P[x,y]
proof
defpred Q[object] means ex x,y st $1=[x,y] & P[x,y];
consider B being set such that
A1: for p being object holds p in B iff p in [:A(),B():] & Q[p] from
XBOOLE_0:sch 1;
for p being object st p in B holds ex x,y st p = [x,y]
proof
let p be object;
assume p in B;
then ex x,y st p=[x,y] & P[x,y] by A1;
hence thesis;
end;
then B is Relation by Def1;
hence thesis by A1;
end;
then consider R being Relation such that
A2: for p being object holds p in R iff p in [:A(),B():] & ex x,y st p=[x,y] &
P[x,y];
take R;
let x,y;
thus [x,y] in R implies x in A() & y in B() & P[x,y]
proof
assume
A3: [x,y] in R;
then consider xx,yy being object such that
A4: [x,y]=[xx,yy] and
A5: P[xx,yy] by A2;
A6: [x,y] in [:A(),B():] by A2,A3;
x=xx by A4,XTUPLE_0:1;
hence thesis by A4,A5,A6,XTUPLE_0:1,ZFMISC_1:87;
end;
thus x in A() & y in B() & P[x,y] implies [x,y] in R
proof
assume that
A7: x in A() & y in B() and
A8: P[x,y];
[x,y] in [:A(),B():] by A7,ZFMISC_1:87;
hence thesis by A2,A8;
end;
end;
definition
let P,R;
redefine pred P = R means :: redefines = (XBOOLE_0, redefinition) → = (HIDDEN, definition)
for a,b holds [a,b] in P iff [a,b] in R;
compatibility
proof
thus P = R implies for a,b holds [a,b] in P iff [a,b] in R;
assume
A1: for a,b holds [a,b] in P iff [a,b] in R;
thus P c= R
proof
let x be object;
assume
A2: x in P;
then ex y,z st x = [y,z] by Def1;
hence x in R by A1,A2;
end;
let x be object;
assume
A3: x in R;
then ex y,z st x = [y,z] by Def1;
hence x in P by A1,A3;
end;
end;
registration
let P,X;
cluster P /\ X -> Relation-like;
coherence
proof
P /\ X c= P by XBOOLE_1:17;
hence thesis;
end;
cluster P \ X -> Relation-like;
coherence;
end;
registration
let P,R;
cluster P \/ R -> Relation-like;
coherence
proof
let x;
A1: x in R implies ex y,z st x = [y,z] by Def1;
x in P implies ex y,z st x = [y,z] by Def1;
hence x in P \/ R implies ex y,z st x = [y,z] by A1,XBOOLE_0:def 3;
end;
end;
registration
let R,S be Relation;
cluster R \+\ S -> Relation-like;
coherence;
end;
registration
let a, b be object;
cluster {[a,b]} -> Relation-like;
coherence
proof
let x;
assume x in {[a,b]};
then x = [a,b] by TARSKI:def 1;
hence thesis;
end;
end;
registration
let a, b be set;
cluster [:a,b:] -> Relation-like;
coherence
proof
let z;
assume z in [:a,b:];
then ex x,y being object st x in a & y in b & [x,y]=z by ZFMISC_1:def 2;
hence thesis;
end;
end;
registration
let a, b, c, d be object;
cluster {[a,b],[c,d]} -> Relation-like;
coherence
proof
{[a,b],[c,d]} = {[a,b]} \/ {[c,d]} by ENUMSET1:1;
hence thesis;
end;
end;
definition
let P,A;
redefine pred P c= A means :: redefines c= (TARSKI, definition)
for a,b holds [a,b] in P implies [a,b] in A;
compatibility
proof
thus P c= A implies for a,b holds [a,b] in P implies [a,b] in A;
assume
A1: for a,b holds [a,b] in P implies [a,b] in A;
let x be object;
assume
A2: x in P;
then ex y,z st x = [y,z] by Def1;
hence thesis by A1,A2;
end;
end;
:: DOMAIN OF RELATION
notation
let R be Relation;
synonym dom R for proj1 R;
end;
:: CODOMAIN OF RELATION
notation
let R be Relation;
synonym rng R for proj2 R;
end;
::$CT 6
theorem Th1:
R c= [:dom R, rng R:]
proof
let y,z;
assume [y,z] in R;
then y in dom R & z in rng R by XTUPLE_0:def 12,def 13;
hence thesis by ZFMISC_1:87;
end;
theorem
R /\ [:dom R, rng R:] = R by Th1,XBOOLE_1:28;
theorem Th3:
dom {[x,y]} = {x} & rng {[x,y]} = {y}
proof
set R = {[x,y]};
for z being object holds z in dom R iff z in {x}
proof let z be object;
thus z in dom R implies z in {x}
proof
assume z in dom R;
then consider b being object such that
A2: [z,b] in R by XTUPLE_0:def 12;
[z,b] = [x,y] by A2,TARSKI:def 1;
then z=x by XTUPLE_0:1;
hence thesis by TARSKI:def 1;
end;
assume z in {x};
then z=x by TARSKI:def 1;
then [z,y] in R by TARSKI:def 1;
hence thesis by XTUPLE_0:def 12;
end;
hence dom R = {x} by TARSKI:2;
for z being object holds z in rng R iff z in {y}
proof let z be object;
thus z in rng R implies z in {y}
proof
assume z in rng R;
then consider a being object such that
A3: [a,z] in R by XTUPLE_0:def 13;
[a,z] = [x,y] by A3,TARSKI:def 1;
then z = y by XTUPLE_0:1;
hence thesis by TARSKI:def 1;
end;
assume z in {y};
then z = y by TARSKI:def 1;
then [x,z] in R by TARSKI:def 1;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
theorem
dom {[a,b],[x,y]} = {a,x} & rng {[a,b],[x,y]} = {b,y}
proof
set R = {[a,b],[x,y]};
thus dom R = {a,x}
proof
thus dom R c= {a,x}
proof
let z be object;
assume z in dom R;
then consider c being object such that
A2: [z,c] in R by XTUPLE_0:def 12;
[z,c] = [a,b] or [z,c] = [x,y] by A2,TARSKI:def 2;
then z = a or z = x by XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
let z be object;
assume z in {a,x};
then z = a or z = x by TARSKI:def 2;
then [z,b] in R or [z,y] in R by TARSKI:def 2;
hence thesis by XTUPLE_0:def 12;
end;
thus rng R c= {b,y}
proof
let z be object;
assume z in rng R;
then consider d being object such that
A3: [d,z] in R by XTUPLE_0:def 13;
[d,z] = [a,b] or [d,z] = [x,y] by A3,TARSKI:def 2;
then z = b or z = y by XTUPLE_0:1;
hence thesis by TARSKI:def 2;
end;
let z be object;
assume z in {b,y};
then z = b or z = y by TARSKI:def 2;
then [a,z] in R or [x,z] in R by TARSKI:def 2;
hence thesis by XTUPLE_0:def 13;
end;
theorem
P c= R implies dom P c= dom R & rng P c= rng R by XTUPLE_0:8,9;
theorem
rng(P \/ R) = rng P \/ rng R by XTUPLE_0:27;
theorem
rng(P /\ R) c= rng P /\ rng R by XTUPLE_0:28;
theorem
rng P \ rng R c= rng(P \ R) by XTUPLE_0:29;
:: FIELD OF RELATION
definition
::$CD 2
let R;
func field R -> set equals
dom R \/ rng R;
coherence;
end;
theorem
[a,b] in R implies a in field R & b in field R
proof
assume
A1: [a,b] in R;
then a in dom R by XTUPLE_0:def 12;
hence a in field R by XBOOLE_0:def 3;
b in rng R by A1,XTUPLE_0:def 13;
hence thesis by XBOOLE_0:def 3;
end;
theorem
P c= R implies field P c= field R
proof
assume P c= R;
then dom P c= dom R & rng P c= rng R by XTUPLE_0:8,9;
hence thesis by XBOOLE_1:13;
end;
theorem Th11:
field {[x,y]} = {x,y}
proof
dom {[x,y]} = {x} & rng {[x,y]} = {y} by Th3;
hence thesis by ENUMSET1:1;
end;
theorem
field(P \/ R) = field P \/ field R
proof
thus field(P \/ R) = dom P \/ dom R \/ rng(P \/ R) by XTUPLE_0:23
.= dom P \/ dom R \/ (rng P \/ rng R) by XTUPLE_0:27
.= dom P \/ dom R \/ rng P \/ rng R by XBOOLE_1:4
.= field P \/ dom R \/ rng R by XBOOLE_1:4
.= field P \/ field R by XBOOLE_1:4;
end;
theorem
field(P /\ R) c= field P /\ field R
proof
let x be object;
assume x in field(P /\ R);
then
A1: x in dom(P /\ R) or x in rng(P /\ R) by XBOOLE_0:def 3;
x in dom P /\ dom R or x in rng P /\ rng R implies (x in dom P or x in
rng P) & (x in dom R or x in rng R) by XBOOLE_0:def 4;
then
A2: x in dom P /\ dom R or x in rng P /\ rng R implies x in dom P \/ rng P &
x in dom R \/ rng R by XBOOLE_0:def 3;
dom(P /\ R) c= dom P /\ dom R & rng(P /\ R) c= rng P /\ rng R
by XTUPLE_0:24,28;
hence thesis by A1,A2,XBOOLE_0:def 4;
end;
:: CONVERSE RELATION
definition
let R;
func R~ -> Relation means
:Def5:
[x,y] in it iff [y,x] in R;
existence
proof
defpred Q[object,object] means [$2,$1] in R;
consider P such that
A1: for x,y holds [x,y] in P iff x in rng R & y in dom R & Q[x,y] from
RelExistence;
take P;
let x,y;
[y,x] in R implies y in dom R & x in rng R by XTUPLE_0:def 12,def 13;
hence thesis by A1;
end;
uniqueness
proof
let P1,P2;
assume that
A2: [x,y] in P1 iff [y,x] in R and
A3: [x,y] in P2 iff [y,x] in R;
let x,y;
[x,y] in P1 iff [y,x] in R by A2;
hence [x,y] in P1 iff [x,y] in P2 by A3;
end;
involutiveness;
end;
theorem Th14:
rng R = dom(R~) & dom R = rng(R~)
proof
thus rng R c= dom(R~)
proof
let u be object;
assume u in rng R;
then consider x being object such that
A1: [x,u] in R by XTUPLE_0:def 13;
[u,x] in R~ by A1,Def5;
hence thesis by XTUPLE_0:def 12;
end;
thus dom(R~) c= rng R
proof
let u be object;
assume u in dom(R~);
then consider x being object such that
A2: [u,x] in R~ by XTUPLE_0:def 12;
[x,u] in R by A2,Def5;
hence thesis by XTUPLE_0:def 13;
end;
thus dom R c= rng(R~)
proof
let u be object;
assume u in dom R;
then consider x being object such that
A3: [u,x] in R by XTUPLE_0:def 12;
[x,u] in R~ by A3,Def5;
hence thesis by XTUPLE_0:def 13;
end;
let u be object;
assume u in rng(R~);
then consider x being object such that
A4: [x,u] in R~ by XTUPLE_0:def 13;
[u,x] in R by A4,Def5;
hence thesis by XTUPLE_0:def 12;
end;
theorem
field R = field(R~)
proof
thus field R = rng(R~) \/ rng R by Th14
.= field(R~) by Th14;
end;
theorem
(P /\ R)~ = P~ /\ R~
proof
let x,y;
[x,y] in (P /\ R)~ iff [y,x] in P /\ R by Def5;
then [x,y] in (P /\ R)~ iff [y,x] in P & [y,x] in R by XBOOLE_0:def 4;
then [x,y] in (P /\ R)~ iff [x,y] in P~ & [x,y] in R~ by Def5;
hence thesis by XBOOLE_0:def 4;
end;
theorem
(P \/ R)~ = P~ \/ R~
proof
let x,y;
[x,y] in (P \/ R)~ iff [y,x] in P \/ R by Def5;
then [x,y] in (P \/ R)~ iff [y,x] in P or [y,x] in R by XBOOLE_0:def 3;
then [x,y] in (P \/ R)~ iff [x,y] in P~ or [x,y] in R~ by Def5;
hence thesis by XBOOLE_0:def 3;
end;
theorem
(P \ R)~ = P~ \ R~
proof
let x,y;
[x,y] in (P \ R)~ iff [y,x] in P \ R by Def5;
then [x,y] in (P \ R)~ iff [y,x] in P & not [y,x] in R by XBOOLE_0:def 5;
then [x,y] in (P \ R)~ iff [x,y] in P~ & not [x,y] in R~ by Def5;
hence thesis by XBOOLE_0:def 5;
end;
:: COMPOSITION OF RELATIONS
definition
let P,R be set;
func P(#)R -> Relation means
:Def6:
[x,y] in it iff ex z st [x,z] in P & [z,y] in R;
existence
proof
defpred Z[object,object] means ex z st [$1,z] in P & [z,$2] in R;
consider Q such that
A1: for x,y holds [x,y] in Q iff x in proj1 P & y in proj2 R & Z[x,y] from
RelExistence;
take Q;
let x,y;
thus [x,y] in Q implies ex z st [x,z] in P & [z,y] in R by A1;
given z such that
A2: [x,z] in P & [z,y] in R;
x in proj1 P & y in proj2 R by A2,XTUPLE_0:def 12,def 13;
hence thesis by A1,A2;
end;
uniqueness
proof
let P1,P2;
assume that
A3: [x,y] in P1 iff ex z st [x,z] in P & [z,y] in R and
A4: [x,y] in P2 iff ex z st [x,z] in P & [z,y] in R;
let x,y;
[x,y] in P1 iff ex z st [x,z] in P & [z,y] in R by A3;
hence [x,y] in P1 iff [x,y] in P2 by A4;
end;
end;
notation
let P,R;
synonym P*R for P(#)R;
end;
theorem Th19:
dom(P*R) c= dom P
proof
let x be object;
assume x in dom(P*R);
then consider y being object such that
A1: [x,y] in P*R by XTUPLE_0:def 12;
ex z st [x,z] in P & [z,y] in R by A1,Def6;
hence thesis by XTUPLE_0:def 12;
end;
theorem Th20:
rng(P*R) c= rng R
proof
let y be object;
assume y in rng(P*R);
then consider x being object such that
A1: [x,y] in P*R by XTUPLE_0:def 13;
ex z st [x,z] in P & [z,y] in R by A1,Def6;
hence thesis by XTUPLE_0:def 13;
end;
theorem
rng R c= dom P implies dom(R*P) = dom R
proof
assume
A1: for y being object holds y in rng R implies y in dom P;
thus dom(R*P) c= dom R by Th19;
let x be object;
assume x in dom R;
then consider y being object such that
A2: [x,y] in R by XTUPLE_0:def 12;
y in rng R by A2,XTUPLE_0:def 13;
then y in dom P by A1;
then consider z being object such that
A3: [y,z] in P by XTUPLE_0:def 12;
[x,z] in R*P by A2,A3,Def6;
hence thesis by XTUPLE_0:def 12;
end;
theorem
dom P c= rng R implies rng(R*P) = rng P
proof
assume
A1: for y being object st y in dom P holds y in rng R;
thus rng(R*P) c= rng P by Th20;
let z be object;
assume z in rng P;
then consider y being object such that
A2: [y,z] in P by XTUPLE_0:def 13;
y in dom P by A2,XTUPLE_0:def 12;
then y in rng R by A1;
then consider x being object such that
A3: [x,y] in R by XTUPLE_0:def 13;
[x,z] in R*P by A2,A3,Def6;
hence thesis by XTUPLE_0:def 13;
end;
theorem Th23:
P c= R implies Q*P c= Q*R
proof
assume
A1: P c= R;
let x,y;
assume [x,y] in Q*P;
then ex z st [x,z] in Q & [z,y] in P by Def6;
hence thesis by A1,Def6;
end;
theorem Th24:
P c= Q implies P*R c= Q*R
proof
assume
A1: P c= Q;
let x,y;
assume [x,y] in P*R;
then ex z st [x,z] in P & [z,y] in R by Def6;
hence thesis by A1,Def6;
end;
theorem
P c= R & Q c= S implies P*Q c= R*S
proof
assume
A1: P c= R & Q c= S;
let x,y;
assume [x,y] in P*Q;
then ex z st [x,z] in P & [z,y] in Q by Def6;
hence [x,y] in R*S by A1,Def6;
end;
theorem
P*(R \/ Q) = (P*R) \/ (P*Q)
proof
let x,y;
hereby
assume [x,y] in P*(R \/ Q);
then consider z such that
A1: [x,z] in P and
A2: [z,y] in R \/ Q by Def6;
[z,y] in R or [z,y] in Q by A2,XBOOLE_0:def 3;
then [x,y] in P*R or [x,y] in P*Q by A1,Def6;
hence [x,y] in (P*R) \/ (P*Q) by XBOOLE_0:def 3;
end;
assume
A3: [x,y] in (P*R) \/ (P*Q);
per cases by A3,XBOOLE_0:def 3;
suppose [x,y] in P*Q;
then consider z such that
A4: [x,z] in P and
A5: [z,y] in Q by Def6;
[z,y] in R \/ Q by A5,XBOOLE_0:def 3;
hence [x,y] in P*(R \/ Q) by A4,Def6;
end;
suppose [x,y] in P*R;
then consider z such that
A6: [x,z] in P and
A7: [z,y] in R by Def6;
[z,y] in R \/ Q by A7,XBOOLE_0:def 3;
hence [x,y] in P*(R \/ Q) by A6,Def6;
end;
end;
theorem
P*(R /\ Q) c= (P*R) /\ (P*Q)
proof
let x,y;
assume [x,y] in P*(R /\ Q);
then consider z such that
A1: [x,z] in P and
A2: [z,y] in R /\ Q by Def6;
[z,y] in Q by A2,XBOOLE_0:def 4;
then
A3: [x,y] in P*Q by A1,Def6;
[z,y] in R by A2,XBOOLE_0:def 4;
then [x,y] in P*R by A1,Def6;
hence [x,y] in (P*R) /\ (P*Q) by A3,XBOOLE_0:def 4;
end;
theorem
(P*R) \ (P*Q) c= P*(R \ Q)
proof
let a,b;
assume
A1: [a,b] in (P*R) \ (P*Q);
then consider y such that
A2: [a,y] in P and
A3: [y,b] in R by Def6;
not [a,b] in P*Q by A1,XBOOLE_0:def 5;
then not [a,y] in P or not [y,b] in Q by Def6;
then [y,b] in R \ Q by A2,A3,XBOOLE_0:def 5;
hence [a,b] in P*(R \ Q) by A2,Def6;
end;
theorem
(P*R)~ = R~*P~
proof
let a,b;
hereby
assume [a,b] in (P*R)~;
then [b,a] in P*R by Def5;
then consider y such that
A1: [b,y] in P & [y,a] in R by Def6;
[y,b] in P~ & [a,y] in R~ by A1,Def5;
hence [a,b] in R~*P~ by Def6;
end;
assume [a,b] in R~*P~;
then consider y such that
A2: [a,y] in R~ & [y,b] in P~ by Def6;
[y,a] in R & [b,y] in P by A2,Def5;
then [b,a] in P*R by Def6;
hence [a,b] in (P*R)~ by Def5;
end;
theorem Th30:
(P*R)*Q = P*(R*Q)
proof
let a,b;
hereby
assume [a,b] in (P*R)*Q;
then consider y such that
A1: [a,y] in P*R and
A2: [y,b] in Q by Def6;
consider x such that
A3: [a,x] in P and
A4: [x,y] in R by A1,Def6;
[x,b] in R*Q by A2,A4,Def6;
hence [a,b] in P*(R*Q) by A3,Def6;
end;
assume [a,b] in P*(R*Q);
then consider y such that
A5: [a,y] in P and
A6: [y,b] in R*Q by Def6;
consider x such that
A7: [y,x] in R and
A8: [x,b] in Q by A6,Def6;
[a,x] in P*R by A5,A7,Def6;
hence [a,b] in (P*R)*Q by A8,Def6;
end;
:: EMPTY RELATION
registration
cluster non empty for Relation;
existence
proof
{[{},{}]} is non empty;
hence thesis;
end;
end;
registration
let f be non empty Relation;
cluster dom f -> non empty;
coherence
proof
ex x1,x2 being object st the Element of f = [x1,x2] by Def1;
hence thesis by XTUPLE_0:def 12;
end;
cluster rng f -> non empty;
coherence
proof
ex x1,x2 being object st the Element of f = [x1,x2] by Def1;
hence thesis by XTUPLE_0:def 13;
end;
end;
theorem Th31:
(for x,y holds not [x,y] in R) implies R = {};
theorem Th32:
dom {} = {} & rng {} = {};
theorem Th33:
{}*R = {} & R*{} = {}
proof
thus {}*R = {}
proof
let x,y;
hereby
assume [x,y] in {}*R;
then ex z st [x,z] in {} & [z,y] in R by Def6;
hence [x,y] in {};
end;
thus thesis;
end;
let x,y;
hereby
assume [x,y] in R*{};
then ex z st [x,z] in R & [z,y] in {} by Def6;
hence [x,y] in {};
end;
thus thesis;
end;
registration
let X be empty set;
cluster dom X -> empty;
coherence;
cluster rng X -> empty;
coherence;
let R;
cluster X*R -> empty;
coherence by Th33;
cluster R*X -> empty;
coherence by Th33;
end;
theorem
field {} = {};
theorem Th35:
dom R = {} or rng R = {} implies R = {};
theorem
dom R = {} iff rng R = {} by Th32,Th35;
registration
let X be empty set;
cluster X~ -> empty;
coherence
proof
for x,y st [x,y] in {}~ holds contradiction by Def5;
hence thesis by Th31;
end;
end;
theorem
{}~ = {};
theorem
rng R misses dom P implies R*P = {}
proof
assume
A1: rng R /\ dom P = {};
assume R*P <> {};
then consider x,z such that
A2: [x,z] in R*P;
consider y such that
A3: [x,y] in R & [y,z] in P by A2,Def6;
y in rng R & y in dom P by A3,XTUPLE_0:def 12,def 13;
hence contradiction by A1,XBOOLE_0:def 4;
end;
definition
let R be Relation;
attr R is non-empty means :Def7:
not {} in rng R;
end;
registration
cluster non-empty for Relation;
existence
proof
take {};
thus not {} in rng {};
end;
end;
registration
let R be Relation, S be non-empty Relation;
cluster R*S -> non-empty;
coherence
proof
rng(R*S) c= rng S by Th20;
hence not {} in rng(R*S) by Def7;
end;
end;
:: IDENTITY RELATION
definition
let X;
func id X -> Relation means
:Def8:
[x,y] in it iff x in X & x = y;
existence
proof
defpred Z[object,object] means $1=$2;
consider R such that
A1: for x,y holds [x,y] in R iff x in X & y in X & Z[x,y] from
RelExistence;
take R;
let x,y;
thus thesis by A1;
end;
uniqueness
proof
let P1,P2;
assume that
A2: [x,y] in P1 iff x in X & x=y and
A3: [x,y] in P2 iff x in X & x=y;
let x,y;
[x,y] in P1 iff x in X & x=y by A2;
hence [x,y] in P1 iff [x,y] in P2 by A3;
end;
end;
registration let X;
reduce dom id X to X;
reducibility
proof
thus dom id X c= X
proof
let x be object;
assume x in dom(id X);
then ex y being object st [x,y] in id X by XTUPLE_0:def 12;
hence x in X by Def8;
end;
let x be object;
assume x in X;
then [x,x] in id X by Def8;
hence x in dom(id X) by XTUPLE_0:def 12;
end;
reduce rng id X to X;
reducibility
proof
thus rng id X c= X
proof
let x be object;
assume x in rng id X;
then consider y being object such that
A1: [y,x] in id X by XTUPLE_0:def 13;
x = y by A1,Def8;
hence thesis by A1,Def8;
end;
let x be object;
[x,x] in id X iff x in X by Def8;
hence thesis by XTUPLE_0:def 13;
end;
end;
theorem
dom id X = X & rng id X = X;
registration let X;
reduce (id X)~ to id X;
reducibility
proof
let x,y;
thus [x,y] in (id X)~ implies [x,y] in id X
proof
assume [x,y] in (id X)~;
then [y,x] in id X by Def5;
hence thesis by Def8;
end;
assume
A1: [x,y] in id X;
then x = y by Def8;
hence thesis by A1,Def5;
end;
end;
theorem
(id X)~ = id X;
theorem
(for x st x in X holds [x,x] in R) implies id X c= R
proof
assume
A1: for x st x in X holds [x,x] in R;
let x,y;
assume [x,y] in id X;
then x in X & x=y by Def8;
hence thesis by A1;
end;
theorem Th42:
[x,y] in (id X)*R iff x in X & [x,y] in R
proof
thus [x,y] in (id X)*R implies x in X & [x,y] in R
proof
assume [x,y] in (id X)*R;
then ex z st [x,z] in id X & [z,y] in R by Def6;
hence thesis by Def8;
end;
assume x in X;
then [x,x] in id X by Def8;
hence thesis by Def6;
end;
theorem Th43:
[x,y] in R*id Y iff y in Y & [x,y] in R
proof
thus [x,y] in R*id Y implies y in Y & [x,y] in R
proof
assume [x,y] in R*id Y;
then consider z such that
A1: [x,z] in R and
A2: [z,y] in id Y by Def6;
z = y by A2,Def8;
hence thesis by A1,A2,Def8;
end;
y in Y implies [y,y] in id Y by Def8;
hence thesis by Def6;
end;
theorem Th44:
R*(id X) c= R & (id X)*R c= R
proof
thus [x,y] in R*id X implies [x,y] in R
proof
assume [x,y] in R*id X;
then ex z st [x,z] in R & [z,y] in id X by Def6;
hence thesis by Def8;
end;
thus [x,y] in (id X)*R implies [x,y] in R
proof
assume [x,y] in (id X)*R;
then ex z st [x,z] in id X & [z,y] in R by Def6;
hence thesis by Def8;
end;
end;
theorem Th45:
dom R c= X implies (id X)*R = R
proof
assume
A1: dom R c= X;
R c= (id X)*R
proof
let x,y;
assume
A2: [x,y] in R;
then x in dom R by XTUPLE_0:def 12;
then [x,x] in id X by A1,Def8;
hence thesis by A2,Def6;
end;
hence thesis by Th44;
end;
theorem
(id dom R)*R = R by Th45;
theorem Th47:
rng R c= Y implies R*(id Y) = R
proof
assume
A1: rng R c= Y;
R c= R*(id Y)
proof
let x,y;
assume
A2: [x,y] in R;
then y in rng R by XTUPLE_0:def 13;
then [y,y] in (id Y) by A1,Def8;
hence thesis by A2,Def6;
end;
hence thesis by Th44;
end;
theorem
R*(id rng R) = R by Th47;
theorem
id {} = {}
proof
dom(id {}) = {};
hence thesis;
end;
theorem
rng P2 c= X & P2*R = id dom P1 & R*P1 = id X implies P1 = P2
proof
(P2*R)*P1 = P2*(R*P1) & id(dom P1)*P1 = P1 by Th30,Th45;
hence thesis by Th47;
end;
definition
let R,X;
func R|X -> Relation means
:Def9:
[x,y] in it iff x in X & [x,y] in R;
existence
proof
defpred Z[object,object] means ($1 in X & [$1,$2] in R);
consider P such that
A1: for x,y holds [x,y] in P iff x in dom R & y in rng R & Z[x,y] from
RelExistence;
take P;
let x,y;
x in X & [x,y] in R implies x in dom R & y in rng R
by XTUPLE_0:def 12,def 13;
hence thesis by A1;
end;
uniqueness
proof
let P1,P2;
assume that
A2: [x,y] in P1 iff x in X & [x,y] in R and
A3: [x,y] in P2 iff x in X & [x,y] in R;
let x,y;
[x,y] in P1 iff x in X & [x,y] in R by A2;
hence [x,y] in P1 iff [x,y] in P2 by A3;
end;
end;
registration
let R be Relation, X be empty set;
cluster R|X -> empty;
coherence
proof
not [x,y] in R|{} by Def9;
hence thesis by Th31;
end;
end;
theorem Th51:
x in dom(R|X) iff x in X & x in dom R
proof
thus x in dom(R|X) implies x in X & x in dom R
proof
assume x in dom(R|X);
then consider y being object such that
A1: [x,y] in R|X by XTUPLE_0:def 12;
[x,y] in R by A1,Def9;
hence thesis by A1,Def9,XTUPLE_0:def 12;
end;
assume
A2: x in X;
assume x in dom R;
then consider y being object such that
A3: [x,y] in R by XTUPLE_0:def 12;
[x,y] in R|X by A2,A3,Def9;
hence thesis by XTUPLE_0:def 12;
end;
theorem
dom(R|X) c= X by Th51;
theorem Th53:
R|X c= R by Def9;
theorem
dom(R|X) c= dom R by Th51;
theorem Th55:
dom(R|X) = dom R /\ X
proof
for x being object holds x in dom(R|X) iff x in dom R /\ X
proof let x be object;
x in dom(R|X) iff x in dom R & x in X by Th51;
hence thesis by XBOOLE_0:def 4;
end;
hence thesis by TARSKI:2;
end;
theorem
X c= dom R implies dom(R|X) = X
proof
dom(R|X) = dom R /\ X by Th55;
hence thesis by XBOOLE_1:28;
end;
theorem
(R|X)*P c= R*P by Th24,Th53;
theorem
P*(R|X) c= P*R by Th23,Th53;
theorem
R|X = (id X)*R
proof
let x,y;
[x,y] in R|X iff [x,y] in R & x in X by Def9;
hence thesis by Th42;
end;
theorem
R|X = {} iff dom R misses X
proof
thus R|X = {} implies dom R misses X
proof
assume
A1: R|X = {};
thus dom R /\ X = {}
proof
thus dom R /\ X c= {}
proof
let x be object;
assume
A2: x in (dom R) /\ X;
then x in dom R by XBOOLE_0:def 4;
then
A3: ex y being object st [x,y] in R by XTUPLE_0:def 12;
x in X by A2,XBOOLE_0:def 4;
hence thesis by A1,A3,Def9;
end;
thus thesis;
end;
end;
assume
A4: (dom R) /\ X = {};
let x,y;
hereby
assume
A5: [x,y] in R|X;
then x in X by Def9;
then
A6: not x in dom R by A4,XBOOLE_0:def 4;
[x,y] in R by A5,Def9;
hence [x,y] in {} by A6,XTUPLE_0:def 12;
end;
thus thesis;
end;
theorem Th61:
R|X = R /\ [:X,rng R:]
proof
set P = R /\ [:X,rng R:];
let x,y;
thus [x,y] in R|X implies [x,y] in P
proof
assume
A1: [x,y] in R|X;
then
A2: x in X by Def9;
A3: [x,y] in R by A1,Def9;
then y in rng R by XTUPLE_0:def 13;
then [x,y] in [:X,rng R:] by A2,ZFMISC_1:def 2;
hence thesis by A3,XBOOLE_0:def 4;
end;
assume
A4: [x,y] in P;
then [x,y] in [:X,rng R:] by XBOOLE_0:def 4;
then
A5: x in X by ZFMISC_1:87;
[x,y] in R by A4,XBOOLE_0:def 4;
hence thesis by A5,Def9;
end;
theorem Th62:
dom R c= X implies R|X = R
proof
assume dom R c= X; then
A1: [:dom R,rng R:] c= [:X,rng R:] by ZFMISC_1:95;
R c= [:dom R,rng R:] & R|X = R /\ [:X,rng R:] by Th1,Th61;
hence thesis by A1,XBOOLE_1:1,28;
end;
registration let R;
reduce R|dom R to R;
reducibility by Th62;
end;
theorem
R|dom R = R;
theorem Th64:
rng(R|X) c= rng R by Th53,XTUPLE_0:9;
theorem Th65:
(R|X)|Y = R|(X /\ Y)
proof
let x,y;
A1: [x,y] in R|X iff [x,y] in R & x in X by Def9;
A2: [x,y] in R|(X /\ Y) iff [x,y] in R & x in X /\ Y by Def9;
[x,y] in (R|X)|Y iff [x,y] in R|X & x in Y by Def9;
hence thesis by A1,A2,XBOOLE_0:def 4;
end;
registration let R,X;
reduce R|X|X to R|X;
reducibility
proof
X /\ X = X;
hence thesis by Th65;
end;
end;
theorem
(R|X)|X = R|X;
theorem
X c= Y implies (R|X)|Y = R|X
proof
X c= Y implies X /\ Y = X by XBOOLE_1:28;
hence thesis by Th65;
end;
theorem
Y c= X implies (R|X)|Y = R|Y
proof
Y c= X implies X /\ Y = Y by XBOOLE_1:28;
hence thesis by Th65;
end;
theorem Th69:
X c= Y implies R|X c= R|Y
proof
assume
A1: X c= Y;
let x,y;
assume [x,y] in R|X;
then x in X & [x,y] in R by Def9;
hence [x,y] in R|Y by A1,Def9;
end;
theorem Th70:
P c= R implies P|X c= R|X
proof
assume
A1: P c= R;
let x,y;
assume [x,y] in P|X;
then [x,y] in P & x in X by Def9;
hence thesis by A1,Def9;
end;
theorem Th71:
P c= R & X c= Y implies P|X c= R|Y
proof
assume P c= R & X c= Y;
then P|X c= R|X & R|X c= R|Y by Th69,Th70;
hence thesis;
end;
theorem Th72:
R|(X \/ Y) = (R|X) \/ (R|Y)
proof
let x,y;
hereby
assume
A1: [x,y] in R|(X \/ Y);
then x in X \/ Y by Def9; then
A2: x in X or x in Y by XBOOLE_0:def 3;
[x,y] in R by A1,Def9;
then [x,y] in R|X or [x,y] in R|Y by A2,Def9;
hence [x,y] in (R|X) \/ (R|Y) by XBOOLE_0:def 3;
end;
assume
A3: [x,y] in (R|X) \/ (R|Y);
per cases by A3,XBOOLE_0:def 3;
suppose
A4: [x,y] in R|Y;
then x in Y by Def9;
then
A5: x in X \/ Y by XBOOLE_0:def 3;
[x,y] in R by A4,Def9;
hence [x,y] in R|(X \/ Y) by A5,Def9;
end;
suppose
A6: [x,y] in R|X;
then x in X by Def9;
then
A7: x in X \/ Y by XBOOLE_0:def 3;
[x,y] in R by A6,Def9;
hence [x,y] in R|(X \/ Y) by A7,Def9;
end;
end;
theorem
R|(X /\ Y) = (R|X) /\ (R|Y)
proof
let x,y;
hereby
assume
A1: [x,y] in R|(X /\ Y); then
A2: x in X /\ Y by Def9;
A3: [x,y] in R by A1,Def9;
x in Y by A2,XBOOLE_0:def 4; then
A4: [x,y] in R|Y by A3,Def9;
x in X by A2,XBOOLE_0:def 4;
then [x,y] in R|X by A3,Def9;
hence [x,y] in (R|X) /\ (R|Y) by A4,XBOOLE_0:def 4;
end;
assume
A5: [x,y] in (R|X) /\ (R|Y);
then [x,y] in R|Y by XBOOLE_0:def 4; then
A6: x in Y by Def9;
A7: [x,y] in R|X by A5,XBOOLE_0:def 4;
then x in X by Def9; then
A8: x in X /\ Y by A6,XBOOLE_0:def 4;
[x,y] in R by A7,Def9;
hence [x,y] in R|(X /\ Y) by A8,Def9;
end;
theorem Th74:
R|(X \ Y) = R|X \ R|Y
proof
let x,y;
hereby
assume
A1: [x,y] in R|(X \ Y); then
A2: x in X \ Y by Def9;
then not x in Y by XBOOLE_0:def 5;
then
A3: not [x,y] in R|Y by Def9;
[x,y] in R by A1,Def9;
then [x,y] in R|X by A2,Def9;
hence [x,y] in R|X \ R|Y by A3,XBOOLE_0:def 5;
end;
assume
A4: [x,y] in R|X \ R|Y; then
A5: [x,y] in R by Def9;
not [x,y] in R|Y by A4,XBOOLE_0:def 5; then
A6: not x in Y or not [x,y] in R by Def9;
x in X by A4,Def9;
then x in X \ Y by A4,A6,Def9,XBOOLE_0:def 5;
hence [x,y] in R|(X \ Y) by A5,Def9;
end;
registration
let R be empty Relation, X be set;
cluster R|X -> empty;
coherence
proof
for x,y st [x,y] in {}|X holds contradiction by Def9;
hence thesis by Th31;
end;
end;
theorem
R|{} = {};
theorem
{}|X = {};
theorem
(P*R)|X = (P|X)*R
proof
let x,y;
hereby
assume
A1: [x,y] in (P*R)|X;
then [x,y] in P*R by Def9;
then consider a such that
A2: [x,a] in P and
A3: [a,y] in R by Def6;
x in X by A1,Def9;
then [x,a] in P|X by A2,Def9;
hence [x,y] in (P|X)*R by A3,Def6;
end;
assume [x,y] in (P|X)*R;
then consider a such that
A4: [x,a] in P|X and
A5: [a,y] in R by Def6;
[x,a] in P by A4,Def9;
then
A6: [x,y] in P*R by A5,Def6;
x in X by A4,Def9;
hence [x,y] in (P*R)|X by A6,Def9;
end;
definition
let Y,R;
func Y|`R -> Relation means
:Def10:
[x,y] in it iff y in Y & [x,y] in R;
existence
proof
defpred Z[object,object] means $2 in Y & [$1,$2] in R;
consider P such that
A1: for x,y holds [x,y] in P iff x in dom R & y in rng R & Z[x,y] from
RelExistence;
take P;
let x,y;
y in Y & [x,y] in R implies x in dom R & y in rng R
by XTUPLE_0:def 12,def 13;
hence thesis by A1;
end;
uniqueness
proof
let P1,P2;
assume that
A2: [x,y] in P1 iff y in Y & [x,y] in R and
A3: [x,y] in P2 iff y in Y & [x,y] in R;
let x,y;
[x,y] in P1 iff y in Y & [x,y] in R by A2;
hence [x,y] in P1 iff [x,y] in P2 by A3;
end;
end;
registration
let R be Relation, X be empty set;
cluster X|`R -> empty;
coherence
proof
not [x,y] in X|`R by Def10;
hence thesis by Th31;
end;
end;
theorem Th78:
y in rng(Y|`R) iff y in Y & y in rng R
proof
thus y in rng(Y|`R) implies y in Y & y in rng R
proof
assume y in rng(Y|`R);
then consider x being object such that
A1: [x,y] in Y|`R by XTUPLE_0:def 13;
[x,y] in R by A1,Def10;
hence thesis by A1,Def10,XTUPLE_0:def 13;
end;
assume
A2: y in Y;
assume y in rng R;
then consider x being object such that
A3: [x,y] in R by XTUPLE_0:def 13;
[x,y] in Y|`R by A2,A3,Def10;
hence thesis by XTUPLE_0:def 13;
end;
theorem
rng(Y|`R) c= Y by Th78;
theorem Th80:
Y|`R c= R by Def10;
theorem
rng(Y|`R) c= rng R by Th80,XTUPLE_0:9;
theorem Th82:
rng(Y|`R) = rng R /\ Y
proof
rng(Y|`R) c= Y & rng(Y|`R) c= rng R by Th78;
hence rng(Y|`R) c= rng R /\ Y by XBOOLE_1:19;
let y be object;
assume
A1: y in rng R /\ Y;
then y in rng R by XBOOLE_0:def 4;
then consider x being object such that
A2: [x,y] in R by XTUPLE_0:def 13;
y in Y by A1,XBOOLE_0:def 4;
then [x,y] in Y|`R by A2,Def10;
hence thesis by XTUPLE_0:def 13;
end;
theorem
Y c= rng R implies rng(Y|`R) = Y
proof
assume Y c= rng R;
then rng R /\ Y = Y by XBOOLE_1:28;
hence thesis by Th82;
end;
theorem
(Y|`R)*P c= R*P by Th24,Th80;
theorem
P*(Y|`R) c= P*R by Th23,Th80;
theorem
Y|`R = R*(id Y)
proof
let x,y;
[x,y] in Y|`R iff y in Y & [x,y] in R by Def10;
hence thesis by Th43;
end;
theorem Th87:
Y|`R = R /\ [:dom R,Y:]
proof
set P = R /\ [:dom R,Y:];
let x,y;
thus [x,y] in Y|`R implies [x,y] in P
proof
assume
A1: [x,y] in Y|`R;
then
A2: y in Y by Def10;
A3: [x,y] in R by A1,Def10;
then x in dom R by XTUPLE_0:def 12;
then [x,y] in [:dom R,Y:] by A2,ZFMISC_1:def 2;
hence thesis by A3,XBOOLE_0:def 4;
end;
assume
A4: [x,y] in P;
then [x,y] in [:dom R,Y:] by XBOOLE_0:def 4; then
A5: y in Y by ZFMISC_1:87;
[x,y] in R by A4,XBOOLE_0:def 4;
hence thesis by A5,Def10;
end;
theorem Th88:
rng R c= Y implies Y|`R = R
proof
assume rng R c= Y; then
A1: [:dom R,rng R:] c= [:dom R,Y:] by ZFMISC_1:95;
R c= [:dom R,rng R:] & Y|`R = R /\ [:dom R,Y:] by Th1,Th87;
hence thesis by A1,XBOOLE_1:1,28;
end;
registration let R;
reduce rng R|`R to R;
reducibility by Th88;
end;
theorem
rng R|`R=R;
theorem Th90:
Y|`(X|`R) = (Y /\ X)|`R
proof
let x,y;
A1: [x,y] in X|`R iff [x,y] in R & y in X by Def10;
A2: [x,y] in (Y /\ X)|`R iff [x,y] in R & y in Y /\ X by Def10;
[x,y] in Y|`(X|`R) iff [x,y] in X|`R & y in Y by Def10;
hence thesis by A1,A2,XBOOLE_0:def 4;
end;
registration let Y,R;
reduce Y|`(Y|`R) to Y|`R;
reducibility
proof
Y /\ Y = Y;
hence thesis by Th90;
end;
end;
theorem
Y|`(Y|`R) = Y|`R;
theorem
X c= Y implies Y|`(X|`R) = X|`R
proof
X c= Y implies Y /\ X = X by XBOOLE_1:28;
hence thesis by Th90;
end;
theorem
Y c= X implies Y|`(X|`R) = Y|`R
proof
Y c= X implies Y /\ X = Y by XBOOLE_1:28;
hence thesis by Th90;
end;
theorem Th94:
X c= Y implies X|`R c= Y|`R
proof
assume
A1: X c= Y;
let x,y; [x,y] in X|`R iff [x,y] in R & y in X by Def10;
hence thesis by A1,Def10;
end;
theorem Th95:
P1 c= P2 implies Y|`P1 c= Y|`P2
proof
assume
A1: P1 c= P2;
let x,y;
assume [x,y] in Y|`P1;
then [x,y] in P1 & y in Y by Def10;
hence thesis by A1,Def10;
end;
theorem
P1 c= P2 & Y1 c= Y2 implies Y1|`P1 c= Y2|`P2
proof
assume P1 c= P2 & Y1 c= Y2;
then Y1|`P1 c= Y1|`P2 & Y1|`P2 c= Y2|`P2 by Th94,Th95;
hence thesis;
end;
theorem
(X \/ Y)|`R = (X|`R) \/ (Y|`R)
proof
let x,y;
A1: y in X \/ Y iff y in X or y in Y by XBOOLE_0:def 3;
A2: [x,y] in (X|`R) \/ (Y|`R) iff [x,y] in X|`R or [x,y] in Y|`R
by XBOOLE_0:def 3;
[x,y] in (X \/ Y)|`R iff y in X \/ Y & [x,y] in R by Def10;
hence thesis by A1,A2,Def10;
end;
theorem
(X /\ Y)|`R = X|`R /\ Y|`R
proof
let x,y;
A1: y in X /\ Y iff y in X & y in Y by XBOOLE_0:def 4;
A2: [x,y] in X|`R /\ Y|`R iff [x,y] in X|`R & [x,y] in Y|`R by XBOOLE_0:def 4;
[x,y] in (X /\ Y)|`R iff y in X /\ Y & [x,y] in R by Def10;
hence thesis by A1,A2,Def10;
end;
theorem
(X \ Y)|`R = X|`R \ Y|`R
proof
let x,y;
A1: y in X \ Y iff y in X & not y in Y by XBOOLE_0:def 5;
A2: [x,y] in X|`R \ Y|`R iff [x,y] in X|`R & not [x,y] in Y|`R
by XBOOLE_0:def 5;
[x,y] in X|`R iff y in X & [x,y] in R by Def10;
hence thesis by A1,A2,Def10;
end;
theorem
{}|`R = {};
theorem
Y|`{} = {}
by Def10;
theorem
Y|`(P*R) = P*(Y|`R)
proof
let x,y;
hereby
assume
A1: [x,y] in Y|`(P*R);
then [x,y] in P*R by Def10;
then consider a such that
A2: [x,a] in P and
A3: [a,y] in R by Def6;
y in Y by A1,Def10;
then [a,y] in Y|`R by A3,Def10;
hence [x,y] in P*(Y|`R) by A2,Def6;
end;
assume [x,y] in P*(Y|`R);
then consider a such that
A4: [x,a] in P and
A5: [a,y] in Y|`R by Def6;
[a,y] in R by A5,Def10;
then
A6: [x,y] in P*R by A4,Def6;
y in Y by A5,Def10;
hence [x,y] in Y|`(P*R) by A6,Def10;
end;
theorem
(Y|`R)|X = Y|`(R|X)
proof
let x,y;
A1: [x,y] in R & x in X iff [x,y] in R|X by Def9;
[x,y] in (Y|`R) iff [x,y] in R & y in Y by Def10;
hence thesis by A1,Def9,Def10;
end;
:: IMAGE OF SET IN RELATION
definition
let R,X;
func R.:X -> set means
:Def11:
y in it iff ex x st [x,y] in R & x in X;
existence
proof
defpred Z[object] means ex x st [x,$1] in R & x in X;
consider Y such that
A1: for y being object holds y in Y iff y in rng R & Z[y] from XBOOLE_0:sch 1;
take Y;
let y;
thus y in Y implies ex x st [x,y] in R & x in X by A1;
given x such that
A2: [x,y] in R and
A3: x in X;
y in rng R by A2,XTUPLE_0:def 13;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let Y1,Y2;
assume that
A4: y in Y1 iff ex x st [x,y] in R & x in X and
A5: y in Y2 iff ex x st [x,y] in R & x in X;
now
let y be object;
y in Y1 iff ex x st [x,y] in R & x in X by A4;
hence y in Y1 iff y in Y2 by A5;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th104:
y in R.:X iff ex x st x in dom R & [x,y] in R & x in X
proof
thus y in R.:X implies ex x st x in dom R & [x,y] in R & x in X
proof
assume y in R.:X;
then consider x such that
A1: [x,y] in R & x in X by Def11;
take x;
thus thesis by A1,XTUPLE_0:def 12;
end;
thus thesis by Def11;
end;
theorem Th105:
R.:X c= rng R
proof
let y be object;
assume y in R.:X;
then ex x st [x,y] in R & x in X by Def11;
hence thesis by XTUPLE_0:def 13;
end;
theorem
R.:X = R.:(dom R /\ X)
proof
for y being object holds y in R.:X iff y in R.:(dom R /\ X)
proof let y be object;
thus y in R.:(X) implies y in R.:(dom R /\ X)
proof
assume y in R.:(X);
then consider x such that
A1: x in dom R and
A2: [x,y] in R and
A3: x in X by Th104;
x in dom R /\ X by A1,A3,XBOOLE_0:def 4;
hence thesis by A2,Def11;
end;
assume y in R.:(dom R /\ X);
then consider x such that
x in dom R and
A4: [x,y] in R and
A5: x in dom R /\ X by Th104;
x in X by A5,XBOOLE_0:def 4;
hence thesis by A4,Def11;
end;
hence thesis by TARSKI:2;
end;
theorem Th107:
R.:dom R = rng R
proof
thus R.:dom R c= rng R by Th105;
let y be object;
assume y in rng R;
then consider x being object such that
A1: [x,y] in R by XTUPLE_0:def 13;
x in dom R by A1,XTUPLE_0:def 12;
hence thesis by A1,Def11;
end;
theorem
R.:X c= R.:(dom R)
proof
R.:X c= rng R by Th105;
hence thesis by Th107;
end;
theorem
rng(R|X) = R.:X
proof
for y being object holds y in rng(R|X) iff y in R.:X
proof let y be object;
thus y in rng(R|X) implies y in R.:X
proof
assume y in rng(R|X);
then consider x being object such that
A1: [x,y] in R|X by XTUPLE_0:def 13;
x in X & [x,y] in R by A1,Def9;
hence thesis by Def11;
end;
assume y in R.:X;
then consider x such that
A2: [x,y] in R & x in X by Def11;
[x,y] in R|X by A2,Def9;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
registration let R; let X be empty set;
cluster R.:X -> empty;
coherence
proof
set y = the Element of R.:{};
y in R.:{} implies ex x st [x,y] in R & x in {} by Def11;
hence thesis;
end;
end;
registration let R be empty Relation; let X;
cluster R.:X -> empty;
coherence
proof
assume not thesis;
then ex x st [x,the Element of {}.:X] in {} & x in X by Def11;
hence contradiction;
end;
end;
::$CT 2
theorem
R.:X = {} iff dom R misses X
proof
set y = the Element of R.:X;
thus R.:X = {} implies dom R misses X
proof
assume
A1: R.:X = {};
assume not thesis;
then consider x be object such that
A2: x in dom R and
A3: x in X by XBOOLE_0:3;
ex y being object st [x,y] in R by A2,XTUPLE_0:def 12;
hence contradiction by A1,A2,A3,Th104;
end;
assume
A4: dom R /\ X ={};
assume not thesis;
then ex x st x in dom R & [x,y] in R & x in X by Th104;
hence contradiction by A4,XBOOLE_0:def 4;
end;
theorem
X <> {} & X c= dom R implies R.:X <> {}
proof
assume that
A1: X <> {} and
A2: X c= dom R;
set x = the Element of X;
A3: x in dom R by A1,A2;
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
hence thesis by A1,A3,Th104;
end;
theorem
R.:(X \/ Y) = R.:X \/ R.:Y
proof
thus R.:(X \/ Y) c= R.:X \/ R.:Y
proof
let y be object;
assume y in R.:(X \/ Y);
then consider x such that
A1: [x,y] in R and
A2: x in X \/ Y by Def11;
x in X or x in Y by A2,XBOOLE_0:def 3;
then y in R.:X or y in R.:Y by A1,Def11;
hence y in R.:X \/ R.:Y by XBOOLE_0:def 3;
end;
let y be object;
assume
A3: y in R.:X \/ R.:Y;
per cases by A3,XBOOLE_0:def 3;
suppose y in R.:Y;
then consider x such that
A4: [x,y] in R and
A5: x in Y by Def11;
x in X \/ Y by A5,XBOOLE_0:def 3;
hence y in R.:(X \/ Y) by A4,Def11;
end;
suppose y in R.:X;
then consider x such that
A6: [x,y] in R and
A7: x in X by Def11;
x in X \/ Y by A7,XBOOLE_0:def 3;
hence y in R.:(X \/ Y) by A6,Def11;
end;
end;
theorem
R.:(X /\ Y) c= R.:X /\ R.:Y
proof
let y be object;
assume y in R.:(X /\ Y);
then consider x such that
A1: [x,y] in R and
A2: x in X /\ Y by Def11;
x in Y by A2,XBOOLE_0:def 4;
then
A3: y in R.:Y by A1,Def11;
x in X by A2,XBOOLE_0:def 4;
then y in R.:X by A1,Def11;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
R.:X \ R.:Y c= R.:(X \ Y)
proof
let y be object;
assume
A1: y in R.:X \ R.:Y;
then consider x such that
A2: [x,y] in R and
A3: x in X by Def11;
not y in R.:Y by A1,XBOOLE_0:def 5;
then not x in Y or not [x,y] in R by Def11;
then x in X \ Y by A2,A3,XBOOLE_0:def 5;
hence thesis by A2,Def11;
end;
theorem Th115:
X c= Y implies R.:X c= R.:Y
proof
assume
A1: X c= Y;
let y be object;
assume y in R.:X;
then ex x st [x,y] in R & x in X by Def11;
hence thesis by A1,Def11;
end;
theorem Th116:
P c= R implies P.:X c= R.:X
proof
assume
A1: P c= R;
let y be object;
assume y in P.:X;
then ex x st [x,y] in P & x in X by Def11;
hence thesis by A1,Def11;
end;
theorem
P c= R & X c= Y implies P.:X c= R.:Y
proof
assume P c= R & X c= Y;
then P.:X c= R.:X & R.:X c= R.:Y by Th115,Th116;
hence thesis;
end;
theorem
(P*R).:X = R.:(P.:X)
proof
for y being object holds y in (P*R).:X iff y in R.:(P.:X)
proof let y be object;
thus y in (P*R).:X implies y in R.:(P.:X)
proof
assume y in (P*R).:X;
then consider x such that
A1: [x,y] in P*R and
A2: x in X by Def11;
consider z such that
A3: [x,z] in P and
A4: [z,y] in R by A1,Def6;
z in P.:X by A2,A3,Def11;
hence thesis by A4,Def11;
end;
assume y in R.:(P.:X);
then consider x such that
A5: [x,y] in R and
A6: x in P.:X by Def11;
consider z such that
A7: [z,x] in P and
A8: z in X by A6,Def11;
[z,y] in P*R by A5,A7,Def6;
hence thesis by A8,Def11;
end;
hence thesis by TARSKI:2;
end;
theorem Th119:
rng(P*R) = R.:(rng P)
proof
for z being object holds z in rng(P*R) iff z in R.:(rng P)
proof let z be object;
thus z in rng(P*R) implies z in R.:(rng P)
proof
assume z in rng(P*R);
then consider x being object such that
A1: [x,z] in P*R by XTUPLE_0:def 13;
consider y such that
A2: [x,y] in P and
A3: [y,z] in R by A1,Def6;
y in rng P by A2,XTUPLE_0:def 13;
hence thesis by A3,Def11;
end;
assume z in R.:(rng P);
then consider y such that
A4: [y,z] in R and
A5: y in rng P by Def11;
consider x being object such that
A6: [x,y] in P by A5,XTUPLE_0:def 13;
[x,z] in P*R by A4,A6,Def6;
hence thesis by XTUPLE_0:def 13;
end;
hence thesis by TARSKI:2;
end;
theorem
(R|X).:Y c= R.:Y by Th53,Th116;
theorem Th121:
for R be Relation, X, Y be set st X c= Y holds (R|Y).:X = R.:X
proof
let R be Relation, X, Y be set such that
A1: X c= Y;
thus (R|Y).:X c= R.:X by Th53,Th116;
let y be object;
assume y in R.:X;
then consider x1 be object such that
A2: [x1,y] in R and
A3: x1 in X by Def11;
ex x be object st [x,y] in R|Y & x in X
proof
take x1;
thus [x1,y] in R|Y by A1,A2,A3,Def9;
thus thesis by A3;
end;
hence thesis by Def11;
end;
theorem
(dom R) /\ X c= (R~).:(R.:X)
proof
let x be object;
assume
A1: x in (dom R) /\ X;
then x in dom R by XBOOLE_0:def 4;
then consider y being object such that
A2: [x,y] in R by XTUPLE_0:def 12;
A3: [y,x] in R~ by A2,Def5;
x in X by A1,XBOOLE_0:def 4;
then y in R.:X by A2,Def11;
hence thesis by A3,Def11;
end;
:: INVERSE IMAGE OF SET IN RELATION
definition
let R,Y;
func R"Y -> set means
:Def12:
x in it iff ex y st [x,y] in R & y in Y;
existence
proof
defpred Z[object] means ex y st [$1,y] in R & y in Y;
consider X such that
A1: for x being object holds x in X iff x in dom R & Z[x] from XBOOLE_0:sch 1;
take X;
let x;
thus x in X implies ex y st [x,y] in R & y in Y by A1;
given y such that
A2: [x,y] in R and
A3: y in Y;
x in dom R by A2,XTUPLE_0:def 12;
hence thesis by A1,A2,A3;
end;
uniqueness
proof
let X1,X2;
assume that
A4: x in X1 iff ex y st [x,y] in R & y in Y and
A5: x in X2 iff ex y st [x,y] in R & y in Y;
now
let x be object;
x in X1 iff ex y st [x,y] in R & y in Y by A4;
hence x in X1 iff x in X2 by A5;
end;
hence thesis by TARSKI:2;
end;
end;
theorem Th123:
x in R"Y iff ex y st y in rng R & [x,y] in R & y in Y
proof
thus x in R"Y implies ex y st y in rng R & [x,y] in R & y in Y
proof
assume x in R"Y;
then consider y such that
A1: [x,y] in R & y in Y by Def12;
take y;
thus thesis by A1,XTUPLE_0:def 13;
end;
thus thesis by Def12;
end;
theorem Th124:
R"Y c= dom R
proof
let x be object;
assume x in R"Y;
then ex y st [x,y] in R & y in Y by Def12;
hence thesis by XTUPLE_0:def 12;
end;
theorem
R"Y = R"(rng R /\ Y)
proof
for x being object holds x in R"Y iff x in R"(rng R /\ Y)
proof let x be object;
thus x in R"Y implies x in R"(rng R /\ Y)
proof
assume x in R"Y;
then consider y such that
A1: y in rng R and
A2: [x,y] in R and
A3: y in Y by Th123;
y in rng R /\ Y by A1,A3,XBOOLE_0:def 4;
hence thesis by A2,Def12;
end;
assume x in R"(rng R /\ Y);
then consider y such that
y in rng R and
A4: [x,y] in R and
A5: y in rng R /\ Y by Th123;
y in Y by A5,XBOOLE_0:def 4;
hence thesis by A4,Def12;
end;
hence thesis by TARSKI:2;
end;
theorem Th126:
R"rng R = dom R
proof
thus R"rng R c= dom R by Th124;
let x be object;
assume x in dom R;
then consider y being object such that
A1: [x,y] in R by XTUPLE_0:def 12;
y in rng R by A1,XTUPLE_0:def 13;
hence thesis by A1,Def12;
end;
theorem
R"Y c= R"rng R
proof
R"Y c= dom R by Th124;
hence thesis by Th126;
end;
registration let R; let Y be empty set;
cluster R"Y -> empty;
coherence
proof
set x = the Element of R"{};
x in R"{} implies ex y st [x,y] in R & y in {} by Def12;
hence thesis;
end;
end;
registration let R be empty Relation; let Y;
cluster R"Y -> empty;
coherence
proof
assume not thesis;
then ex y st [the Element of {}"Y,y] in {} & y in Y by Def12;
hence contradiction;
end;
end;
::$CT 2
theorem
R"Y = {} iff rng R misses Y
proof
set x = the Element of R"Y;
thus R"Y = {} implies rng R misses Y
proof
assume
A1: R"Y = {};
assume not thesis;
then consider y being object such that
A2: y in rng R and
A3: y in Y by XBOOLE_0:3;
ex x being object st [x,y] in R by A2,XTUPLE_0:def 13;
hence contradiction by A1,A2,A3,Th123;
end;
assume
A4: rng R /\ Y = {};
assume not thesis;
then ex y st y in rng R & [x,y] in R & y in Y by Th123;
hence contradiction by A4,XBOOLE_0:def 4;
end;
theorem
Y <> {} & Y c= rng R implies R"Y <> {}
proof
assume that
A1: Y <> {} and
A2: Y c= rng R;
set y = the Element of Y;
A3: y in rng R by A1,A2;
then ex x being object st [x,y] in R by XTUPLE_0:def 13;
hence thesis by A1,A3,Th123;
end;
theorem
R"(X \/ Y) = R"X \/ R"Y
proof
thus R"(X \/ Y) c= R"X \/ R"Y
proof
let x be object;
assume x in R"(X \/ Y);
then consider y such that
A1: [x,y] in R and
A2: y in X \/ Y by Def12;
y in X or y in Y by A2,XBOOLE_0:def 3;
then x in R"X or x in R"Y by A1,Def12;
hence x in R"X \/ R"Y by XBOOLE_0:def 3;
end;
let x be object;
assume
A3: x in R"X \/ R"Y;
per cases by A3,XBOOLE_0:def 3;
suppose x in R"Y;
then consider y such that
A4: [x,y] in R and
A5: y in Y by Def12;
y in X \/ Y by A5,XBOOLE_0:def 3;
hence x in R"(X \/ Y) by A4,Def12;
end;
suppose x in R"X;
then consider y such that
A6: [x,y] in R and
A7: y in X by Def12;
y in X \/ Y by A7,XBOOLE_0:def 3;
hence x in R"(X \/ Y) by A6,Def12;
end;
end;
theorem
R"(X /\ Y) c= R"X /\ R"Y
proof
let x be object;
assume x in R"(X /\ Y);
then consider y such that
A1: [x,y] in R and
A2: y in X /\ Y by Def12;
y in Y by A2,XBOOLE_0:def 4;
then
A3: x in R"Y by A1,Def12;
y in X by A2,XBOOLE_0:def 4;
then x in R"X by A1,Def12;
hence thesis by A3,XBOOLE_0:def 4;
end;
theorem
R"X \ R"Y c= R"(X \ Y)
proof
let x be object;
assume
A1: x in R"X \ R"Y;
then consider y such that
A2: [x,y] in R and
A3: y in X by Def12;
not x in R"Y by A1,XBOOLE_0:def 5;
then not y in Y or not [x,y] in R by Def12;
then y in X \ Y by A2,A3,XBOOLE_0:def 5;
hence thesis by A2,Def12;
end;
theorem Th133:
X c= Y implies R"X c= R"Y
proof
assume
A1: X c= Y;
let x be object;
assume x in R"X;
then ex y st [x,y] in R & y in X by Def12;
hence thesis by A1,Def12;
end;
theorem Th134:
P c= R implies P"Y c= R"Y
proof
assume
A1: P c= R;
let x be object;
assume x in P"Y;
then ex y st [x,y] in P & y in Y by Def12;
hence thesis by A1,Def12;
end;
theorem
P c= R & X c= Y implies P"X c= R"Y
proof
assume P c= R & X c= Y;
then P"X c= R"X & R"X c= R"Y by Th133,Th134;
hence thesis;
end;
theorem
(P*R)"Y = P"(R"Y)
proof
for x being object holds x in (P*R)"Y iff x in P"(R"Y)
proof let x be object;
thus x in (P*R)"Y implies x in P"(R"Y)
proof
assume x in (P*R)"Y;
then consider y such that
A1: [x,y] in P*R and
A2: y in Y by Def12;
consider z such that
A3: [x,z] in P and
A4: [z,y] in R by A1,Def6;
z in R"Y by A2,A4,Def12;
hence thesis by A3,Def12;
end;
assume x in P"(R"Y);
then consider y such that
A5: [x,y] in P and
A6: y in R"Y by Def12;
consider z such that
A7: [y,z] in R and
A8: z in Y by A6,Def12;
[x,z] in P*R by A5,A7,Def6;
hence thesis by A8,Def12;
end;
hence thesis by TARSKI:2;
end;
theorem Th137:
dom(P*R) = P"(dom R)
proof
for z being object holds z in dom(P*R) iff z in P"(dom R)
proof let z be object;
thus z in dom(P*R) implies z in P"(dom R)
proof
assume z in dom(P*R);
then consider x being object such that
A1: [z,x] in P*R by XTUPLE_0:def 12;
consider y such that
A2: [z,y] in P and
A3: [y,x] in R by A1,Def6;
y in dom R by A3,XTUPLE_0:def 12;
hence thesis by A2,Def12;
end;
assume z in P"(dom R);
then consider y such that
A4: [z,y] in P and
A5: y in dom R by Def12;
consider x being object such that
A6: [y,x] in R by A5,XTUPLE_0:def 12;
[z,x] in P*R by A4,A6,Def6;
hence thesis by XTUPLE_0:def 12;
end;
hence thesis by TARSKI:2;
end;
theorem
(rng R) /\ Y c= (R~)"(R"Y)
proof
let y be object;
assume
A1: y in (rng R) /\ Y;
then y in rng R by XBOOLE_0:def 4;
then consider x being object such that
A2: [x,y] in R by XTUPLE_0:def 13;
A3: [y,x] in R~ by A2,Def5;
y in Y by A1,XBOOLE_0:def 4;
then x in R"Y by A2,Def12;
hence thesis by A3,Def12;
end;
begin :: Addenda
definition
let R;
attr R is empty-yielding means
:Def13:
rng R c= {{}};
end;
theorem
R is empty-yielding iff for X st X in rng R holds X = {}
proof
thus R is empty-yielding implies
for X st X in rng R holds X = {} by TARSKI:def 1;
assume
A1: for X st X in rng R holds X = {};
let Y be object;
assume Y in rng R;
then Y = {} by A1;
hence thesis by TARSKI:def 1;
end;
:: from AMI_3
theorem
for f,g being Relation, A,B being set st f|A = g|A & f|B = g|B holds
f|(A \/ B) = g|(A \/ B)
proof
let f,g be Relation, A,B be set;
assume f|A = g|A & f|B = g|B;
hence f|(A \/ B) = g|A \/ g|B by Th72
.= g|(A \/ B) by Th72;
end;
theorem
for X being set, f,g being Relation st dom g c= X & g c= f holds g c= f|X
proof
let X be set, f,g be Relation;
assume dom g c= X & g c= f;
then g|dom g c= f|X by Th71;
hence thesis;
end;
theorem
for f being Relation, X being set st X misses dom f holds f|X = {}
proof
let f be Relation, X be set such that
A1: X /\ dom f = {};
thus f|X = (f|dom f)|X
.= f|({} qua set) by A1,Th65
.= {};
end;
:: from AMI_5
theorem
for f,g being Relation, A,B being set st A c= B & f|B = g|B holds f|A = g|A
proof
let f,g be Relation, A,B be set;
assume that
A1: A c= B and
A2: f|B = g|B;
A3: A = B /\ A by A1,XBOOLE_1:28;
hence f|A = (f|B)|A by Th65
.= g|A by A2,A3,Th65;
end;
:: missing, 2005.07.11, A.T.
theorem
R|dom S = R|dom(S|dom R)
proof
thus R|dom S = R|dom R|dom S
.= R|(dom S /\ dom R) by Th65
.= R|dom(S|dom R) by Th55;
end;
:: missing, 2005.11.13, A.T.
registration
cluster empty -> empty-yielding for Relation;
coherence
proof
let R be Relation;
assume R is empty;
hence rng R c= {{}};
end;
end;
registration
let R be empty-yielding Relation;
let X be set;
cluster R|X -> empty-yielding;
coherence
proof
rng R c= {{}} & rng(R|X) c= rng R by Def13,Th53,XTUPLE_0:9;
hence rng(R|X) c= {{}};
end;
end;
theorem
R|X is non empty-yielding implies R is non empty-yielding;
:: from EQREL_1 (Class), 2007.02.06
definition
let R be Relation, x be object;
func Im(R,x) -> set equals
R.:{x};
correctness;
end;
:: from YELLOW_3, 2007.06.13, A.T.
scheme
ExtensionalityR { A, B() -> Relation, P[object,object] }:
A() = B()
provided
A1: for a, b being object holds [a,b] in A() iff P[a,b] and
A2: for a, b being object holds [a,b] in B() iff P[a,b]
proof
let y,z be object;
thus [y,z] in A() implies [y,z] in B() by A1,A2;
assume [y,z] in B();
hence thesis by A1,A2;
end;
:: from SCMFSA6A, 2007.07.23, A.T.
theorem
dom (R | (dom R \ X)) = dom R \ X
proof
thus dom (R | (dom R \ X)) = dom R /\ (dom R \ X) by Th55
.= (dom R /\ dom R) \ X by XBOOLE_1:49
.= dom R \ X;
end;
theorem
R | X = R | (dom R /\ X)
proof
thus R | X = (R | dom R) | X
.= R | (dom R /\ X) by Th65;
end;
:: missing, 2007.11.07, A.T.
theorem
dom [:X,Y:] c= X
proof
let x be object;
assume x in dom [:X,Y:];
then ex y being object st [x,y] in [:X,Y:] by XTUPLE_0:def 12;
hence thesis by ZFMISC_1:87;
end;
theorem
rng [:X,Y:] c= Y
proof
let x be object;
assume x in rng [:X,Y:];
then ex y being object st [y,x] in [:X,Y:] by XTUPLE_0:def 13;
hence thesis by ZFMISC_1:87;
end;
:: from FUNCOP_1, 2008.02.19, A.T.
theorem
X <> {} & Y <> {} implies dom [:X,Y:] = X & rng [:X,Y:] = Y
proof
assume X <> {};
then consider a being object such that
A1: a in X by XBOOLE_0:def 1;
assume Y <> {};
then consider b being object such that
A2: b in Y by XBOOLE_0:def 1;
A3: now
let x be object;
assume x in X;
then [x,b] in [:X,Y:] by A2,ZFMISC_1:87;
hence ex y being object st [x,y] in [:X,Y:];
end;
(ex y being object st [x,y] in [:X,Y:]) implies x in X by ZFMISC_1:87;
hence dom[:X,Y:] = X by A3,XTUPLE_0:def 12;
A4: now
let y be object;
assume y in Y;
then [a,y] in [:X,Y:] by A1,ZFMISC_1:87;
hence ex x being object st [x,y] in [:X,Y:];
end;
(ex x being object st [x,y] in [:X,Y:]) implies y in Y by ZFMISC_1:87;
hence thesis by A4,XTUPLE_0:def 13;
end;
theorem
dom R = {} & dom Q = {} implies R = Q;
theorem
rng R = {} & rng Q = {} implies R = Q;
theorem
dom R = dom Q implies dom(S*R) = dom (S*Q)
proof
assume
A1: dom R = dom Q;
thus dom(S*R) = S"dom R by Th137
.= dom (S*Q) by A1,Th137;
end;
theorem
rng R = rng Q implies rng(R*S) = rng (Q*S)
proof
assume
A1: rng R = rng Q;
thus rng(R*S) = S.:rng R by Th119
.= rng (Q*S) by A1,Th119;
end;
:: from RELSET_2 (R"x, generalized), 2008.07.16, A.T.
definition
let R be Relation, x be object;
func Coim(R,x) -> set equals
R"{x};
coherence;
end;
:: from NECKLACE, 2008.07.25, A.T.
registration
let R be trivial Relation;
cluster dom R -> trivial;
coherence
proof
let x,y be object;
assume x in dom R;
then consider a being object such that
A1: [x,a] in R by XTUPLE_0:def 12;
assume y in dom R;
then consider b being object such that
A2: [y,b] in R by XTUPLE_0:def 12;
[x,a] = [y,b] by A1,A2,ZFMISC_1:def 10;
hence thesis by XTUPLE_0:1;
end;
end;
registration
let R be trivial Relation;
cluster rng R -> trivial;
coherence
proof
let x,y be object;
assume x in rng R;
then consider a being object such that
A1: [a,x] in R by XTUPLE_0:def 13;
assume y in rng R;
then consider b being object such that
A2: [b,y] in R by XTUPLE_0:def 13;
[a,x] = [b,y] by A1,A2,ZFMISC_1:def 10;
hence thesis by XTUPLE_0:1;
end;
end;
:: comp. RFUNCT_2:34, CFCONT_1:31, 2008.08.07, A.T.
theorem
rng R c= dom (S|X) implies R*(S|X) = R*S
proof
assume
A1: rng R c= dom (S|X);
let a,b;
R*(S|X) c= R*S by Th23,Th53;
hence [a,b] in R*(S|X) implies [a,b] in R*S;
assume [a,b] in R*S;
then consider c such that
A2: [a,c] in R and
A3: [c,b] in S by Def6;
c in rng R by A2,XTUPLE_0:def 13;
then c in X by A1,Th51;
then [c,b] in S|X by A3,Def9;
hence thesis by A2,Def6;
end;
:: from LATTICE2, 2008.09.14, A.T.
theorem
Q|A = R|A implies Q.:A = R.:A
proof
assume Q|A = R|A;
hence Q.:A = (R|A).:A by Th121
.= R.:A by Th121;
end;
:: new, 2009.01.21, A.T
definition
let X,R;
attr R is X-defined means
:Def16:
dom R c= X;
attr R is X-valued means
:Def17:
rng R c= X;
end;
Lm1:
{} is X-defined Y-valued
proof
thus dom{} c= X & rng{} c= Y;
end;
registration
let X,Y;
cluster X-defined Y-valued for Relation;
existence
proof
take {};
thus thesis by Lm1;
end;
end;
:: from QC_LANG4, 2009.01.23, A.T
theorem
for D being set, R being D-valued Relation
for y being object st y in rng R holds y in D
proof
let D be set, R be D-valued Relation;
rng R c= D by Def17;
hence thesis;
end;
:: new, 2009.02.07, A.T.
registration
let X,A;
let R be A-valued Relation;
cluster R|X -> A-valued;
coherence
proof
rng(R|X) c= rng R & rng R c= A by Def17,Th53,XTUPLE_0:9;
hence rng(R|X) c= A;
end;
end;
registration
let X,A;
let R be A-defined Relation;
cluster R|X -> A-defined X-defined;
coherence
proof
dom(R|X) c= dom R & dom R c= A by Def16,Th51;
hence dom(R|X) c= A;
thus dom(R|X) c= X by Th51;
end;
end;
registration
let X;
cluster id X -> X-defined X-valued;
coherence;
end;
:: 2009.02.16, A.T.
registration
let A be set;
let R be A-valued Relation, S be Relation;
cluster S*R -> A-valued;
coherence
proof
rng R c= A & rng(S*R) c= rng R by Def17,Th20;
hence rng(S*R) c= A;
end;
end;
registration
let A be set;
let R be A-defined Relation, S be Relation;
cluster R*S -> A-defined;
coherence
proof
dom R c= A & dom(R*S) c= dom R by Def16,Th19;
hence dom(R*S) c= A;
end;
end;
:: 2009.02.16, A.T.
theorem
x in X implies Im([:X,Y:],x) = Y
proof assume
A1: x in X;
thus Im([:X,Y:],x) c= Y
proof let y be object;
assume y in Im([:X,Y:],x);
then ex z st [z,y] in [:X,Y:] & z in {x} by Def11;
hence y in Y by ZFMISC_1:87;
end;
let y be object;
assume y in Y; then
A2: [x,y] in [:X,Y:] by A1,ZFMISC_1:87;
x in {x} by TARSKI:def 1;
hence y in Im([:X,Y:],x) by A2,Def11;
end;
theorem Th159:
[x,y] in R iff y in Im(R,x)
proof
thus [x,y] in R implies y in Im(R,x)
proof
x in {x} by TARSKI:def 1;
hence thesis by Def11;
end;
assume y in Im(R,x);
then ex z st [z,y] in R & z in {x} by Def11;
hence [x,y] in R by TARSKI:def 1;
end;
theorem
x in dom R iff Im(R,x) <> {}
proof
thus x in dom R implies Im(R,x) <> {}
proof
assume x in dom R;
then ex y being object st [x,y] in R by XTUPLE_0:def 12;
hence Im(R,x) <> {} by Th159;
end;
assume Im(R,x) <> {};
then consider y being object such that
A1: y in Im(R,x) by XBOOLE_0:def 1;
[x,y] in R by A1,Th159;
hence x in dom R by XTUPLE_0:def 12;
end;
theorem
{} is X-defined Y-valued by Lm1;
:: 2009.10.02, A.T.
registration
cluster empty -> non-empty for Relation;
coherence;
end;
registration let X be set, R be X-defined Relation;
cluster -> X-defined for Subset of R;
coherence
proof let S be Subset of R;
A1: dom R c= X by Def16;
dom S c= dom R by XTUPLE_0:8;
hence dom S c= X by A1;
end;
end;
registration let X be set, R be X-valued Relation;
cluster -> X-valued for Subset of R;
coherence
proof let S be Subset of R;
A1: rng R c= X by Def17;
rng S c= rng R by XTUPLE_0:9;
hence rng S c= X by A1;
end;
end;
:: missing, 2010.01.02, A.T
theorem
X misses Y implies R|X|Y = {}
proof
assume X misses Y;
hence R|X|Y = R|({} qua set) by Th65
.= {};
end;
:: from AMISTD_3, 2010.01.10, A.T.
theorem
field {[x,x]} = {x}
proof
thus field {[x,x]} = {x,x} by Th11
.= {x} by ENUMSET1:29;
end;
registration let X; let R be X-defined Relation;
reduce R|X to R;
reducibility
proof
dom R c= X by Def16;
hence R|X = R by Th62;
end;
end;
registration let Y; let R be Y-valued Relation;
reduce Y|`R to R;
reducibility
proof
rng R c= Y by Def17;
hence Y|`R = R by Th88;
end;
end;
theorem
for R being X-defined Relation holds R = R|X;
theorem
for S being Relation, R being X-defined Relation st R c= S holds R c= S|X
proof let S be Relation, R be X-defined Relation;
R = R|X;
hence thesis by Th70;
end;
:: missing, 2010.04.07, A.T.
theorem Th166:
dom R c= X implies R \ (R|A) = R|(X\A)
proof
assume dom R c= X;
hence R \ (R|A) = R|X \ R|A by Th62
.= R|(X\A) by Th74;
end;
theorem Th167:
dom(R \ (R|A)) = dom R \ A
proof
R \ (R|A) = R|(dom R \ A) by Th166;
hence dom(R \ (R|A)) = dom R /\ (dom R \ A) by Th55
.= (dom R /\ dom R) \ A by XBOOLE_1:49
.= dom R \ A;
end;
theorem
dom R \ dom(R|A) = dom(R \ (R|A))
proof
thus dom R \ dom(R|A) = dom R \ A /\ dom R by Th55
.= dom R \ A by XBOOLE_1:47
.= dom(R \ (R|A)) by Th167;
end;
theorem Th169:
dom R misses dom S implies R misses S
proof
assume
A1: dom R misses dom S;
assume R meets S;
then consider x being object such that
A2:x in R and
A3:x in S by XBOOLE_0:3;
consider y,z such that
A4:x = [y,z] by A2,Def1;
y in dom R & y in dom S by A2,A3,A4,XTUPLE_0:def 12;
hence contradiction by A1,XBOOLE_0:3;
end;
theorem
rng R misses rng S implies R misses S
proof
assume
A1:rng R misses rng S;
assume R meets S;
then consider x being object such that
A2: x in R and
A3: x in S by XBOOLE_0:3;
consider y,z such that
A4: x = [y,z] by A2,Def1;
z in rng R & z in rng S by A2,A3,A4,XTUPLE_0:def 13;
hence contradiction by A1,XBOOLE_0:3;
end;
theorem
X c= Y implies (R \ R|Y)|X = {}
proof
assume
A1: X c= Y;
dom R /\ X c= X by XBOOLE_1:17; then
A2: dom R /\ X c= Y by A1;
dom(R \ R|Y) = dom R \ Y by Th167;
then dom((R \ R|Y)|X) =(dom R \ Y) /\ X by Th55
.= dom R /\ X \ Y by XBOOLE_1:49
.= {} by A2,XBOOLE_1:37;
hence (R \ R|Y)|X = {};
end;
theorem
X c= Y implies
for R being X-defined Relation holds R is Y-defined
proof assume
A1: X c= Y;
let R be X-defined Relation;
dom R c= X by Def16;
hence dom R c= Y by A1;
end;
theorem
X c= Y implies
for R being X-valued Relation holds R is Y-valued
proof assume
A1: X c= Y;
let R be X-valued Relation;
rng R c= X by Def17;
hence rng R c= Y by A1;
end;
theorem
R c= S iff R c= S|dom R
proof
thus R c= S implies R c= S|dom R
proof
assume R c= S;
then R|dom R c= S|dom R by Th70;
hence thesis;
end;
thus thesis by Def9;
end;
theorem Th175:
for R being X-defined Y-valued Relation holds R c= [:X,Y:]
proof
let R be X-defined Y-valued Relation;
A1: R c= [:dom R,rng R:] by Th1;
dom R c= X & rng R c= Y by Def16,Def17;
then [:dom R,rng R:] c= [:X,Y:] by ZFMISC_1:96;
hence thesis by A1;
end;
:: new, 20011.06.11, A.T.
theorem
dom(X|`R) c= dom R by Th80,XTUPLE_0:8;
registration
let A,X;
let R be A-defined Relation;
cluster X|`R -> A-defined;
coherence
proof
dom(X|`R) c= dom R & dom R c= A by Def16,Th80,XTUPLE_0:8;
hence dom(X|`R) c= A;
end;
end;
registration
let X,A;
let R be A-valued Relation;
cluster X|`R -> A-valued X-valued;
coherence
proof
rng(X|`R) c= rng R & rng R c= A by Def17,Th80,XTUPLE_0:9;
hence rng(X|`R) c= A;
thus rng(X|`R) c= X by Th78;
end;
end;
registration
let X be empty set;
cluster -> empty for X-defined Relation;
coherence
proof let R be X-defined Relation;
dom R c= X by Def16;
hence thesis by XBOOLE_1:3;
end;
cluster -> empty for X-valued Relation;
coherence
proof let R be X-valued Relation;
rng R c= X by Def17;
hence thesis by XBOOLE_1:3;
end;
end;
:: from PNPROC_1, 2012.02.20, A.T.
theorem
for X,Y being set, P,R being Relation st X misses Y holds P|X misses R|Y
proof
let X,Y be set, P,R be Relation;
assume
A1: X misses Y;
A2: dom (P|X) = dom P /\ X by Th55;
dom (R|Y) = dom R /\ Y by Th55;
then dom (P|X) /\ dom (R|Y) = dom P /\ (X /\ (dom R /\ Y)) by A2,XBOOLE_1:16
.= dom P /\ (X /\ Y /\ dom R) by XBOOLE_1:16
.= {} by A1;
then dom (P|X) misses dom (R|Y);
hence thesis by Th169;
end;
theorem
for Y being set, R being Relation holds Y|`R c= R|(R"Y)
proof
let Y be set, R be Relation;
let a,b be object;
assume
A1: [a,b] in Y|`R;
then
A2: b in Y by Def10;
A3: [a,b] in R by A1,Def10;
then a in R"Y by A2,Def12;
hence thesis by A3,Def9;
end;
theorem
for f being Relation, x, y st dom f = {x} & rng f = {y}
holds f = { [x,y] }
proof
let f be Relation, x, y;
A1: f c= [:dom f,rng f:] by Th1;
assume
A2: dom f = {x} & rng f = {y};
x in dom f by A2,TARSKI:def 1;
then consider yy being object such that
A3: [x,yy] in f by XTUPLE_0:def 12;
yy in rng f by A3,XTUPLE_0:def 13;
then [x,y] in f by A3,A2,TARSKI:def 1;
hence thesis by A1,A2,ZFMISC_1:29,31;
end;
registration
let X,Y;
sethood of X-defined Y-valued Relation
proof
take bool [:X,Y:];
let R be X-defined Y-valued Relation;
R c= [:X,Y:] by Th175;
hence thesis by ZFMISC_1:def 1;
end;
end;
registration
let R be non-empty Relation, A be set;
cluster R | A -> non-empty;
coherence
proof
rng (R|A) c= rng R by Th64;
hence thesis by Def7;
end;
end;