### The Mizar article:

### Relations and Their Basic Properties

**by****Edmund Woronowicz**

- Received March 15, 1989
Copyright (c) 1989 Association of Mizar Users

- MML identifier: RELAT_1
- [ MML identifier index ]

environ vocabulary BOOLE, TARSKI, RELAT_1, ZF_REFLE, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1; constructors TARSKI, SUBSET_1, XBOOLE_0; clusters XBOOLE_0, SUBSET_1, ZFMISC_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0; theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, XBOOLE_1; schemes XBOOLE_0; begin reserve A,X,X1,X2,Y,Y1,Y2,a,b,c,d,x,y,z for set; definition let IT be set; attr IT is Relation-like means :Def1: x in IT implies ex y,z st x = [y,z]; end; definition cluster Relation-like empty set; existence proof take {}; thus x in {} implies ex y,z st x = [y,z]; thus thesis; end; end; definition mode Relation is Relation-like set; end; reserve P,P1,P2,Q,R,S for Relation; canceled 2; theorem Th3: A c= R implies A is Relation-like proof assume A1: x in A implies x in R; thus x in A implies ex y,z st x = [y,z] proof assume x in A; then x in R by A1; hence thesis by Def1; end; end; theorem Th4: {[x,y]} is Relation-like proof thus a in {[x,y]} implies ex x,y st a = [x,y] proof assume a in {[x,y]}; then a = [x,y] by TARSKI:def 1; hence thesis; end; end; theorem {[a,b],[c,d]} is Relation-like proof thus x in {[a,b],[c,d]} implies ex y,z st x = [y,z] proof assume x in {[a,b],[c,d]}; then x = [a,b] or x = [c,d] by TARSKI:def 2; hence thesis; end; end; theorem [:X,Y:] is Relation-like proof thus a in [:X,Y:] implies ex x,y st a = [x,y] by ZFMISC_1:102; end; scheme Rel_Existence{A,B() -> set, P[set,set]}: 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 set holds p in R iff p in [:A(),B():] & ex x,y st p=[x,y] & P[x,y] proof defpred Q[set] means ex x,y st $1=[x,y] & P[x,y]; consider B being set such that A1: for p being set holds p in B iff p in [:A(),B():] & Q[p] from Separation; for p being set st p in B holds ex x,y st p = [x,y] proof let p be set; assume p in B; then ex x,y st p=[x,y] & P[x,y] by A1; hence thesis; end; then reconsider B as Relation by Def1; take B; let p be set; thus p in B iff p in [:A(),B():] & ex x,y st p=[x,y] & P[x,y] by A1; end; then consider R being Relation such that A2: for p being set 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 set such that A4: [x,y]=[xx,yy] & P[xx,yy] by A2; A5: x=xx & y=yy by A4,ZFMISC_1:33; [x,y] in [:A(),B():] by A2,A3; hence thesis by A4,A5,ZFMISC_1:106; end; thus x in A() & y in B() & P[x,y] implies [x,y] in R proof assume A6: x in A() & y in B() & P[x,y]; then [x,y] in [:A(),B():] by ZFMISC_1:106; hence thesis by A2,A6; end; end; Lm1: [x,y] in R implies x in union(union R) & y in union(union R) proof assume A1: [x,y] in R; set xy=[x,y]; [x,y] = { {x,y} , {x} } by TARSKI:def 5; then {x,y} in xy & { x } in xy by TARSKI:def 2; then A2: {x,y} in union R & {x} in union R by A1,TARSKI:def 4; y in {x,y} & x in {x} by TARSKI:def 1,def 2; hence thesis by A2,TARSKI:def 4; end; definition let P,R; redefine pred P = R means :Def2: 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); thus (for a,b holds [a,b] in P iff [a,b] in R) implies P = R proof assume A1: for a,b holds [a,b] in P iff [a,b] in R; now let x; A2: now assume A3: x in P; then ex y,z st x = [y,z] by Def1; hence x in R by A1,A3; end; now assume A4: x in R; then ex y,z st x = [y,z] by Def1; hence x in P by A1,A4; end; hence x in P iff x in R by A2; end; hence thesis by TARSKI:2; end; end; end; definition let P,R; cluster P /\ R -> Relation-like; coherence proof now let x; x in P & x in R implies ex y,z st x = [y,z] by Def1; hence x in P /\ R implies ex y,z st x = [y,z] by XBOOLE_0:def 3; end; hence P /\ R is Relation-like by Def1; end; cluster P \/ R -> Relation-like; coherence proof now let x; A1: x in P implies ex y,z st x = [y,z] by Def1; x in R 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 2; end; hence P \/ R is Relation-like by Def1; end; cluster P \ R -> Relation-like; coherence proof now let x; 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 XBOOLE_0:def 4; end; hence P \ R is Relation-like by Def1; end; end; definition let P,R; redefine pred P c= R means :Def3: for a,b holds [a,b] in P implies [a,b] in R; compatibility proof thus P c= R implies (for a,b holds [a,b] in P implies [a,b] in R); thus (for a,b holds [a,b] in P implies [a,b] in R) implies P c= R proof assume A1: for a,b holds [a,b] in P implies [a,b] in R; now let x; assume A2: x in P; then ex y,z st x = [y,z] by Def1; hence x in R by A1,A2; end; hence thesis by TARSKI:def 3; end; end; end; canceled 2; theorem Th9: X /\ R is Relation proof X /\ R c= R by XBOOLE_1:17; hence thesis by Th3; end; theorem R \ X is Relation proof R \ X c= R by XBOOLE_1:36; hence thesis by Th3; end; :: DOMAIN OF RELATION :: __________________ definition let R; func dom R -> set means :Def4: x in it iff ex y st [x,y] in R; existence proof defpred Q[set] means ex y st [$1,y] in R; consider X such that A1: for x holds x in X iff x in union(union R) & Q[x] from Separation; take X; let x; (ex y st [x,y] in R) implies x in union(union R) by Lm1; hence thesis by A1; end; uniqueness proof let X1,X2; assume A2: (for x holds x in X1 iff ex y st [x,y] in R) & (for x holds x in X2 iff ex y st [x,y] in R); now let x; (x in X1 iff ex y st [x,y] in R) & (x in X2 iff ex y st [x,y] in R) by A2; hence x in X1 iff x in X2; end; hence X1=X2 by TARSKI:2; end; end; canceled 2; theorem Th13: dom(P \/ R) = dom P \/ dom R proof now let x; A1: now assume x in dom(P \/ R); then consider y such that A2: [x,y] in P \/ R by Def4; [x,y] in P or [x,y] in R by A2,XBOOLE_0:def 2; then x in dom P or x in dom R by Def4; hence x in dom P \/ dom R by XBOOLE_0:def 2; end; now assume A3: x in dom P \/ dom R; A4: now assume x in dom P; then consider y such that A5: [x,y] in P by Def4; [x,y] in P \/ R by A5,XBOOLE_0:def 2; hence x in dom(P \/ R) by Def4; end; now assume x in dom R; then consider y such that A6: [x,y] in R by Def4; [x,y] in P \/ R by A6,XBOOLE_0:def 2; hence x in dom(P \/ R) by Def4; end; hence x in dom(P \/ R) by A3,A4,XBOOLE_0:def 2; end; hence x in dom(P \/ R) iff x in dom P \/ dom R by A1; end; hence thesis by TARSKI:2; end; theorem Th14: dom(P /\ R) c= dom P /\ dom R proof let x; assume x in dom(P /\ R); then consider y such that A1: [x,y] in P /\ R by Def4; [x,y] in P & [x,y] in R by A1,XBOOLE_0:def 3; then x in dom P & x in dom R by Def4; hence x in dom P /\ dom R by XBOOLE_0:def 3; end; theorem dom P \ dom R c= dom(P \ R) proof let x; assume x in dom P \ dom R; then A1: x in dom P & not x in dom R by XBOOLE_0:def 4; then consider y such that A2: [x,y] in P by Def4; not [x,y] in R by A1,Def4; then [x,y] in P \ R by A2,XBOOLE_0:def 4; hence x in dom (P \ R) by Def4; end; :: CODOMAIN OF RELATION :: ____________________ definition let R; func rng R -> set means :Def5: y in it iff ex x st [x,y] in R; existence proof defpred Q[set] means ex x st [x,$1] in R; consider Y such that A1: for y holds y in Y iff y in union(union R) & Q[y] from Separation; take Y; let y; (ex x st [x,y] in R) implies y in union(union R) by Lm1; hence thesis by A1; end; uniqueness proof let Y1,Y2; assume A2: (for y holds y in Y1 iff ex x st [x,y] in R) & (for y holds y in Y2 iff ex x st [x,y] in R); now let y; (y in Y1 iff ex x st [x,y] in R) & (y in Y2 iff ex x st [x,y] in R) by A2; hence y in Y1 iff y in Y2; end; hence Y1=Y2 by TARSKI:2; end; end; canceled 2; theorem x in dom R implies ex y st y in rng R proof assume x in dom R; then consider y such that A1: [x,y] in R by Def4; take y; thus thesis by A1,Def5; end; theorem y in rng R implies ex x st x in dom R proof assume y in rng R; then consider x such that A1: [x,y] in R by Def5; take x; thus thesis by A1,Def4; end; theorem [x,y] in R implies x in dom R & y in rng R by Def4,Def5; theorem Th21: R c= [:dom R, rng R:] proof let x; assume A1: x in R; then consider y,z such that A2: x = [y,z] by Def1; y in dom R & z in rng R by A1,A2,Def4,Def5; hence x in [:dom R, rng R:] by A2,ZFMISC_1:106; end; theorem R /\ [:dom R, rng R:] = R proof R c= [:dom R, rng R:] by Th21; hence thesis by XBOOLE_1:28; end; theorem Th23: R = {[x,y]} implies dom R = {x} & rng R = {y} proof assume A1: R = {[x,y]}; z in dom R iff z in {x} proof thus z in dom R implies z in {x} proof assume z in dom R; then consider b such that A2: [z,b] in R by Def4; [z,b] = [x,y] by A1,A2,TARSKI:def 1; then z=x by ZFMISC_1:33; hence z in {x} by TARSKI:def 1; end; assume z in {x}; then z=x by TARSKI:def 1; then [z,y] in R by A1,TARSKI:def 1; hence thesis by Def4; end; hence dom R = {x} by TARSKI:2; z in rng R iff z in {y} proof thus z in rng R implies z in {y} proof assume z in rng R; then consider a such that A3: [a,z] in R by Def5; [a,z] = [x,y] by A1,A3,TARSKI:def 1; then z = y by ZFMISC_1:33; hence z in {y} by TARSKI:def 1; end; assume z in {y}; then z = y by TARSKI:def 1; then [x,z] in R by A1,TARSKI:def 1; hence thesis by Def5; end; hence thesis by TARSKI:2; end; theorem R = {[a,b],[x,y]} implies dom R = {a,x} & rng R = {b,y} proof assume A1: R = {[a,b],[x,y]}; z in dom R iff z in {a,x} proof thus z in dom R implies z in {a,x} proof assume z in dom R; then consider c such that A2: [z,c] in R by Def4; [z,c] = [a,b] or [z,c] = [x,y] by A1,A2,TARSKI:def 2; then z=a or z=x by ZFMISC_1:33; hence z in {a,x} by TARSKI:def 2; end; assume A3: z in {a,x}; A4: now assume z=a; then [z,b] in R by A1,TARSKI:def 2; hence z in dom R by Def4; end; now assume z=x; then [z,y] in R by A1,TARSKI:def 2; hence z in dom R by Def4; end; hence thesis by A3,A4,TARSKI:def 2; end; hence dom R = {a,x} by TARSKI:2; z in rng R iff z in {b,y} proof thus z in rng R implies z in {b,y} proof assume z in rng R; then consider d such that A5: [d,z] in R by Def5; [d,z] = [a,b] or [d,z] = [x,y] by A1,A5,TARSKI:def 2; then z=b or z=y by ZFMISC_1:33; hence z in {b,y} by TARSKI:def 2; end; assume A6: z in {b,y}; A7: now assume z=b; then [a,z] in R by A1,TARSKI:def 2; hence z in rng R by Def5; end; now assume z=y; then [x,z] in R by A1,TARSKI:def 2; hence z in rng R by Def5; end; hence thesis by A6,A7,TARSKI:def 2; end; hence thesis by TARSKI:2; end; theorem Th25: P c= R implies dom P c= dom R & rng P c= rng R proof assume A1: P c= R; thus dom P c= dom R proof let x; assume x in dom P; then consider y such that A2: [x,y] in P by Def4; thus x in dom R by A1,A2,Def4; end; thus rng P c= rng R proof let y; assume y in rng P; then consider x such that A3: [x,y] in P by Def5; thus thesis by A1,A3,Def5; end; end; theorem Th26: rng(P \/ R) = rng P \/ rng R proof now let y; A1: now assume y in rng(P \/ R); then consider x such that A2: [x,y] in P \/ R by Def5; [x,y] in P or [x,y] in R by A2,XBOOLE_0:def 2; then y in rng P or y in rng R by Def5; hence y in rng P \/ rng R by XBOOLE_0:def 2; end; now assume A3: y in rng P \/ rng R; A4: now assume y in rng P; then consider x such that A5: [x,y] in P by Def5; [x,y] in P \/ R by A5,XBOOLE_0:def 2; hence y in rng(P \/ R) by Def5; end; now assume y in rng R; then consider x such that A6: [x,y] in R by Def5; [x,y] in P \/ R by A6,XBOOLE_0:def 2; hence y in rng(P \/ R) by Def5; end; hence y in rng(P \/ R) by A3,A4,XBOOLE_0:def 2; end; hence y in rng(P \/ R) iff y in rng P \/ rng R by A1; end; hence thesis by TARSKI:2; end; theorem Th27: rng(P /\ R) c= rng P /\ rng R proof let y; assume y in rng(P /\ R); then consider x such that A1: [x,y] in P /\ R by Def5; [x,y] in P & [x,y] in R by A1,XBOOLE_0:def 3; then y in rng P & y in rng R by Def5; hence y in rng P /\ rng R by XBOOLE_0:def 3; end; theorem rng P \ rng R c= rng(P \ R) proof let y; assume y in rng P \ rng R; then A1: y in rng P & not y in rng R by XBOOLE_0:def 4; then consider x such that A2: [x,y] in P by Def5; not [x,y] in R by A1,Def5; then [x,y] in P \ R by A2,XBOOLE_0:def 4; hence y in rng (P \ R) by Def5; end; :: FIELD OF RELATION :: _________________ definition let R; func field R -> set equals :Def6: dom R \/ rng R; correctness; end; theorem dom R c= field R & rng R c= field R proof field R = dom R \/ rng R by Def6; hence thesis by XBOOLE_1:7; 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 Def4; then a in dom R \/ rng R by XBOOLE_0:def 2; hence a in field R by Def6; b in rng R by A1,Def5; then b in dom R \/ rng R by XBOOLE_0:def 2; hence b in field R by Def6; 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 Th25; then dom P \/ rng P c= dom R \/ rng R by XBOOLE_1:13; then field P c= dom R \/ rng R by Def6; hence thesis by Def6; end; theorem R = {[x,y]} implies field R = {x,y} proof assume R = {[x,y]}; then A1: dom R = {x} & rng R = {y} by Th23; {x} \/ {y} = {x,y} by ENUMSET1:41; hence thesis by A1,Def6; end; theorem field(P \/ R) = field P \/ field R proof thus field(P \/ R) = dom(P \/ R) \/ rng(P \/ R) by Def6 .= dom P \/ dom R \/ rng(P \/ R) by Th13 .= dom P \/ dom R \/ (rng P \/ rng R) by Th26 .= dom P \/ dom R \/ rng P \/ rng R by XBOOLE_1:4 .= dom P \/ rng P \/ dom R \/ rng R by XBOOLE_1:4 .= field P \/ dom R \/ rng R by Def6 .= field P \/ (dom R \/ rng R) by XBOOLE_1:4 .= field P \/ field R by Def6; end; theorem field(P /\ R) c= field P /\ field R proof let x; assume x in field(P /\ R); then x in dom(P /\ R) \/ rng(P /\ R) by Def6; then A1: x in dom(P /\ R) or x in rng(P /\ R) by XBOOLE_0:def 2; A2: dom(P /\ R) c= dom P /\ dom R by Th14; A3: rng(P /\ R) c= rng P /\ rng R by Th27; 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 3; then 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 2; then x in field P & x in field R by A1,A2,A3,Def6; hence x in field P /\ field R by XBOOLE_0:def 3; end; :: CONVERSE RELATION :: _________________ definition let R; func R~ -> Relation means :Def7: [x,y] in it iff [y,x] in R; existence proof defpred Q[set,set] 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 Rel_Existence; take P; let x,y; [y,x] in R implies y in dom R & x in rng R by Def4,Def5; 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; now 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; hence P1=P2 by Def2; end; involutiveness; end; canceled 2; theorem Th37: rng R = dom(R~) & dom R = rng(R~) proof thus rng R c= dom(R~) proof let u be set; assume u in rng R; then consider x such that A1: [x,u] in R by Def5; [u,x] in R~ by A1,Def7; hence u in dom(R~) by Def4; end; thus dom(R~) c= rng R proof let u be set; assume u in dom(R~); then consider x such that A2: [u,x] in R~ by Def4; [x,u] in R by A2,Def7; hence u in rng R by Def5; end; thus dom R c= rng(R~) proof let u be set; assume u in dom R; then consider x such that A3: [u,x] in R by Def4; [x,u] in R~ by A3,Def7; hence u in rng(R~) by Def5; end; let u be set; assume u in rng(R~); then consider x such that A4: [x,u] in R~ by Def5; [u,x] in R by A4,Def7; hence u in dom R by Def4; end; theorem field R = field(R~) proof thus field R = dom R \/ rng R by Def6 .= rng(R~) \/ rng R by Th37 .= rng(R~) \/ dom(R~) by Th37 .= field(R~) by Def6; end; theorem (P /\ R)~ = P~ /\ R~ proof [x,y] in (P /\ R)~ iff [x,y] in P~ /\ R~ proof [x,y] in (P /\ R)~ iff [y,x] in P /\ R by Def7; then [x,y] in (P /\ R)~ iff [y,x] in P & [y,x] in R by XBOOLE_0:def 3; then [x,y] in (P /\ R)~ iff [x,y] in P~ & [x,y] in R~ by Def7; hence [x,y] in (P /\ R)~ iff [x,y] in P~ /\ R~ by XBOOLE_0:def 3; end; hence thesis by Def2; end; theorem (P \/ R)~ = P~ \/ R~ proof [x,y] in (P \/ R)~ iff [x,y] in P~ \/ R~ proof [x,y] in (P \/ R)~ iff [y,x] in P \/ R by Def7; then [x,y] in (P \/ R)~ iff [y,x] in P or [y,x] in R by XBOOLE_0:def 2; then [x,y] in (P \/ R)~ iff [x,y] in P~ or [x,y] in R~ by Def7; hence [x,y] in (P \/ R)~ iff [x,y] in P~ \/ R~ by XBOOLE_0:def 2; end; hence thesis by Def2; end; theorem (P \ R)~ = P~ \ R~ proof [x,y] in (P \ R)~ iff [x,y] in P~ \ R~ proof [x,y] in (P \ R)~ iff [y,x] in P \ R by Def7; then [x,y] in (P \ R)~ iff [y,x] in P & not [y,x] in R by XBOOLE_0:def 4; then [x,y] in (P \ R)~ iff [x,y] in P~ & not [x,y] in R~ by Def7; hence [x,y] in (P \ R)~ iff [x,y] in P~ \ R~ by XBOOLE_0:def 4; end; hence thesis by Def2; end; :: COMPOSITION OF RELATIONS :: ________________________ definition let P,R; func P*R -> Relation means :Def8: [x,y] in it iff ex z st [x,z] in P & [z,y] in R; existence proof defpred Z[set,set] 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 dom P & y in rng R & Z[x,y] from Rel_Existence; 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 dom P & y in rng R by A2,Def4,Def5; hence [x,y] in Q 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; now 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; hence P1=P2 by Def2; end; end; canceled 2; theorem Th44: dom(P*R) c= dom P proof let x; assume x in dom(P*R); then consider y such that A1: [x,y] in P*R by Def4; ex z st [x,z] in P & [z,y] in R by A1,Def8; hence x in dom P by Def4; end; theorem Th45: rng(P*R) c= rng R proof let y; assume y in rng(P*R); then consider x such that A1: [x,y] in P*R by Def5; ex z st [x,z] in P & [z,y] in R by A1,Def8; hence y in rng R by Def5; end; theorem rng R c= dom P implies dom(R*P)=dom R proof assume A1: y in rng R implies y in dom P; thus dom(R*P) c= dom R by Th44; let x; assume x in dom R; then consider y such that A2: [x,y] in R by Def4; y in rng R by A2,Def5; then y in dom P by A1; then consider z such that A3: [y,z] in P by Def4; [x,z] in R*P by A2,A3,Def8; hence x in dom(R*P) by Def4; end; theorem dom P c= rng R implies rng(R*P)=rng P proof assume A1: for y st y in dom P holds y in rng R; thus rng(R*P) c= rng P by Th45; let z; assume z in rng P; then consider y such that A2: [y,z] in P by Def5; y in dom P by A2,Def4; then y in rng R by A1; then consider x such that A3: [x,y] in R by Def5; [x,z] in R*P by A2,A3,Def8; hence z in rng(R*P) by Def5; end; theorem Th48: P c= R implies Q*P c= Q*R proof assume A1: P c= R; [x,y] in Q*P implies [x,y] in Q*R proof assume [x,y] in Q*P; then consider z such that A2: [x,z] in Q & [z,y] in P by Def8; thus thesis by A1,A2,Def8; end; hence thesis by Def3; end; theorem Th49: P c= Q implies P*R c= Q*R proof assume A1: P c= Q; [x,y] in P*R implies [x,y] in Q*R proof assume [x,y] in P*R; then consider z such that A2: [x,z] in P & [z,y] in R by Def8; thus thesis by A1,A2,Def8; end; hence thesis by Def3; end; theorem P c= R & Q c= S implies P*Q c= R*S proof assume A1: P c= R & Q c= S; now let x,y; assume [x,y] in P*Q; then consider z such that A2: [x,z] in P & [z,y] in Q by Def8; thus [x,y] in R*S by A1,A2,Def8; end; hence thesis by Def3; end; theorem P*(R \/ Q) = (P*R) \/ (P*Q) proof now let x,y; A1: now assume [x,y] in P*(R \/ Q); then consider z such that A2: [x,z] in P & [z,y] in R \/ Q by Def8; [z,y] in R or [z,y] in Q by A2,XBOOLE_0:def 2; then [x,y] in P*R or [x,y] in P*Q by A2,Def8; hence [x,y] in (P*R) \/ (P*Q) by XBOOLE_0:def 2; end; now assume A3: [x,y] in (P*R) \/ (P*Q); A4: now assume [x,y] in P*R; then consider z such that A5: [x,z] in P & [z,y] in R by Def8; [z,y] in R \/ Q by A5,XBOOLE_0:def 2; hence [x,y] in P*(R \/ Q) by A5,Def8; end; now assume [x,y] in P*Q; then consider z such that A6: [x,z] in P & [z,y] in Q by Def8; [z,y] in R \/ Q by A6,XBOOLE_0:def 2; hence [x,y] in P*(R \/ Q) by A6,Def8; end; hence [x,y] in P*(R \/ Q) by A3,A4,XBOOLE_0:def 2; end; hence [x,y] in P*(R \/ Q) iff [x,y] in (P*R) \/ (P*Q) by A1; end; hence thesis by Def2; end; theorem P*(R /\ Q) c= (P*R) /\ (P*Q) proof now let x,y; now assume [x,y] in P*(R /\ Q); then consider z such that A1: [x,z] in P & [z,y] in R /\ Q by Def8; [z,y] in R & [z,y] in Q by A1,XBOOLE_0:def 3; then [x,y] in P*R & [x,y] in P*Q by A1,Def8; hence [x,y] in (P*R) /\ (P*Q) by XBOOLE_0:def 3; end; hence [x,y] in P*(R /\ Q) implies [x,y] in (P*R) /\ (P*Q); end; hence thesis by Def3; end; theorem (P*R) \ (P*Q) c= P*(R \ Q) proof now let a,b; assume [a,b] in (P*R) \ (P*Q); then A1: [a,b] in P*R & not [a,b] in P*Q by XBOOLE_0:def 4; then consider y such that A2: [a,y] in P & [y,b] in R by Def8; not [a,y] in P or not [y,b] in Q by A1,Def8; then [y,b] in R \ Q by A2,XBOOLE_0:def 4; hence [a,b] in P*(R \ Q) by A2,Def8; end; hence thesis by Def3; end; theorem (P*R)~ = R~*P~ proof now let a,b; A1: now assume [a,b] in (P*R)~; then [b,a] in P*R by Def7; then consider y such that A2: [b,y] in P & [y,a] in R by Def8; A3: [y,b] in P~ by A2,Def7; [a,y] in R~ by A2,Def7; hence [a,b] in R~*P~ by A3,Def8; end; now assume [a,b] in R~*P~; then consider y such that A4: [a,y] in R~ & [y,b] in P~ by Def8; A5: [y,a] in R by A4,Def7; [b,y] in P by A4,Def7; then [b,a] in P*R by A5,Def8; hence [a,b] in (P*R)~ by Def7; end; hence [a,b] in (P*R)~ iff [a,b] in R~*P~ by A1; end; hence thesis by Def2; end; theorem Th55: (P*R)*Q = P*(R*Q) proof now let a,b; A1: now assume [a,b] in (P*R)*Q; then consider y such that A2: [a,y] in P*R & [y,b] in Q by Def8; consider x such that A3: [a,x] in P & [x,y] in R by A2,Def8; [x,b] in R*Q by A2,A3,Def8; hence [a,b] in P*(R*Q) by A3,Def8; end; now assume [a,b] in P*(R*Q); then consider y such that A4: [a,y] in P & [y,b] in R*Q by Def8; consider x such that A5: [y,x] in R & [x,b] in Q by A4,Def8; [a,x] in P*R by A4,A5,Def8; hence [a,b] in (P*R)*Q by A5,Def8; end; hence [a,b] in (P*R)*Q iff [a,b] in P*(R*Q) by A1; end; hence thesis by Def2; end; :: EMPTY RELATION :: ______________ definition cluster empty -> Relation-like set; coherence proof let X be set; assume X is empty; hence for p being set st p in X ex x,y st [x,y] = p; end; end; definition cluster {} -> Relation-like; coherence; end; definition cluster non empty Relation; existence proof reconsider X = {[0,0]} as Relation by Th4; X is non empty; hence thesis; end; end; definition let f be non empty Relation; cluster dom f -> non empty; coherence proof consider x being Element of f; consider x1,x2 being set such that A1: x = [x1,x2] by Def1; thus thesis by A1,Def4; end; cluster rng f -> non empty; coherence proof consider x being Element of f; consider x1,x2 being set such that A2: x = [x1,x2] by Def1; thus thesis by A2,Def5; end; end; theorem Th56: (for x,y holds not [x,y] in R) implies R = {} proof assume A1: for x,y holds not [x,y] in R; consider e being Element of R; assume A2: not thesis; then ex x,y st e = [x,y] by Def1; hence contradiction by A1,A2; end; canceled 3; theorem Th60: dom {} = {} & rng {} = {} proof thus dom {} = {} proof now let x be set; now assume x in dom {}; then ex y st [x,y] in {} by Def4; hence contradiction; end; hence x in dom {} iff x in {}; end; hence dom {} = {} by TARSKI:2; end; thus rng {} = {} proof now let y be set; now assume y in rng({}); then ex x st [x,y] in {} by Def5; hence contradiction; end; hence y in rng({}) iff y in {}; end; hence rng({}) = {} by TARSKI:2; end; end; canceled; theorem Th62: {}*R = {} & R*{} = {} proof A1:now let x,y; now assume [x,y] in {}*R; then ex z st [x,z] in {} & [z,y] in R by Def8; hence thesis; end; hence [x,y] in {}*R iff [x,y] in {}; end; now let x,y; now assume [x,y] in R*{}; then ex z st [x,z] in R & [z,y] in {} by Def8; hence thesis; end; hence [x,y] in R*{} iff [x,y] in {}; end; hence thesis by A1,Def2; end; definition let X be empty set; cluster dom X -> empty; coherence by Th60; cluster rng X -> empty; coherence by Th60; let R; cluster X*R -> empty; coherence by Th62; cluster R*X -> empty; coherence by Th62; end; theorem R*{} = {}*R; theorem Th64: dom R = {} or rng R = {} implies R = {} proof assume A1: dom R = {} or rng R = {}; A2: dom R = {} implies R = {} proof assume dom R = {}; then for x,y holds not [x,y] in R by Def4; hence thesis by Th56; end; rng R = {} implies R = {} proof assume rng R = {}; then for x,y holds not [x,y] in R by Def5; hence thesis by Th56; end; hence thesis by A1,A2; end; theorem dom R = {} iff rng R = {} by Th60,Th64; theorem Th66: {}~ = {} proof for x,y st [x,y] in {}~ holds contradiction by Def7; hence thesis by Th56; end; definition let X be empty set; cluster X~ -> empty; coherence by Th66; end; theorem rng R misses dom P implies R*P = {} proof assume A1: rng R /\ dom P = {}; now assume R*P <> {}; then consider x,z such that A2: [x,z] in R*P by Th56; consider y such that A3: [x,y] in R & [y,z] in P by A2,Def8; y in rng R & y in dom P by A3,Def4,Def5; hence contradiction by A1,XBOOLE_0:def 3; end; hence thesis; end; definition let R be Relation; attr R is non-empty means not {} in rng R; end; :: IDENTITY RELATION :: _________________ definition let X; func id X -> Relation means :Def10: [x,y] in it iff x in X & x = y; existence proof defpred Z[set,set] 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 Rel_Existence; 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; now 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; hence P1=P2 by Def2; end; end; canceled 3; theorem Th71: dom id X = X & rng id X = X proof thus dom id X = X proof now let x; A1: now assume x in dom(id X); then ex y st [x,y] in id X by Def4; hence x in X by Def10; end; now assume x in X; then [x,x] in id X by Def10; hence x in dom(id X) by Def4; end; hence x in X iff x in dom(id X) by A1; end; hence thesis by TARSKI:2; end; thus rng id X = X proof x in rng id X iff x in X proof thus x in rng id X implies x in X proof assume x in rng id X; then consider y such that A2: [y,x] in id X by Def5; x=y by A2,Def10; hence thesis by A2,Def10; end; [x,x] in id X iff x in X by Def10; hence thesis by Def5; end; hence rng id X = X by TARSKI:2; end; end; theorem (id X)~ = id X proof [x,y] in (id X)~ iff [x,y] in id X proof thus [x,y] in (id X)~ implies [x,y] in id X proof assume A1: [x,y] in (id X)~; then [y,x] in id X by Def7; then x = y by Def10; hence thesis by A1,Def7; end; thus [x,y] in id X implies [x,y] in (id X)~ proof assume A2: [x,y] in id X; then x = y by Def10; hence thesis by A2,Def7; end; end; hence thesis by Def2; end; 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; thus [x,y] in id X implies [x,y] in R proof assume [x,y] in id X; then x in X & x=y by Def10; hence thesis by A1; end; end; theorem Th74: [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 Def8; hence thesis by Def10; end; assume x in X; then [x,x] in id X by Def10; hence thesis by Def8; end; theorem Th75: [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 & [z,y] in id Y by Def8; z = y & z in Y by A1,Def10; hence thesis by A1; end; y in Y implies [y,y] in id Y by Def10; hence thesis by Def8; end; theorem Th76: 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 Def8; hence [x,y] in R by Def10; 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 Def8; hence [x,y] in R by Def10; end; end; theorem Th77: dom R c= X implies (id X)*R = R proof assume A1: dom R c= X; A2: (id X)*R c= R by Th76; R c= (id X)*R proof let x,y; assume A3: [x,y] in R; then x in dom R by Def4; then [x,x] in id X by A1,Def10; hence thesis by A3,Def8; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem (id dom R)*R = R by Th77; theorem Th79: rng R c= Y implies R*(id Y) = R proof assume A1: rng R c= Y; A2: R*(id Y) c= R by Th76; R c= R*(id Y) proof let x,y; assume A3: [x,y] in R; then y in rng R by Def5; then [y,y] in (id Y) by A1,Def10; hence thesis by A3,Def8; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem R*(id rng R) = R by Th79; theorem id {} = {} proof dom(id {}) = {} by Th71; hence thesis by Th64; end; theorem dom R = X & rng P2 c= X & P2*R = id(dom P1) & R*P1 = id X implies P1 =P2 proof assume that dom R = X and A1: rng P2 c= X and A2: P2*R = id(dom P1) and A3: R*P1 = id X; (P2*R)*P1 = P2*(R*P1) & id(dom P1)*P1 = P1 & P2*id X = P2 by A1,Th55,Th77,Th79; hence thesis by A2,A3; end; definition let R,X; func R|X -> Relation means :Def11: [x,y] in it iff x in X & [x,y] in R; existence proof defpred Z[set,set] 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 Rel_Existence; take P; let x,y; x in X & [x,y] in R implies x in dom R & y in rng R by Def4,Def5; 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; now 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; hence P1=P2 by Def2; end; end; canceled 3; theorem Th86: 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 such that A1: [x,y] in R|X by Def4; [x,y] in R & x in X by A1,Def11; hence thesis by Def4; end; assume A2: x in X; assume x in dom R; then consider y such that A3: [x,y] in R by Def4; [x,y] in R|X by A2,A3,Def11; hence thesis by Def4; end; theorem dom(R|X) c= X proof let x; thus thesis by Th86; end; theorem Th88: R|X c= R proof [x,y] in R|X implies [x,y] in R by Def11; hence thesis by Def3; end; theorem dom(R|X) c= dom R proof let x; thus thesis by Th86; end; theorem Th90: dom(R|X) = dom R /\ X proof x in dom(R|X) iff x in dom R /\ X proof x in dom(R|X) iff x in dom R & x in X by Th86; hence thesis by XBOOLE_0:def 3; end; hence thesis by TARSKI:2; end; theorem X c= dom R implies dom(R|X) = X proof dom(R|X) = dom R /\ X & (X c= dom R implies dom R /\ X = X) by Th90,XBOOLE_1:28; hence thesis; end; theorem (R|X)*P c= R*P proof (R|X) c= R by Th88; hence thesis by Th49; end; theorem P*(R|X) c= P*R proof (R|X) c= R by Th88; hence thesis by Th48; end; theorem R|X = (id X)*R proof [x,y] in R|X iff [x,y] in (id X)*R proof ([x,y] in R|X iff [x,y] in R & x in X) & ([x,y] in (id X)*R iff x in X & [x,y] in R) by Def11,Th74; hence thesis; end; hence thesis by Def2; end; theorem R|X = {} iff dom R misses X proof hereby assume A1: R|X = {}; now let x be set; now assume x in (dom R) /\ X; then A2: x in dom R & x in X by XBOOLE_0:def 3; then ex y st [x,y] in R by Def4; hence contradiction by A1,A2,Def11; end; hence x in (dom R) /\ X iff x in {}; end; then dom R /\ X = {} by TARSKI:2; hence dom R misses X by XBOOLE_0:def 7; end; assume A3: (dom R) /\ X = {}; now let x,y; now assume [x,y] in R|X; then A4: x in X & [x,y] in R by Def11; then not x in dom R by A3,XBOOLE_0:def 3; hence contradiction by A4,Def4; end; hence [x,y] in R|X iff [x,y] in {}; end; hence R|X = {} by Def2; end; theorem Th96: R|X = R /\ [:X,rng R:] proof reconsider P=R /\ [:X,rng R:] as Relation by Th9; [x,y] in R|X iff [x,y] in P proof thus [x,y] in R|X implies [x,y] in P proof assume A1: [x,y] in R|X; then A2: [x,y] in R by Def11; then y in rng R & x in X by A1,Def5,Def11; then [x,y] in [:X,rng R:] by ZFMISC_1:def 2; hence thesis by A2,XBOOLE_0:def 3; end; assume A3: [x,y] in P; then [x,y] in [:X,rng R:] by XBOOLE_0:def 3; then x in X & [x,y] in R by A3,XBOOLE_0:def 3,ZFMISC_1:106; hence thesis by Def11; end; hence thesis by Def2; end; theorem Th97: dom R c= X implies R|X = R proof assume dom R c= X; then R c= [:dom R,rng R:] & [:dom R,rng R:] c= [:X,rng R:] by Th21,ZFMISC_1:118; then R c= [:X,rng R:] & R|X = R /\ [:X,rng R:] by Th96,XBOOLE_1:1; hence R|X = R by XBOOLE_1:28; end; theorem R|dom R = R by Th97; theorem rng(R|X) c= rng R proof (R|X) c= R by Th88; hence thesis by Th25; end; theorem Th100: (R|X)|Y = R|(X /\ Y) proof [x,y] in (R|X)|Y iff [x,y] in R|(X /\ Y) proof ([x,y] in (R|X)|Y iff [x,y] in R|X & x in Y) & ([x,y] in R|X iff [x,y] in R & x in X) & ([x,y] in R|(X /\ Y) iff [x,y] in R & x in X /\ Y) & (x in X /\ Y iff x in X & x in Y) by Def11,XBOOLE_0:def 3; hence thesis; end; hence thesis by Def2; end; theorem (R|X)|X = R|X proof X /\ X = X; hence thesis by Th100; end; 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 Th100; 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 Th100; end; theorem Th104: X c= Y implies R|X c= R|Y proof assume A1: X c= Y; now let x,y; assume [x,y] in R|X; then x in X & [x,y] in R by Def11; hence [x,y] in R|Y by A1,Def11; end; hence thesis by Def3; end; theorem Th105: P c= R implies P|X c= R|X proof assume A1: P c= R; [x,y] in P|X implies [x,y] in R|X proof assume [x,y] in P|X; then [x,y] in P & x in X by Def11; hence thesis by A1,Def11; end; hence thesis by Def3; 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 Th104,Th105; hence thesis by XBOOLE_1:1; end; theorem R|(X \/ Y) = (R|X) \/ (R|Y) proof now let x,y; A1: now assume [x,y] in R|(X \/ Y); then x in X \/ Y & [x,y] in R by Def11; then (x in X or x in Y) & [x,y] in R by XBOOLE_0:def 2; then [x,y] in R|X or [x,y] in R|Y by Def11; hence [x,y] in (R|X) \/ (R|Y) by XBOOLE_0:def 2; end; now assume A2: [x,y] in (R|X) \/ (R|Y); A3: now assume [x,y] in R|X; then x in X & [x,y] in R by Def11; then x in X \/ Y & [x,y] in R by XBOOLE_0:def 2; hence [x,y] in R|(X \/ Y) by Def11; end; now assume [x,y] in R|Y; then x in Y & [x,y] in R by Def11; then x in X \/ Y & [x,y] in R by XBOOLE_0:def 2; hence [x,y] in R|(X \/ Y) by Def11; end; hence [x,y] in R|(X \/ Y) by A2,A3,XBOOLE_0:def 2; end; hence [x,y] in R|(X \/ Y) iff [x,y] in (R|X) \/ (R|Y) by A1; end; hence thesis by Def2; end; theorem R|(X /\ Y) = (R|X) /\ (R|Y) proof now let x,y; A1: now assume [x,y] in R|(X /\ Y); then x in X /\ Y & [x,y] in R by Def11; then (x in X & x in Y) & [x,y] in R by XBOOLE_0:def 3; then [x,y] in R|X & [x,y] in R|Y by Def11; hence [x,y] in (R|X) /\ (R|Y) by XBOOLE_0:def 3; end; now assume [x,y] in (R|X) /\ (R|Y); then A2: [x,y] in R|X & [x,y] in R|Y by XBOOLE_0:def 3; then A3: x in X & [x,y] in R by Def11; x in Y & [x,y] in R by A2,Def11; then x in X /\ Y & [x,y] in R by A3,XBOOLE_0:def 3; hence [x,y] in R|(X /\ Y) by Def11; end; hence [x,y] in R|(X /\ Y) iff [x,y] in (R|X) /\ (R|Y) by A1; end; hence thesis by Def2; end; theorem R|(X \ Y) = R|X \ R|Y proof now let x,y; A1: now assume [x,y] in R|(X \ Y); then x in X \ Y & [x,y] in R by Def11; then A2: x in X & not x in Y & [x,y] in R by XBOOLE_0:def 4; then A3: [x,y] in R|X by Def11; not [x,y] in R|Y by A2,Def11; hence [x,y] in R|X \ R|Y by A3,XBOOLE_0:def 4; end; now assume [x,y] in R|X \ R|Y; then A4: [x,y] in R|X & not [x,y] in R|Y by XBOOLE_0:def 4; then A5: x in X & [x,y] in R by Def11; not x in Y or not [x,y] in R by A4,Def11; then x in X \ Y & [x,y] in R by A5,XBOOLE_0:def 4; hence [x,y] in R|(X \ Y) by Def11; end; hence [x,y] in R|(X \ Y) iff [x,y] in R|X \ R|Y by A1; end; hence thesis by Def2; end; theorem R|{} = {} proof not [x,y] in R|{} by Def11; hence thesis by Th56; end; theorem {}|X = {} proof for x,y st [x,y] in {}|X holds contradiction by Def11; hence thesis by Th56; end; theorem (P*R)|X = (P|X)*R proof now let x,y; A1: now assume [x,y] in (P*R)|X; then A2: x in X & [x,y] in P*R by Def11; then consider a such that A3: [x,a] in P & [a,y] in R by Def8; [x,a] in P|X by A2,A3,Def11; hence [x,y] in (P|X)*R by A3,Def8; end; now assume [x,y] in (P|X)*R; then consider a such that A4: [x,a] in P|X & [a,y] in R by Def8; A5: x in X & [x,a] in P by A4,Def11; then [x,y] in P*R by A4,Def8; hence [x,y] in (P*R)|X by A5,Def11; end; hence [x,y] in (P*R)|X iff [x,y] in (P|X)*R by A1; end; hence thesis by Def2; end; definition let Y,R; func Y|R -> Relation means :Def12: [x,y] in it iff y in Y & [x,y] in R; existence proof defpred Z[set,set] 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 Rel_Existence; take P; let x,y; y in Y & [x,y] in R implies x in dom R & y in rng R by Def4,Def5; 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; now 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; hence P1 = P2 by Def2; end; end; canceled 2; theorem Th115: 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 such that A1: [x,y] in Y|R by Def5; [x,y] in R & y in Y by A1,Def12; hence thesis by Def5; end; assume A2: y in Y; assume y in rng R; then consider x such that A3: [x,y] in R by Def5; [x,y] in Y|R by A2,A3,Def12; hence thesis by Def5; end; theorem Th116: rng(Y|R) c= Y proof let y; thus thesis by Th115; end; theorem Th117: Y|R c= R proof [x,y] in Y|R implies [x,y] in R by Def12; hence thesis by Def3; end; theorem Th118: rng(Y|R) c= rng R proof Y|R c= R by Th117; hence thesis by Th25; end; theorem Th119: rng(Y|R) = rng R /\ Y proof rng(Y|R) c= Y & rng(Y|R) c= rng R by Th116,Th118; then A1: rng(Y|R) c= rng R /\ Y by XBOOLE_1:19; rng R /\ Y c= rng(Y|R) proof let y; assume y in rng R /\ Y; then A2: y in rng R & y in Y by XBOOLE_0:def 3; then consider x such that A3: [x,y] in R by Def5; [x,y] in Y|R by A2,A3,Def12; hence thesis by Def5; end; hence thesis by A1,XBOOLE_0:def 10; 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 Th119; end; theorem (Y|R)*P c= R*P proof (Y|R) c= R by Th117; hence thesis by Th49; end; theorem P*(Y|R) c= P*R proof (Y|R) c= R by Th117; hence thesis by Th48; end; theorem Y|R = R*(id Y) proof [x,y] in Y|R iff [x,y] in R*(id Y) proof ([x,y] in Y|R iff y in Y & [x,y] in R) & ([x,y] in R*id(Y) iff y in Y & [x,y] in R) by Def12,Th75; hence thesis; end; hence thesis by Def2; end; theorem Th124: Y|R = R /\ [:dom R,Y:] proof reconsider P = R /\ [:dom R,Y:] as Relation by Th9; [x,y] in Y|R iff [x,y] in P proof thus [x,y] in Y|R implies [x,y] in P proof assume A1: [x,y] in Y|R; then A2: [x,y] in R by Def12; then x in dom R & y in Y by A1,Def4,Def12; then [x,y] in [:dom R,Y:] by ZFMISC_1:def 2; hence thesis by A2,XBOOLE_0:def 3; end; assume A3: [x,y] in P; then [x,y] in [:dom R,Y:] by XBOOLE_0:def 3; then y in Y & [x,y] in R by A3,XBOOLE_0:def 3,ZFMISC_1:106; hence thesis by Def12; end; hence thesis by Def2; end; theorem Th125: rng R c= Y implies Y|R = R proof assume rng R c= Y; then R c= [:dom R,rng R:] & [:dom R,rng R:] c= [:dom R,Y:] by Th21,ZFMISC_1:118; then R c= [:dom R,Y:] & Y|R = R /\ [:dom R,Y:] by Th124,XBOOLE_1:1; hence Y|R = R by XBOOLE_1:28; end; theorem rng R|R=R by Th125; theorem Th127: Y|(X|R) = (Y /\ X)|R proof [x,y] in Y|(X|R) iff [x,y] in (Y /\ X)|R proof ([x,y] in Y|(X|R) iff [x,y] in X|R & y in Y) & ([x,y] in X|R iff [x,y] in R & y in X) & ([x,y] in (Y /\ X)|R iff [x,y] in R & y in Y /\ X) & (y in Y /\ X iff y in X & y in Y) by Def12,XBOOLE_0:def 3; hence thesis; end; hence thesis by Def2; end; theorem Y|(Y|R) = Y|R proof Y /\ Y = Y; hence thesis by Th127; end; 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 Th127; 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 Th127; end; theorem Th131: X c= Y implies X|R c= Y|R proof assume A1: X c= Y; [x,y] in X|R implies [x,y] in Y|R proof ([x,y] in X|R iff [x,y] in R & y in X) & ([x,y] in Y|R iff [x,y] in R & y in Y) by Def12; hence thesis by A1; end; hence thesis by Def3; end; theorem Th132: P1 c= P2 implies Y|P1 c= Y|P2 proof assume A1: P1 c= P2; [x,y] in Y|P1 implies [x,y] in Y|P2 proof assume [x,y] in Y|P1; then [x,y] in P1 & y in Y by Def12; hence thesis by A1,Def12; end; hence thesis by Def3; 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 Th131,Th132; hence thesis by XBOOLE_1:1; end; theorem (X \/ Y)|R = (X|R) \/ (Y|R) proof [x,y] in (X \/ Y)|R iff [x,y] in (X|R) \/ (Y|R) proof ([x,y] in (X \/ Y)|R iff y in X \/ Y & [x,y] in R) & (y in X \/ Y iff y in X or y in Y) & ([x,y] in (X|R) \/ (Y|R) iff [x,y] in X|R or [x,y] in Y|R) & ([x,y] in X|R iff y in X & [x,y] in R) & ([x,y] in Y|R iff y in Y & [x,y] in R) by Def12,XBOOLE_0:def 2; hence thesis; end; hence thesis by Def2; end; theorem (X /\ Y)|R = X|R /\ Y|R proof [x,y] in (X /\ Y)|R iff [x,y] in X|R /\ Y|R proof ([x,y] in (X /\ Y)|R iff y in X /\ Y & [x,y] in R) & (y in X /\ Y iff y in X & y in Y) & ([x,y] in X|R /\ Y|R iff [x,y] in X|R & [x,y] in Y|R) & ([x,y] in X|R iff y in X & [x,y] in R) & ([x,y] in Y|R iff y in Y & [x,y] in R) by Def12,XBOOLE_0:def 3; hence thesis; end; hence thesis by Def2; end; theorem (X \ Y)|R = X|R \ Y|R proof [x,y] in (X \ Y)|R iff [x,y] in X|R \ Y|R proof ([x,y] in (X \ Y)|R iff y in X \ Y & [x,y] in R) & (y in X \ Y iff y in X & not y in Y) & ([x,y] in X|R \ Y|R iff [x,y] in X|R & not [x,y] in Y|R) & ([x,y] in X|R iff y in X & [x,y] in R) & ([x,y] in Y|R iff y in Y & [x,y] in R) by Def12,XBOOLE_0:def 4; hence thesis; end; hence thesis by Def2; end; theorem {}|R = {} proof not [x,y] in {}|R by Def12; hence thesis by Th56; end; theorem Y|{} = {} proof for x,y st [x,y] in Y|{} holds contradiction by Def12; hence thesis by Th56; end; theorem Y|(P*R) = P*(Y|R) proof now let x,y; A1: now assume [x,y] in Y|(P*R); then A2: y in Y & [x,y] in P*R by Def12; then consider a such that A3: [x,a] in P & [a,y] in R by Def8; [a,y] in Y|R by A2,A3,Def12; hence [x,y] in P*(Y|R) by A3,Def8; end; now assume [x,y] in P*(Y|R); then consider a such that A4: [x,a] in P & [a,y] in Y|R by Def8; A5: y in Y & [a,y] in R by A4,Def12; then [x,y] in P*R by A4,Def8; hence [x,y] in Y|(P*R) by A5,Def12; end; hence [x,y] in Y|(P*R) iff [x,y] in P*(Y|R) by A1; end; hence thesis by Def2; end; theorem (Y|R)|X = Y|(R|X) proof [x,y] in (Y|R)|X iff [x,y] in Y|(R|X) proof ([x,y] in (Y|R) iff [x,y] in R & y in Y) & ([x,y] in R & x in X iff [x,y] in R|X) & ([x,y] in (Y|R)|X iff x in X & [x,y] in (Y|R)) & ([x,y] in Y|(R|X) iff y in Y & [x,y] in R|X) by Def11,Def12; hence thesis; end; hence thesis by Def2; end; :: IMAGE OF SET IN RELATION :: ________________________ definition let R,X; func R.:X -> set means :Def13: y in it iff ex x st [x,y] in R & x in X; existence proof defpred Z[set] means ex x st [x,$1] in R & x in X; consider Y such that A1: for y holds y in Y iff y in rng R & Z[y] from Separation; 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 & x in X; y in rng R by A2,Def5; hence y in Y by A1,A2; end; uniqueness proof let Y1,Y2; assume that A3: y in Y1 iff ex x st [x,y] in R & x in X and A4: y in Y2 iff ex x st [x,y] in R & x in X; now let y; y in Y1 iff ex x st [x,y] in R & x in X by A3; hence y in Y1 iff y in Y2 by A4; end; hence Y1=Y2 by TARSKI:2; end; end; canceled 2; theorem Th143: 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 Def13; take x; thus thesis by A1,Def4; end; given x such that A2: x in dom R & [x,y] in R & x in X; thus y in R.:X by A2,Def13; end; theorem Th144: R.:X c= rng R proof let y; assume y in R.:X; then ex x st [x,y] in R & x in X by Def13; hence thesis by Def5; end; theorem R.:X = R.:(dom R /\ X) proof y in R.:X iff y in R.:(dom R /\ X) proof 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 & x in X by Th143; x in dom R /\ X by A1,A2,XBOOLE_0:def 3; hence thesis by A2,Def13; end; assume y in R.:(dom R /\ X); then consider x such that x in dom R and A3: [x,y] in R & x in dom R /\ X by Th143; x in X by A3,XBOOLE_0:def 3; hence thesis by A3,Def13; end; hence thesis by TARSKI:2; end; theorem Th146: R.:dom R = rng R proof A1: R.:dom R c= rng R by Th144; rng R c= R.:dom R proof let y; assume y in rng R; then consider x such that A2: [x,y] in R by Def5; x in dom R by A2,Def4; hence thesis by A2,Def13; end; hence thesis by A1,XBOOLE_0:def 10; end; theorem R.:X c= R.:(dom R) proof R.:X c= rng R & R.:dom R = rng R by Th144,Th146; hence thesis; end; theorem rng(R|X) = R.:X proof y in rng(R|X) iff y in R.:X proof thus y in rng(R|X) implies y in R.:X proof assume y in rng(R|X); then consider x such that A1: [x,y] in R|X by Def5; x in X & [x,y] in R by A1,Def11; hence thesis by Def13; end; assume y in R.:X; then consider x such that A2: [x,y] in R & x in X by Def13; [x,y] in R|X by A2,Def11; hence thesis by Def5; end; hence thesis by TARSKI:2; end; theorem R.:{} = {} proof consider y being Element of R.:{}; assume A1: not thesis; y in R.:{} iff ex x st [x,y] in R & x in {} by Def13; hence thesis by A1; end; theorem {}.:X = {} proof consider y being Element of {}.:X; assume not thesis; then ex x st [x,y] in {} & x in X by Def13; hence contradiction; end; theorem R.:X = {} iff dom R misses X proof thus R.:X = {} implies dom R misses X proof assume A1: R.:X = {}; assume not thesis; then consider x be set such that A2: x in dom R & x in X by XBOOLE_0:3; consider y such that A3: [x,y] in R by A2,Def4; thus contradiction by A1,A2,A3,Th143; end; assume A4: dom R /\ X ={}; consider y being Element of R.:X; assume not thesis; then consider x such that A5: x in dom R & [x,y] in R & x in X by Th143; thus contradiction by A4,A5,XBOOLE_0:def 3; end; theorem X <> {} & X c= dom R implies R.:X <> {} proof assume that A1: X <> {} and A2: X c= dom R; consider x being Element of X; A3: x in dom R by A1,A2,TARSKI:def 3; then consider y such that A4: [x,y] in R by Def4; thus thesis by A1,A3,A4,Th143; end; theorem R.:(X \/ Y) = R.:X \/ R.:Y proof now let y; A1: now assume y in R.:(X \/ Y); then consider x such that A2: [x,y] in R & x in X \/ Y by Def13; (x in X or x in Y) & [x,y] in R by A2,XBOOLE_0:def 2; then y in R.:X or y in R.:Y by Def13; hence y in R.:X \/ R.:Y by XBOOLE_0:def 2; end; now assume A3: y in R.:X \/ R.:Y; A4: now assume y in R.:X; then consider x such that A5: [x,y] in R & x in X by Def13; x in X \/ Y & [x,y] in R by A5,XBOOLE_0:def 2; hence y in R.:(X \/ Y) by Def13; end; now assume y in R.:Y; then consider x such that A6: [x,y] in R & x in Y by Def13; x in X \/ Y & [x,y] in R by A6,XBOOLE_0:def 2; hence y in R.:(X \/ Y) by Def13; end; hence y in R.:(X \/ Y) by A3,A4,XBOOLE_0:def 2; end; hence y in R.:(X \/ Y) iff y in R.:X \/ R.:Y by A1; end; hence thesis by TARSKI:2; end; theorem R.:(X /\ Y) c= R.:X /\ R.:Y proof let y; assume y in R.:(X /\ Y); then consider x such that A1: [x,y] in R & x in X /\ Y by Def13; x in X & x in Y & [x,y] in R by A1,XBOOLE_0:def 3; then y in R.:X & y in R.:Y by Def13; hence y in R.:X /\ R.:Y by XBOOLE_0:def 3; end; theorem R.:X \ R.:Y c= R.:(X \ Y) proof let y; assume y in R.:X \ R.:Y; then A1: y in R.:X & not y in R.:Y by XBOOLE_0:def 4; then consider x such that A2: [x,y] in R & x in X by Def13; not x in Y or not [x,y] in R by A1,Def13; then x in X \ Y & [x,y] in R by A2,XBOOLE_0:def 4; hence y in R.:(X \ Y) by Def13; end; theorem Th156: X c= Y implies R.:X c= R.:Y proof assume A1: X c= Y; let y; assume y in R.:X; then consider x such that A2: [x,y] in R & x in X by Def13; thus y in R.:Y by A1,A2,Def13; end; theorem Th157: P c= R implies P.:X c= R.:X proof assume A1: P c= R; let y; assume y in P.:X; then consider x such that A2: [x,y] in P and A3: x in X by Def13; thus thesis by A1,A2,A3,Def13; 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 Th156,Th157; hence thesis by XBOOLE_1:1; end; theorem (P*R).:X=R.:(P.:X) proof y in (P*R).:X iff y in R.:(P.:X) proof 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 Def13; consider z such that A3: [x,z] in P & [z,y] in R by A1,Def8; z in P.:X & [z,y] in R by A2,A3,Def13; hence thesis by Def13; end; assume y in R.:(P.:X); then consider x such that A4: [x,y] in R and A5: x in P.:X by Def13; consider z such that A6: [z,x] in P and A7: z in X by A5,Def13; [z,y] in P*R by A4,A6,Def8; hence thesis by A7,Def13; end; hence thesis by TARSKI:2; end; theorem rng(P*R) = R.:(rng P) proof z in rng(P*R) iff z in R.:(rng P) proof thus z in rng(P*R) implies z in R.:(rng P) proof assume z in rng(P*R); then consider x such that A1: [x,z] in P*R by Def5; consider y such that A2: [x,y] in P & [y,z] in R by A1,Def8; y in rng P by A2,Def5; hence z in R.:(rng P) by A2,Def13; end; assume z in R.:(rng P); then consider y such that A3: [y,z] in R and A4: y in rng P by Def13; consider x such that A5: [x,y] in P by A4,Def5; [x,z] in P*R by A3,A5,Def8; hence z in rng(P*R) by Def5; end; hence thesis by TARSKI:2; end; theorem (R|X).:Y c= R.:Y proof (R|X) c= R by Th88; hence thesis by Th157; end; canceled; theorem (dom R) /\ X c= (R~).:(R.:X) proof let x; assume x in (dom R) /\ X; then A1: x in dom R & x in X by XBOOLE_0:def 3; then consider y such that A2: [x,y] in R by Def4; A3: y in R.:X by A1,A2,Def13; [y,x] in R~ by A2,Def7; hence x in (R~).:(R.:X) by A3,Def13; end; :: INVERSE IMAGE OF SET IN RELATION :: ________________________________ definition let R,Y; func R"Y -> set means :Def14: x in it iff ex y st [x,y] in R & y in Y; existence proof defpred Z[set] means ex y st [$1,y] in R & y in Y; consider X such that A1: for x holds x in X iff x in dom R & Z[x] from Separation; 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 & y in Y; x in dom R by A2,Def4; hence x in X by A1,A2; end; uniqueness proof let X1,X2; assume that A3: x in X1 iff ex y st [x,y] in R & y in Y and A4: x in X2 iff ex y st [x,y] in R & y in Y; now let x; x in X1 iff ex y st [x,y] in R & y in Y by A3; hence x in X1 iff x in X2 by A4; end; hence X1=X2 by TARSKI:2; end; end; canceled 2; theorem Th166: 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 Def14; take y; thus thesis by A1,Def5; end; given y such that A2: y in rng R & [x,y] in R & y in Y; thus x in R"Y by A2,Def14; end; theorem Th167: R"Y c= dom R proof let x; assume x in R"Y; then ex y st [x,y] in R & y in Y by Def14; hence thesis by Def4; end; theorem R"Y = R"(rng R /\ Y) proof x in R"Y iff x in R"(rng R /\ Y) proof 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 & y in Y by Th166; y in rng R /\ Y by A1,A2,XBOOLE_0:def 3; hence thesis by A2,Def14; end; assume x in R"(rng R /\ Y); then consider y such that y in rng R and A3: [x,y] in R & y in rng R /\ Y by Th166; y in Y by A3,XBOOLE_0:def 3; hence thesis by A3,Def14; end; hence thesis by TARSKI:2; end; theorem Th169: R"rng R = dom R proof thus R"rng R c= dom R by Th167; let x; assume x in dom R; then consider y such that A1: [x,y] in R by Def4; y in rng R by A1,Def5; hence thesis by A1,Def14; end; theorem R"Y c= R"rng R proof R"Y c= dom R & R"rng R = dom R by Th167,Th169; hence thesis; end; theorem R"{} = {} proof consider x being Element of R"{}; assume A1: not thesis; x in R"{} iff ex y st [x,y] in R & y in {} by Def14; hence thesis by A1; end; theorem {}"Y = {} proof consider x being Element of {}"Y; assume not thesis; then ex y st [x,y] in {} & y in Y by Def14; hence contradiction; end; theorem R"Y = {} iff rng R misses Y proof thus R"Y = {} implies rng R misses Y proof assume A1: R"Y = {}; assume not thesis; then consider y being set such that A2: y in rng R & y in Y by XBOOLE_0:3; ex x st [x,y] in R by A2,Def5; hence contradiction by A1,A2,Th166; end; assume A3: rng R /\ Y = {}; consider x being Element of R"Y; assume not thesis; then ex y st y in rng R & [x,y] in R & y in Y by Th166; hence contradiction by A3,XBOOLE_0:def 3; end; theorem Y <> {} & Y c= rng R implies R"Y <> {} proof assume that A1: Y <> {} and A2: Y c= rng R; consider y being Element of Y; A3: y in rng R by A1,A2,TARSKI:def 3; then ex x st [x,y] in R by Def5; hence thesis by A1,A3,Th166; end; theorem R"(X \/ Y) = R"X \/ R"Y proof now let x; A1: now assume x in R"(X \/ Y); then consider y such that A2: [x,y] in R & y in X \/ Y by Def14; (y in X or y in Y) & [x,y] in R by A2,XBOOLE_0:def 2; then x in R"X or x in R"Y by Def14; hence x in R"X \/ R"Y by XBOOLE_0:def 2; end; now assume A3: x in R"X \/ R"Y; A4: now assume x in R"X; then consider y such that A5: [x,y] in R & y in X by Def14; y in X \/ Y & [x,y] in R by A5,XBOOLE_0:def 2; hence x in R"(X \/ Y) by Def14; end; now assume x in R"Y; then consider y such that A6: [x,y] in R & y in Y by Def14; y in X \/ Y & [x,y] in R by A6,XBOOLE_0:def 2; hence x in R"(X \/ Y) by Def14; end; hence x in R"(X \/ Y) by A3,A4,XBOOLE_0:def 2; end; hence x in R"(X \/ Y) iff x in R"X \/ R"Y by A1; end; hence thesis by TARSKI:2; end; theorem R"(X /\ Y) c= R"X /\ R"Y proof let x; assume x in R"(X /\ Y); then consider y such that A1: [x,y] in R & y in X /\ Y by Def14; y in X & y in Y & [x,y] in R by A1,XBOOLE_0:def 3; then x in R"X & x in R"Y by Def14; hence x in R"X /\ R"Y by XBOOLE_0:def 3; end; theorem R"X \ R"Y c= R"(X \ Y) proof let x; assume x in R"X \ R"Y; then A1: x in R"X & not x in R"Y by XBOOLE_0:def 4; then consider y such that A2: [x,y] in R & y in X by Def14; not y in Y or not [x,y] in R by A1,Def14; then y in X \ Y & [x,y] in R by A2,XBOOLE_0:def 4; hence x in R"(X \ Y) by Def14; end; theorem Th178: X c= Y implies R"X c= R"Y proof assume A1: X c= Y; let x; assume x in R"X; then ex y st [x,y] in R & y in X by Def14; hence x in R"Y by A1,Def14; end; theorem Th179: P c= R implies P"Y c= R"Y proof assume A1: P c= R; let x; assume x in P"Y; then ex y st [x,y] in P & y in Y by Def14; hence thesis by A1,Def14; 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 Th178,Th179; hence thesis by XBOOLE_1:1; end; theorem (P*R)"Y = P"(R"Y) proof x in (P*R)"Y iff x in P"(R"Y) proof 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 Def14; consider z such that A3: [x,z] in P & [z,y] in R by A1,Def8; z in R"Y & [x,z] in P by A2,A3,Def14; hence thesis by Def14; end; assume x in P"(R"Y); then consider y such that A4: [x,y] in P and A5: y in R"Y by Def14; consider z such that A6: [y,z] in R and A7: z in Y by A5,Def14; [x,z] in P*R by A4,A6,Def8; hence thesis by A7,Def14; end; hence thesis by TARSKI:2; end; theorem dom(P*R) = P"(dom R) proof z in dom(P*R) iff z in P"(dom R) proof thus z in dom(P*R) implies z in P"(dom R) proof assume z in dom(P*R); then consider x such that A1: [z,x] in P*R by Def4; consider y such that A2: [z,y] in P & [y,x] in R by A1,Def8; y in dom R by A2,Def4; hence z in P"(dom R) by A2,Def14; end; assume z in P"(dom R); then consider y such that A3: [z,y] in P and A4: y in dom R by Def14; consider x such that A5: [y,x] in R by A4,Def4; [z,x] in P*R by A3,A5,Def8; hence z in dom(P*R) by Def4; end; hence thesis by TARSKI:2; end; theorem (rng R) /\ Y c= (R~)"(R"Y) proof let y; assume y in (rng R) /\ Y; then A1: y in rng R & y in Y by XBOOLE_0:def 3; then consider x such that A2: [x,y] in R by Def5; A3: x in R"Y by A1,A2,Def14; [y,x] in R~ by A2,Def7; hence y in (R~)"(R"Y) by A3,Def14; end;

Back to top