:: Relations Defined on Sets :: by Edmund Woronowicz :: :: Received April 14, 1989 :: Copyright (c) 1990-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies RELAT_1, SUBSET_1, ZFMISC_1, TARSKI, XBOOLE_0; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1; constructors TARSKI, SUBSET_1, RELAT_1, XTUPLE_0; registrations XBOOLE_0, RELAT_1, SUBSET_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, RELAT_1; equalities RELAT_1; expansions TARSKI, XBOOLE_0, RELAT_1; theorems TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XTUPLE_0; schemes RELAT_1; begin reserve A,B,X,X1,Y,Y1,Y2,Z for set, a,x,y,z for object; :: :: RELATION AS A SUBSET OF CARTESIAN PRODUCT OF TWO SETS :: _____________________________________________________ definition let X,Y; mode Relation of X,Y is Subset of [:X,Y:]; end; registration let X,Y; cluster -> Relation-like for Subset of [:X,Y:]; coherence; end; registration let X,Y; cluster -> X-defined Y-valued for Relation of X,Y; coherence proof let R be Relation of X,Y; thus dom R c= X proof let x be object; assume x in dom R; then ex y being object st [x,y] in R by XTUPLE_0:def 12; hence thesis by ZFMISC_1:87; end; let y be object; assume y in rng R; then ex x being object st [x,y] in R by XTUPLE_0:def 13; hence thesis by ZFMISC_1:87; end; end; reserve P,R for Relation of X,Y; definition let X,Y,R,Z; redefine pred R c= Z means for x being Element of X, y being Element of Y holds [x,y] in R implies [x,y] in Z; compatibility proof thus R c= Z implies for x being Element of X, y being Element of Y holds [ x,y] in R implies [x,y] in Z; assume A1: for x being Element of X, y being Element of Y holds [x,y] in R implies [x,y] in Z; let a,b be object; assume A2: [a,b] in R; then reconsider a9=a as Element of X by ZFMISC_1:87; reconsider b9=b as Element of Y by A2,ZFMISC_1:87; [a9,b9] in Z by A1,A2; hence thesis; end; end; definition let X,Y,P,R; redefine pred P = R means for x being Element of X, y being Element of Y holds [x,y] in P iff [x,y] in R; compatibility proof thus P = R implies for x being Element of X, y being Element of Y holds [x ,y] in P iff [x,y] in R; assume A1: for x being Element of X, y being Element of Y holds [x,y] in P iff [x,y] in R; let a,b be object; hereby assume A2: [a,b] in P; then reconsider a9=a as Element of X by ZFMISC_1:87; reconsider b9=b as Element of Y by A2,ZFMISC_1:87; [a9,b9] in R by A1,A2; hence [a,b] in R; end; assume A3: [a,b] in R; then reconsider a9=a as Element of X by ZFMISC_1:87; reconsider b9=b as Element of Y by A3,ZFMISC_1:87; [a9,b9] in P by A1,A3; hence thesis; end; end; theorem A c= R implies A is Relation of X,Y by XBOOLE_1:1; theorem a in R implies ex x,y st a = [x,y] & x in X & y in Y proof assume A1: a in R; then consider x,y being object such that A2: a = [x,y] by RELAT_1:def 1; x in X & y in Y by A1,A2,ZFMISC_1:87; hence thesis by A2; end; theorem x in X & y in Y implies {[x,y]} is Relation of X,Y by ZFMISC_1:31,87; theorem for R being Relation st dom R c= X & rng R c= Y holds R is Relation of X,Y proof let R be Relation; assume dom R c= X & rng R c= Y; then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X,Y:] by RELAT_1:7 ,ZFMISC_1:96; hence thesis by XBOOLE_1:1; end; theorem dom R c= X1 implies R is Relation of X1,Y proof A1: rng R c= Y by RELAT_1:def 19; assume dom R c= X1; then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X1,Y:] by A1,RELAT_1:7 ,ZFMISC_1:96; hence thesis by XBOOLE_1:1; end; theorem rng R c= Y1 implies R is Relation of X,Y1 proof A1: dom R c= X by RELAT_1:def 18; assume rng R c= Y1; then R c= [:dom R, rng R:] & [:dom R, rng R:] c= [:X,Y1:] by A1,RELAT_1:7 ,ZFMISC_1:96; hence thesis by XBOOLE_1:1; end; theorem X c= X1 & Y c= Y1 implies R is Relation of X1,Y1 proof assume X c= X1 & Y c= Y1; then [:X,Y:] c= [:X1,Y1:] by ZFMISC_1:96; hence thesis by XBOOLE_1:1; end; registration let X; let R,S be X-defined Relation; cluster R \/ S -> X-defined; coherence proof A1: dom(R \/ S) = dom R \/ dom S by XTUPLE_0:23; dom R c= X & dom S c= X by RELAT_1:def 18; hence dom(R \/ S) c= X by A1,XBOOLE_1:8; end; end; registration let X; let R be X-defined Relation, S be Relation; cluster R /\ S -> X-defined; coherence proof R /\ S c= R by XBOOLE_1:17; then dom R c= X & dom(R /\ S) c= dom R by RELAT_1:11,def 18; hence dom(R /\ S) c= X; end; cluster R \ S -> X-defined; coherence; end; registration let X; let R,S be X-valued Relation; cluster R \/ S -> X-valued; coherence proof A1: rng(R \/ S) = rng R \/ rng S by RELAT_1:12; rng R c= X & rng S c= X by RELAT_1:def 19; hence rng(R \/ S) c= X by A1,XBOOLE_1:8; end; end; registration let X; let R be X-valued Relation, S be Relation; cluster R /\ S -> X-valued; coherence proof R /\ S c= R by XBOOLE_1:17; then rng R c= X & rng(R /\ S) c= rng R by RELAT_1:11,def 19; hence rng(R /\ S) c= X; end; cluster R \ S -> X-valued; coherence; end; definition let X; let R be X-defined Relation; redefine func dom R -> Subset of X; coherence by RELAT_1:def 18; end; definition let X; let R be X-valued Relation; redefine func rng R -> Subset of X; coherence by RELAT_1:def 19; end; theorem field R c= X \/ Y proof dom R \/ rng R c= X \/ Y by XBOOLE_1:13; hence thesis; end; theorem (for x being object st x in X ex y being object st [x,y] in R) iff dom R = X proof thus (for x being object st x in X ex y being object st [x,y] in R) implies dom R = X proof assume A1: for x being object st x in X ex y being object st [x,y] in R; now let x be object; now assume x in X; then ex y being object st [x,y] in R by A1; hence x in dom R by XTUPLE_0:def 12; end; hence x in dom R iff x in X; end; hence dom R = X by TARSKI:2; end; thus thesis by XTUPLE_0:def 12; end; theorem (for y being object st y in Y ex x being object st [x,y] in R) iff rng R = Y proof thus (for y being object st y in Y ex x being object st [x,y] in R) implies rng R = Y proof assume A1: for y being object st y in Y ex x being object st [x,y] in R; now let y be object; now assume y in Y; then ex x being object st [x,y] in R by A1; hence y in rng R by XTUPLE_0:def 13; end; hence y in rng R iff y in Y; end; hence rng R = Y by TARSKI:2; end; thus thesis by XTUPLE_0:def 13; end; definition let X,Y,R; redefine func R~ -> Relation of Y,X; coherence proof now let x,y be object; assume [x,y] in R~; then [y,x] in R by RELAT_1:def 7; hence [x,y] in [:Y,X:] by ZFMISC_1:88; end; hence thesis by RELAT_1:def 3; end; end; definition let X,Y1,Y2,Z; let P be Relation of X,Y1; let R be Relation of Y2,Z; redefine func P*R -> Relation of X,Z; coherence proof now let x,z be object; assume [x,z] in P*R; then ex y being object st [x,y] in P & [y,z] in R by RELAT_1:def 8; then x in X & z in Z by ZFMISC_1:87; hence [x,z] in [:X,Z:] by ZFMISC_1:87; end; hence thesis by RELAT_1:def 3; end; end; theorem dom (R~) = rng R & rng (R~) = dom R proof now let x be object; A1: now assume x in rng R; then consider y being object such that A2: [y,x] in R by XTUPLE_0:def 13; [x,y] in R~ by A2,RELAT_1:def 7; hence x in dom (R~) by XTUPLE_0:def 12; end; now assume x in dom (R~); then consider y being object such that A3: [x,y] in R~ by XTUPLE_0:def 12; [y,x] in R by A3,RELAT_1:def 7; hence x in rng R by XTUPLE_0:def 13; end; hence x in dom (R~) iff x in rng R by A1; end; hence dom (R~) = rng R by TARSKI:2; now let x be object; A4: now assume x in dom R; then consider y being object such that A5: [x,y] in R by XTUPLE_0:def 12; [y,x] in R~ by A5,RELAT_1:def 7; hence x in rng (R~) by XTUPLE_0:def 13; end; now assume x in rng (R~); then consider y being object such that A6: [y,x] in R~ by XTUPLE_0:def 13; [x,y] in R by A6,RELAT_1:def 7; hence x in dom R by XTUPLE_0:def 12; end; hence x in rng (R~) iff x in dom R by A4; end; hence thesis by TARSKI:2; end; theorem {} is Relation of X,Y by XBOOLE_1:2; registration let A be empty set, B be set; cluster -> empty for Relation of A,B; coherence; cluster -> empty for Relation of B,A; coherence; end; theorem Th13: id X c= [:X,X:] proof [:X,X:] c= [:X,X:]; then reconsider R = [:X,X:] as Relation of X,X; for x,y being object holds [x,y] in id X implies [x,y] in R proof let x,y be object; assume [x,y] in id X; then x in X & x = y by RELAT_1:def 10; hence thesis by ZFMISC_1:87; end; hence thesis; end; theorem id X is Relation of X,X by Th13; theorem Th15: id A c= R implies A c= dom R & A c= rng R proof assume A1: id A c= R; thus A c= dom R proof let x be object; assume x in A; then [x,x] in id A by RELAT_1:def 10; hence thesis by A1,XTUPLE_0:def 12; end; thus A c= rng R proof let x be object; assume x in A; then [x,x] in id A by RELAT_1:def 10; hence thesis by A1,XTUPLE_0:def 13; end; end; theorem id X c= R implies X = dom R & X c= rng R by Th15; theorem id Y c= R implies Y c= dom R & Y = rng R by Th15; definition let X,Y,R,A; redefine func R|A -> Relation of X,Y; coherence proof now let x,y be object; assume [x,y] in R|A; then [x,y] in R by RELAT_1:def 11; hence [x,y] in [:X,Y:]; end; hence thesis by RELAT_1:def 3; end; end; definition let X,Y,B,R; redefine func B|`R -> Relation of X,Y; coherence proof now let x,y be object; assume [x,y] in B|`R; then [x,y] in R by RELAT_1:def 12; hence [x,y] in [:X,Y:]; end; hence thesis by RELAT_1:def 3; end; end; theorem R|X1 is Relation of X1,Y proof now let x,y be object; assume [x,y] in R|X1; then x in X1 & y in Y by RELAT_1:def 11,ZFMISC_1:87; hence [x,y] in [:X1,Y:] by ZFMISC_1:87; end; hence thesis by RELAT_1:def 3; end; theorem X c= X1 implies R|X1 = R proof assume A1: X c= X1; now let x,y be object; now assume A2: [x,y] in R; then x in X by ZFMISC_1:87; hence [x,y] in R|X1 by A1,A2,RELAT_1:def 11; end; hence [x,y] in R|X1 iff [x,y] in R by RELAT_1:def 11; end; hence thesis; end; theorem Y1|`R is Relation of X,Y1 proof now let x,y be object; assume [x,y] in Y1|`R; then y in Y1 & x in X by RELAT_1:def 12,ZFMISC_1:87; hence [x,y] in [:X,Y1:] by ZFMISC_1:87; end; hence thesis by RELAT_1:def 3; end; theorem Y c= Y1 implies Y1|`R = R proof assume A1: Y c= Y1; now let x,y be object; now assume A2: [x,y] in R; then y in Y by ZFMISC_1:87; hence [x,y] in Y1|`R by A1,A2,RELAT_1:def 12; end; hence [x,y] in Y1|`R iff [x,y] in R by RELAT_1:def 12; end; hence thesis; end; definition let X,Y,R,A; redefine func R.:A -> Subset of Y; coherence proof R.:A c= rng R by RELAT_1:111; hence thesis by XBOOLE_1:1; end; redefine func R"A -> Subset of X; coherence proof R"A c= dom R by RELAT_1:132; hence thesis by XBOOLE_1:1; end; end; theorem Th22: R.:X = rng R & R"Y = dom R proof now let y be object; A1: now assume y in rng R; then consider x being object such that A2: [x,y] in R by XTUPLE_0:def 13; x in X by A2,ZFMISC_1:87; hence y in R.:X by A2,RELAT_1:def 13; end; now assume y in R.:X; then ex x being object st [x,y] in R & x in X by RELAT_1:def 13; hence y in rng R by XTUPLE_0:def 13; end; hence y in R.:X iff y in rng R by A1; end; hence R.:X = rng R by TARSKI:2; now let x be object; A3: now assume x in dom R; then consider y being object such that A4: [x,y] in R by XTUPLE_0:def 12; y in Y by A4,ZFMISC_1:87; hence x in R"Y by A4,RELAT_1:def 14; end; now assume x in R"Y; then ex y being object st [x,y] in R & y in Y by RELAT_1:def 14; hence x in dom R by XTUPLE_0:def 12; end; hence x in R"Y iff x in dom R by A3; end; hence thesis by TARSKI:2; end; theorem R.:(R"Y) = rng R & R"(R.:X) = dom R proof R"Y = dom R & R.:X = rng R by Th22; hence thesis by RELAT_1:113,134; end; scheme RelOnSetEx{A() -> set,B() -> set,P[object,object]}: ex R being Relation of A(),B() st for x,y holds [x,y] in R iff x in A() & y in B() & P[x,y] proof consider R being Relation such that A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y] from RELAT_1:sch 1; R c= [:A(),B():] proof let x1,x2 be object; assume [x1,x2] in R; then x1 in A() & x2 in B() by A1; hence thesis by ZFMISC_1:87; end; then reconsider R as Relation of A(),B(); take R; thus thesis by A1; end; :: Relation on a set definition let X; mode Relation of X is Relation of X,X; end; reserve D,D1,D2,E,F for non empty set; reserve R for Relation of D,E; reserve x for Element of D; reserve y for Element of E; registration let D be non empty set; cluster id D -> non empty; coherence proof now set y = the Element of D; A1: [y,y] in id D by RELAT_1:def 10; assume id D = {}; hence contradiction by A1; end; hence thesis; end; end; theorem for x being Element of D holds x in dom R iff ex y being Element of E st [x,y] in R proof let x be Element of D; thus x in dom R implies ex y being Element of E st [x,y] in R proof assume x in dom R; then consider y being object such that A1: [x,y] in R by XTUPLE_0:def 12; reconsider b = y as Element of E by A1,ZFMISC_1:87; take b; thus thesis by A1; end; given y being Element of E such that A2: [x,y] in R; thus thesis by A2,XTUPLE_0:def 12; end; theorem for y being object holds y in rng R iff ex x being Element of D st [x,y] in R proof let y be object; thus y in rng R implies ex x being Element of D st [x,y] in R proof assume y in rng R; then consider x being object such that A1: [x,y] in R by XTUPLE_0:def 13; reconsider a = x as Element of D by A1,ZFMISC_1:87; take a; thus thesis by A1; end; thus thesis by XTUPLE_0:def 13; end; theorem dom R <> {} implies ex y being Element of E st y in rng R proof assume dom R <> {}; then rng R <> {} by RELAT_1:42; then ex y being object st y in rng R by XBOOLE_0:def 1; hence thesis; end; theorem rng R <> {} implies ex x being Element of D st x in dom R proof assume rng R <> {}; then dom R <> {} by RELAT_1:42; then ex x being object st x in dom R by XBOOLE_0:def 1; hence thesis; end; theorem for P being Relation of D,E, R being Relation of E,F for x, z being object holds [x,z] in P*R iff ex y being Element of E st [x,y] in P & [y,z] in R proof let P be Relation of D,E, R be Relation of E,F; let x, z be object; thus [x,z] in P*R implies ex y being Element of E st [x,y] in P & [y,z] in R proof assume [x,z] in P*R; then consider y being object such that A1: [x,y] in P and A2: [y,z] in R by RELAT_1:def 8; reconsider a = y as Element of E by A1,ZFMISC_1:87; take a; thus thesis by A1,A2; end; given y such that A3: [x,y] in P & [y,z] in R; thus thesis by A3,RELAT_1:def 8; end; theorem y in R.:D1 iff ex x being Element of D st [x,y] in R & x in D1 proof thus y in R.:D1 implies ex x being Element of D st [x,y] in R & x in D1 proof assume y in R.:D1; then consider x being object such that A1: [x,y] in R and A2: x in D1 by RELAT_1:def 13; reconsider a = x as Element of D by A1,ZFMISC_1:87; take a; thus thesis by A1,A2; end; given x such that A3: [x,y] in R & x in D1; thus thesis by A3,RELAT_1:def 13; end; theorem x in R"D2 iff ex y being Element of E st [x,y] in R & y in D2 proof thus x in R"D2 implies ex y being Element of E st [x,y] in R & y in D2 proof assume x in R"D2; then consider y being object such that A1: [x,y] in R and A2: y in D2 by RELAT_1:def 14; reconsider b = y as Element of E by A1,ZFMISC_1:87; take b; thus thesis by A1,A2; end; given y being Element of E such that A3: [x,y] in R & y in D2; thus thesis by A3,RELAT_1:def 14; end; scheme RelOnDomEx{A,B() -> non empty set, P[object,object]}: ex R being Relation of A(),B () st for x being Element of A(), y being Element of B() holds [x,y] in R iff P [x,y] proof consider R being Relation of A(),B() qua set such that A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y] from RelOnSetEx; take R; thus thesis by A1; end; begin :: Addenda :: missing, 2006.11.04, A.T. scheme { N()-> set, M() -> Subset of N(), F(object)->set }: ex R being Relation of M() st for i being Element of N() st i in M() holds Im(R,i) = F(i) provided A1: for i being Element of N() st i in M() holds F(i) c= M() proof defpred P[object,object] means \$2 in F(\$1); consider R being Relation of M() such that A2: for x,y being object holds [x,y] in R iff x in M() & y in M() & P[x,y] from RelOnSetEx; take R; let i be Element of N(); assume A3: i in M(); thus Im(R,i) c= F(i) proof let e be object; assume e in Im(R,i); then consider u being object such that A4: [u,e] in R and A5: u in {i} by RELAT_1:def 13; u = i by A5,TARSKI:def 1; hence thesis by A2,A4; end; let e be object; assume A6: e in F(i); F(i) c= M() by A1,A3; then i in {i} & [i,e] in R by A2,A3,A6,TARSKI:def 1; hence thesis by RELAT_1:def 13; end; theorem for N being set, R,S being Relation of N st for i being set st i in N holds Im(R,i) = Im(S,i) holds R = S proof let N be set, R,S be Relation of N such that A1: for i being set st i in N holds Im(R,i) = Im(S,i); let a,b be Element of N; thus [a,b] in R implies [a,b] in S proof assume A2: [a,b] in R; then A3: a in dom R by XTUPLE_0:def 12; a in {a} by TARSKI:def 1; then b in Im(R,a) by A2,RELAT_1:def 13; then b in Im(S,a) by A1,A3; then ex e being object st [e,b] in S & e in {a} by RELAT_1:def 13; hence thesis by TARSKI:def 1; end; assume A4: [a,b] in S; then A5: a in dom S by XTUPLE_0:def 12; a in {a} by TARSKI:def 1; then b in Im(S,a) by A4,RELAT_1:def 13; then b in Im(R,a) by A1,A5; then ex e being object st [e,b] in R & e in {a} by RELAT_1:def 13; hence thesis by TARSKI:def 1; end; :: from AMI_3, 2007.06.13, A.T. (generalized) scheme {A,B() -> set, P[set,set], P,R()->Relation of A(), B()}: P() = R() provided A1: for p being Element of A(), q being Element of B() holds [p,q] in P( ) iff P[p,q] and A2: for p being Element of A(), q being Element of B() holds [p,q] in R( ) iff P[p,q] proof let y be Element of A(), z be Element of B(); [y,z] in P() iff P[y,z] by A1; hence thesis by A2; end; :: missing, 2007.06.14, A.T. registration let X,Y,Z; let f be Relation of [:X,Y:], Z; cluster dom f -> Relation-like; coherence; end; registration let X,Y,Z; let f be Relation of X, [:Y, Z:]; cluster rng f -> Relation-like; coherence; end; :: missing, 2008.04.30, A.T. theorem A misses X implies P|A = {} proof assume A misses X; then A misses dom P by XBOOLE_1:63; hence thesis by RELAT_1:152; end; :: missing, 2008.09.15, A.T. registration let R be non empty Relation, Y be non empty Subset of dom R; cluster R|Y -> non empty; coherence proof dom(R|Y) = Y by RELAT_1:62; hence thesis; end; end; registration let R be non empty Relation; let Y be non empty Subset of dom R; cluster R.:Y -> non empty; coherence proof R.:Y = rng(R|Y) by RELAT_1:115; hence thesis; end; end; :: missing, 2008.11.29 A.T. registration let X,Y be set; cluster empty for Relation of X,Y; existence proof {} is Relation of X,Y by XBOOLE_1:2; hence thesis; end; end; scheme {A() -> set,B() -> set,P[object,object]}: ex R being Relation of A(),B() st for x,y being set holds [x,y] in R iff x in A() & y in B() & P[x,y]; consider R being Relation of A(),B() such that A1: for x,y being object holds [x,y] in R iff x in A() & y in B() & P[x,y] from RelOnSetEx; take R; thus thesis by A1; end;