### The Mizar article:

### Functions and Their Basic Properties

**by****Czeslaw Bylinski**

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

- MML identifier: FUNCT_1
- [ MML identifier index ]

environ vocabulary RELAT_1, BOOLE, FUNCT_1; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1; constructors TARSKI, RELAT_1, SUBSET_1, XBOOLE_0; clusters SUBSET_1, RELAT_1, ZFMISC_1, XBOOLE_0; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, RELAT_1; theorems TARSKI, XBOOLE_0, ZFMISC_1, RELAT_1, XBOOLE_1; schemes TARSKI, XBOOLE_0; begin reserve X,X1,X2,Y,Y1,Y2 for set, p,x,x1,x2,y,y1,y2,z,z1,z2 for set; definition let X be set; attr X is Function-like means :Def1: for x,y1,y2 st [x,y1] in X & [x,y2] in X holds y1 = y2; end; definition cluster Relation-like Function-like set; existence proof take {}; thus (for p st p in {} ex x,y st [x,y] = p) & (for x,y1,y2 st [x,y1] in {} & [x,y2] in {} holds y1 = y2); end; end; definition mode Function is Function-like Relation-like set; end; definition cluster empty -> Function-like set; coherence proof let f be set; assume f is empty; hence for x,y1,y2 st [x,y1] in f & [x,y2] in f holds y1 = y2; end; end; reserve f,g,g1,g2,h for Function, R,S for Relation; canceled; theorem for F being set st (for p st p in F ex x,y st [x,y] = p) & (for x,y1,y2 st [x,y1] in F & [x,y2] in F holds y1 = y2) holds F is Function by Def1,RELAT_1:def 1; scheme GraphFunc{A()->set,P[set,set]}: ex f st for x,y holds [x,y] in f iff x in A() & P[x,y] provided A1: for x,y1,y2 st P[x,y1] & P[x,y2] holds y1 = y2 proof defpred R[set,set] means P[$1,$2]; A2: for x,y1,y2 st R[x,y1] & R[x,y2] holds y1 = y2 by A1; consider Y such that A3: for y holds y in Y iff ex x st x in A() & R[x,y] from Fraenkel(A2); defpred R[set] means ex x,y st [x,y] = $1 & P[x,y]; consider F being set such that A4: p in F iff p in [:A(),Y:] & R[p] from Separation; now thus p in F implies ex x,y st [x,y] = p proof p in F implies ex x,y st [x,y] = p & P[x,y] by A4; hence thesis; end; let x,y1,y2; assume [x,y1] in F; then consider x1,z1 such that A5: [x1,z1] = [x,y1] and A6: P[x1,z1] by A4; assume [x,y2] in F; then consider x2,z2 such that A7: [x2,z2] = [x,y2] and A8: P[x2,z2] by A4; x = x1 & z1 = y1 & x = x2 & z2 = y2 by A5,A7,ZFMISC_1:33; hence y1 = y2 by A1,A6,A8; end; then reconsider f = F as Function by Def1,RELAT_1:def 1; take f; let x,y; thus [x,y] in f implies x in A() & P[x,y] proof assume A9: [x,y] in f; then [x,y] in [:A(),Y:] by A4; hence x in A() by ZFMISC_1:106; consider x1,y1 such that A10: [x1,y1] = [x,y] and A11: P[x1,y1] by A4,A9; x1 = x & y1 = y by A10,ZFMISC_1:33; hence thesis by A11; end; assume that A12: x in A() and A13: P[x,y]; y in Y by A3,A12,A13; then [x,y] in [:A(),Y:] by A12,ZFMISC_1:106; hence thesis by A4,A13; end; definition let f,x; canceled 2; func f.x -> set means :Def4: [x,it] in f if x in dom f otherwise it = {}; existence by RELAT_1:def 4; uniqueness by Def1; consistency; end; canceled 5; theorem Th8: [x,y] in f iff x in dom f & y = f.x proof thus [x,y] in f implies x in dom f & y = f.x proof assume A1: [x,y] in f; hence x in dom f by RELAT_1:def 4; hence thesis by A1,Def4; end; thus thesis by Def4; end; theorem Th9: dom f = dom g & (for x st x in dom f holds f.x = g.x) implies f = g proof assume that A1: dom f = dom g and A2: for x st x in dom f holds f.x = g.x; A3: (for p st p in f ex x,y st [x,y] = p) & (for p st p in g ex x,y st [x,y] = p) by RELAT_1:def 1; [x,y] in f iff [x,y] in g proof thus [x,y] in f implies [x,y] in g proof assume A4: [x,y] in f; then A5: x in dom f by RELAT_1:def 4; then f.x = y by A4,Def4; then g.x = y by A2,A5; hence thesis by A1,A5,Def4; end; assume A6: [x,y] in g; then A7: x in dom g by RELAT_1:def 4; then g.x = y by A6,Def4; then f.x = y by A1,A2,A7; hence thesis by A1,A7,Def4; end; hence thesis by A3,ZFMISC_1:112; end; definition let f; redefine func rng f means :Def5: for y holds y in it iff ex x st x in dom f & y = f.x; compatibility proof let Y; hereby assume A1: Y = rng f; let y; hereby assume y in Y; then consider x such that A2: [x,y] in f by A1,RELAT_1:def 5; take x; thus x in dom f & y = f.x by A2,Th8; end; given x such that A3: x in dom f and A4: y = f.x; [x,y] in f by A3,A4,Def4; hence y in Y by A1,RELAT_1:def 5; end; assume A5: for y holds y in Y iff ex x st x in dom f & y = f.x; hereby let y; assume y in Y; then consider x such that A6: x in dom f and A7: y = f.x by A5; [x,y] in f by A6,A7,Def4; hence y in rng f by RELAT_1:def 5; end; let y; assume y in rng f; then consider x such that A8: [x,y] in f by RELAT_1:def 5; x in dom f & y = f.x by A8,Th8; hence y in Y by A5; end; end; canceled 2; theorem x in dom f implies f.x in rng f by Def5; canceled; theorem Th14: dom f = {x} implies rng f = {f.x} proof assume A1: dom f = {x}; y in rng f iff y in {f.x} proof thus y in rng f implies y in {f.x} proof assume y in rng f; then consider z such that A2: z in dom f and A3: y = f.z by Def5; z = x by A1,A2,TARSKI:def 1; hence thesis by A3,TARSKI:def 1; end; assume y in {f.x}; then y = f.x & x in dom f by A1,TARSKI:def 1; hence y in rng f by Def5; end; hence thesis by TARSKI:2; end; scheme FuncEx{A()->set,P[set,set]}: ex f st dom f = A() & for x st x in A() holds P[x,f.x] provided A1: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2 and A2: for x st x in A() ex y st P[x,y] proof defpred R[set,set] means $1 in A() & P[$1,$2]; A3: for x,y1,y2 st R[x,y1] & R[x,y2] holds y1 = y2 by A1; consider f being Function such that A4: for x,y holds [x,y] in f iff x in A() & R[x,y] from GraphFunc(A3); take f; x in dom f iff x in A() proof thus x in dom f implies x in A() proof assume x in dom f; then ex y st [x,y] in f by RELAT_1:def 4; hence x in A() by A4; end; assume A5: x in A(); then consider y such that A6: P[x,y] by A2; [x,y] in f by A4,A5,A6; hence x in dom f by RELAT_1:def 4; end; hence A7: dom f = A() by TARSKI:2; let x; assume A8: x in A(); then consider y such that A9: P[x,y] by A2; [x,y] in f by A4,A8,A9; hence thesis by A7,A8,A9,Def4; end; scheme Lambda{A()->set,F(set)->set}: ex f being Function st dom f = A() & for x st x in A() holds f.x = F(x) proof deffunc G(set) = F($1); defpred P[set,set] means $2 = G($1); A1: for x,y1,y2 st x in A() & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x st x in A() ex y st P[x,y]; thus ex f being Function st dom f = A() & for x st x in A() holds P[x,f.x] from FuncEx(A1,A2); end; theorem X <> {} implies for y ex f st dom f = X & rng f = {y} proof assume A1: X <> {}; let y; deffunc F(set) = y; consider f such that A2: dom f = X and A3: for x st x in X holds f.x = F(x) from Lambda; take f; thus dom f = X by A2; y1 in rng f iff y1 = y proof A4: now assume y1 in rng f; then ex x st x in dom f & y1 = f.x by Def5; hence y1 = y by A2,A3; end; now assume A5: y1 = y; consider x being Element of X; f.x = y by A1,A3; hence y1 in rng f by A1,A2,A5,Def5; end; hence thesis by A4; end; hence rng f = {y} by TARSKI:def 1; end; theorem (for f,g st dom f = X & dom g = X holds f = g) implies X = {} proof assume A1: for f,g st dom f = X & dom g = X holds f = g; consider x being Element of X; assume A2: not thesis; deffunc F(set) = 0; consider f being Function such that A3: dom f = X and A4: for x st x in X holds f.x = F(x) from Lambda; deffunc F(set) = 1; consider g being Function such that A5: dom g = X and A6: for x st x in X holds g.x = F(x) from Lambda; f.x = 0 & g.x = 1 by A2,A4,A6; hence contradiction by A1,A3,A5; end; theorem dom f = dom g & rng f = {y} & rng g = {y} implies f = g proof assume that A1: dom f = dom g and A2: rng f = {y} & rng g = {y}; x in dom f implies f.x = g.x proof assume x in dom f; then f.x in rng f & g.x in rng g by A1,Def5; then f.x = y & g.x = y by A2,TARSKI:def 1; hence thesis; end; hence f = g by A1,Th9; end; theorem Y <> {} or X = {} implies ex f st X = dom f & rng f c= Y proof assume A1: Y <> {} or X = {}; A2: now assume A3: X = {}; deffunc F(set) = $1; consider f being Function such that A4: dom f = {} and for x st x in {} holds f.x = F(x) from Lambda; take f; thus dom f = X by A3,A4; rng f = {} by A4,RELAT_1:65; hence rng f c= Y by XBOOLE_1:2; end; now assume A5: X <> {}; consider y being Element of Y; A6: y in Y by A1,A5; deffunc F(set) = y; consider f such that A7: dom f = X and A8: for x st x in X holds f.x = F(x) from Lambda; take f; thus dom f = X by A7; z in rng f implies z in Y proof assume z in rng f; then ex x st x in dom f & z = f.x by Def5; hence z in Y by A6,A7,A8; end; hence rng f c= Y by TARSKI:def 3; end; hence thesis by A2; end; theorem (for y st y in Y ex x st x in dom f & y = f.x) implies Y c= rng f proof assume A1: for y st y in Y ex x st x in dom f & y = f.x; let y; assume y in Y; then ex x st x in dom f & y = f.x by A1; hence y in rng f by Def5; end; definition let f,g; redefine func f*g; synonym g*f; end; definition let f,g; cluster g*f -> Function-like; coherence proof let x,y1,y2; assume [x,y1] in g*f; then consider z1 such that A1: [x,z1] in f & [z1,y1] in g by RELAT_1:def 8; assume [x,y2] in g*f; then consider z2 such that A2: [x,z2] in f & [z2,y2] in g by RELAT_1:def 8; z1 = z2 by A1,A2,Def1; hence y1 = y2 by A1,A2,Def1; end; end; theorem for h st (for x holds x in dom h iff x in dom f & f.x in dom g) & (for x st x in dom h holds h.x = g.(f.x)) holds h = g*f proof let h; assume that A1: for x holds x in dom h iff x in dom f & f.x in dom g and A2: for x st x in dom h holds h.x = g.(f.x); now let x,y; hereby assume A3: [x,y] in h; then A4: x in dom h by RELAT_1:def 4; then A5: y = h.x by A3,Def4 .= g.(f.x) by A2,A4; take y1 = f.x; x in dom f by A1,A4; hence [x,y1] in f by Def4; f.x in dom g by A1,A4; hence [y1,y] in g by A5,Def4; end; given z such that A6: [x,z] in f and A7: [z,y] in g; A8: x in dom f by A6,RELAT_1:def 4; then A9: z = f.x by A6,Def4; A10: z in dom g by A7,RELAT_1:def 4; then A11: y = g.z by A7,Def4; A12: x in dom h by A1,A8,A9,A10; then y = h.x by A2,A9,A11; hence [x,y] in h by A12,Def4; end; hence h = g*f by RELAT_1:def 8; end; theorem Th21: x in dom(g*f) iff x in dom f & f.x in dom g proof set h = g*f; hereby assume x in dom h; then consider y such that A1: [x,y] in h by RELAT_1:def 4; consider z such that A2: [x,z] in f and A3: [z,y] in g by A1,RELAT_1:def 8; thus x in dom f by A2,RELAT_1:def 4; then z = f.x by A2,Def4; hence f.x in dom g by A3,RELAT_1:def 4; end; assume A4: x in dom f; then consider z such that A5: [x,z] in f by RELAT_1:def 4; assume f.x in dom g; then consider y such that A6: [f.x,y] in g by RELAT_1:def 4; z = f.x by A4,A5,Def4; then [x,y] in h by A5,A6,RELAT_1:def 8; hence x in dom h by RELAT_1:def 4; end; theorem Th22: x in dom(g*f) implies (g*f).x = g.(f.x) proof set h = g*f; assume A1: x in dom h; then consider y such that A2: [x,y] in h by RELAT_1:def 4; consider z such that A3: [x,z] in f and A4: [z,y] in g by A2,RELAT_1:def 8; x in dom f by A3,RELAT_1:def 4; then A5: z = f.x by A3,Def4; then f.x in dom g by A4,RELAT_1:def 4; then y = g.(f.x) by A4,A5,Def4; hence h.x = g.(f.x) by A1,A2,Def4; end; theorem Th23: x in dom f implies (g*f).x = g.(f.x) proof assume A1: x in dom f; per cases; suppose f.x in dom g; then x in dom(g*f) by A1,Th21; hence (g*f).x = g.(f.x) by Th22; suppose A2: not f.x in dom g; then not x in dom(g*f) by Th21; hence (g*f).x = {} by Def4 .= g.(f.x) by A2,Def4; end; canceled; theorem z in rng(g*f) implies z in rng g proof assume z in rng(g*f); then consider x such that A1: x in dom(g*f) and A2: z = (g*f).x by Def5; f.x in dom g & (g*f).x = g.(f.x) by A1,Th21,Th22; hence z in rng g by A2,Def5; end; canceled; theorem Th27: dom(g*f) = dom f implies rng f c= dom g proof assume A1: dom(g*f) = dom f; let y; assume y in rng f; then ex x st x in dom f & y = f.x by Def5; hence y in dom g by A1,Th21; end; canceled 5; theorem rng f c= Y & (for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h) implies Y = rng f proof assume that A1: rng f c= Y and A2: for g,h st dom g = Y & dom h = Y & g*f = h*f holds g = h; Y c= rng f proof let y; assume that A3: y in Y and A4: not y in rng f; deffunc F(set) = 0; consider g being Function such that A5: dom g = Y and A6: x in Y implies g.x = F(x) from Lambda; defpred P[set,set] means ($1 = y implies $2 = 1) & ($1 <> y implies $2 = 0); A7: x in Y implies ex y1 st P[x,y1] proof assume x in Y; (x = y implies thesis) & (x <> y implies thesis); hence thesis; end; A8: for x,y1,y2 st x in Y & P[x,y1] & P[x,y2] holds y1 = y2; consider h being Function such that A9: dom h = Y and A10: for x st x in Y holds P[x,h.x] from FuncEx(A8,A7); A11: dom(g*f) = dom f & dom(h*f) = dom f by A1,A5,A9,RELAT_1:46; x in dom f implies (g*f).x = (h*f).x proof assume A12: x in dom f; then f.x in rng f by Def5; then g.(f.x) = 0 & h.(f.x) = 0 & (g*f).x = g.(f.x) & (h*f).x = h.(f.x) by A1,A4,A6,A10,A11,A12,Th22; hence thesis; end; then g*f = h*f by A11,Th9; then g.y = 0 & h.y = 1 & g = h by A2,A3,A5,A6,A9,A10; hence contradiction; end; hence thesis by A1,XBOOLE_0:def 10; end; definition let X; cluster id X -> Function-like; coherence proof let x,y1,y2; assume [x,y1] in id X & [x,y2] in id X; then x = y1 & x = y2 by RELAT_1:def 10; hence y1 = y2; end; end; theorem Th34: f = id X iff dom f = X & for x st x in X holds f.x = x proof hereby assume A1: f = id X; hence A2: dom f = X by RELAT_1:71; let x; assume A3: x in X; then [x,x] in f by A1,RELAT_1:def 10; hence f.x = x by A2,A3,Def4; end; assume that A4: dom f = X and A5: for x st x in X holds f.x = x; now let x,y; hereby assume A6: [x,y] in f; hence x in X by A4,Th8; then y = f.x & x = f.x by A5,A6,Th8; hence x = y; end; assume A7: x in X; then f.x = x by A5; hence x = y implies [x,y] in f by A4,A7,Th8; end; hence f = id X by RELAT_1:def 10; end; theorem x in X implies (id X).x = x by Th34; canceled; theorem Th37: dom(f*(id X)) = dom f /\ X proof x in dom(f*(id X)) iff x in dom f /\ X proof x in dom(f*(id X)) iff x in dom f & x in X proof thus x in dom(f*(id X)) implies x in dom f & x in X proof assume x in dom(f*(id X)); then x in dom((id X)) & dom((id X)) = X & (id X).x in dom f by Th21,Th34; hence thesis by Th34; end; assume A1: x in dom f; assume A2: x in X; then (id X).x in dom f & dom((id X)) = X by A1,Th34; hence thesis by A2,Th21; end; hence thesis by XBOOLE_0:def 3; end; hence thesis by TARSKI:2; end; theorem x in dom f /\ X implies f.x = (f*(id X)).x proof assume x in dom f /\ X; then dom id X = X & x in X & x in dom f by Th34,XBOOLE_0:def 3; then (id X).x = x & x in dom id X & x in dom f by Th34; hence thesis by Th23; end; canceled; theorem x in dom((id Y)*f) iff x in dom f & f.x in Y proof dom((id Y)) = Y by Th34; hence thesis by Th21; end; canceled; theorem f*(id dom f) = f & (id rng f)*f = f by RELAT_1:77,79; theorem (id X)*(id Y) = id(X /\ Y) proof A1: dom((id X)*(id Y)) = dom((id X)) /\ Y by Th37 .= X /\ Y by Th34; A2: X /\ Y = dom id(X /\ Y) by Th34; z in X /\ Y implies ((id X)*(id Y)).z = (id(X /\ Y)).z proof assume A3: z in X /\ Y; then A4: z in X & z in Y by XBOOLE_0:def 3; thus ((id X)*(id Y)).z = (id X).((id Y).z) by A1,A3,Th22 .= (id X).z by A4,Th34 .= z by A4,Th34 .= (id(X /\ Y)).z by A3,Th34; end; hence thesis by A1,A2,Th9; end; theorem Th44: rng f = dom g & g*f = f implies g = id dom g proof assume that A1: rng f = dom g and A2: g*f = f; set X = dom g; x in X implies g.x = x proof assume x in X; then ex y st y in dom f & f.y = x by A1,Def5; hence x = g.x by A2,Th23; end; hence g = id X by Th34; end; definition let f; canceled 2; attr f is one-to-one means :Def8: for x1,x2 st x1 in dom f & x2 in dom f & f.x1 = f.x2 holds x1 = x2; end; canceled; theorem Th46: f is one-to-one & g is one-to-one implies g*f is one-to-one proof assume that A1: f is one-to-one and A2: g is one-to-one; now let x1,x2; assume A3: x1 in dom(g*f) & x2 in dom(g*f); then A4: f.x1 in dom g & f.x2 in dom g & (g*f).x1 = g.(f.x1) & (g*f).x2 = g .(f.x2) by Th21,Th22; assume (g*f).x1 = (g*f).x2; then f.x1 = f.x2 & x1 in dom f & x2 in dom f by A2,A3,A4,Def8,Th21; hence x1 = x2 by A1,Def8; end; hence thesis by Def8; end; theorem Th47: g*f is one-to-one & rng f c= dom g implies f is one-to-one proof assume that A1: g*f is one-to-one and A2: rng f c= dom g; now let x1,x2; assume that A3: x1 in dom f & x2 in dom f and A4: f.x1 =f.x2; (g*f).x1 = g.(f.x1) & (g*f).x2 = g.(f.x2) & x1 in dom(g*f) & x2 in dom(g*f) by A2,A3,Th23,RELAT_1:46; hence x1 = x2 by A1,A4,Def8; end; hence f is one-to-one by Def8; end; theorem g*f is one-to-one & rng f = dom g implies f is one-to-one & g is one-to-one proof assume that A1: g*f is one-to-one and A2: rng f = dom g; thus f is one-to-one by A1,A2,Th47; assume not g is one-to-one; then consider y1,y2 such that A3: y1 in dom g and A4: y2 in dom g and A5: g.y1 = g.y2 and A6: y1 <> y2 by Def8; consider x1 such that A7: x1 in dom f and A8: f.x1 = y1 by A2,A3,Def5; consider x2 such that A9: x2 in dom f and A10: f.x2 = y2 by A2,A4,Def5; dom(g*f) = dom f & (g*f).x1 = g.(f.x1) & (g*f).x2 = g.(f.x2) by A2,A7,A9,Th23,RELAT_1:46; hence contradiction by A1,A5,A6,A7,A8,A9,A10,Def8; end; theorem f is one-to-one iff (for g,h st rng g c= dom f & rng h c= dom f & dom g = dom h & f*g = f*h holds g = h) proof thus f is one-to-one implies (for g,h st rng g c=dom f & rng h c=dom f & dom g = dom h & f*g = f*h holds g = h) proof assume A1: f is one-to-one; let g,h such that A2: rng g c= dom f and A3: rng h c= dom f and A4: dom g = dom h and A5: f*g = f*h; x in dom g implies g.x = h.x proof assume x in dom g; then (f*g).x = f.(g.x) & (f*h).x = f.(h.x) & g.x in rng g & h.x in rng h & (g.x in rng g implies g.x in dom f) & (h.x in rng h implies h.x in dom f) by A2,A3,A4,Def5,Th23; hence thesis by A1,A5,Def8; end; hence g = h by A4,Th9; end; assume A6: for g,h st rng g c=dom f & rng h c=dom f & dom g = dom h & f*g = f*h holds g = h; x1 in dom f & x2 in dom f & f.x1 = f.x2 implies x1 = x2 proof assume that A7: x1 in dom f & x2 in dom f and A8: f.x1 = f.x2; deffunc F(set) = x1; consider g being Function such that A9: dom g = {{}} and A10: for x st x in {{}} holds g.x = F(x) from Lambda; deffunc F(set) = x2; consider h being Function such that A11: dom h = {{}} and A12: for x st x in {{}} holds h.x = F(x) from Lambda; {} in {{}} by TARSKI:def 1; then A13: g.{} = x1 & h.{} = x2 by A10,A12; then rng g = {x1} & rng h = {x2} by A9,A11,Th14; then A14: rng g c= dom f & rng h c= dom f by A7,ZFMISC_1:37; then A15: dom(f*g) = dom g & dom(f*h) = dom h by RELAT_1:46; x in dom(f*g) implies (f*g).x = (f*h).x proof assume x in dom(f*g); then (f*g).x = f.(g.x) & (f*h).x = f.(h.x) & g.x = x1 & h.x = x2 by A9,A10,A11,A12,A15,Th22; hence thesis by A8; end; then f*g = f*h by A9,A11,A15,Th9; hence thesis by A6,A13,A14,A15; end; hence f is one-to-one by Def8; end; theorem dom f = X & dom g = X & rng g c= X & f is one-to-one & f*g = f implies g = id X proof assume that A1: dom f = X and A2: dom g = X and A3: rng g c= X and A4: f is one-to-one and A5: f*g = f; x in X implies g.x = x proof assume A6: x in X; then g.x in rng g by A2,Def5; then f.x = f.(g.x) & g.x in X by A2,A3,A5,A6,Th23; hence x = g.x by A1,A4,A6,Def8; end; hence g = id X by A2,Th34; end; theorem rng(g*f) = rng g & g is one-to-one implies dom g c= rng f proof assume that A1: rng(g*f) = rng g and A2: g is one-to-one; let y; assume A3: y in dom g; then g.y in rng(g*f) by A1,Def5; then consider x such that A4: x in dom(g*f) and A5: g.y = (g*f).x by Def5; (g*f).x = g.(f.x) & f.x in dom g by A4,Th21,Th22; then y = f.x & x in dom f by A2,A3,A4,A5,Def8,Th21; hence y in rng f by Def5; end; theorem Th52: id X is one-to-one proof let x1,x2; assume x1 in dom id X & x2 in dom id X; then x1 in X & x2 in X by Th34; then (id X).x1 = x1 & (id X).x2 = x2 by Th34; hence thesis; end; theorem (ex g st g*f = id dom f) implies f is one-to-one proof given g such that A1: g*f = id dom f; dom(g*f) = dom f by A1,RELAT_1:71; then g*f is one-to-one & rng f c= dom g by A1,Th27,Th52; hence f is one-to-one by Th47; end; definition cluster empty Function; existence proof {} is Function; hence thesis; end; end; definition cluster empty -> one-to-one Function; coherence proof let f be Function; assume A1: f is empty; let x1,x2; thus thesis by A1,RELAT_1:60; end; end; definition cluster one-to-one Function; existence proof consider f being empty Function; take f; thus thesis; end; end; definition let f be one-to-one Function; cluster f~ -> Function-like; coherence proof let x,y1,y2; assume [x,y1] in f~ & [x,y2] in f~; then A1: [y1,x] in f & [y2,x] in f by RELAT_1:def 7; then A2: y1 in dom f & y2 in dom f by RELAT_1:def 4; then x = f.y1 & x = f.y2 by A1,Def4; hence y1 = y2 by A2,Def8; end; end; definition let f; assume A1: f is one-to-one; func f" -> Function equals :Def9: f~; coherence proof reconsider g=f as one-to-one Function by A1; g~ is Function; hence f~ is Function; end; end; theorem Th54: f is one-to-one implies for g being Function holds g=f" iff dom g = rng f & for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x proof assume A1: f is one-to-one; let g be Function; thus g = f" implies dom g = rng f & for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x proof assume g = f"; then A2: g = f~ by A1,Def9; hence dom g = rng f by RELAT_1:37; let y,x; thus y in rng f & x = g.y implies x in dom f & y = f.x proof assume that A3: y in rng f and A4: x = g.y; y in dom g by A2,A3,RELAT_1:37; then [y,x] in g by A4,Def4; then A5: [x,y] in f by A2,RELAT_1:def 7; hence x in dom f by RELAT_1:def 4; hence y = f.x by A5,Def4; end; assume that A6: x in dom f and A7: y = f.x; A8: [x,y] in f by A6,A7,Def4; hence y in rng f by RELAT_1:def 5; then A9: y in dom g by A2,RELAT_1:37; [y,x] in g by A2,A8,RELAT_1:def 7; hence x = g.y by A9,Def4; end; assume that A10: dom g = rng f and A11: for y,x holds y in rng f & x = g.y iff x in dom f & y = f.x; let a,b be set; thus [a,b] in g implies [a,b] in f" proof assume A12: [a,b] in g; then a in dom g by RELAT_1:def 4; then a in rng f & b = g.a by A10,A12,Def4; then b in dom f & a = f.b by A11; then [b,a] in f by Def4; then [a,b] in f~ by RELAT_1:def 7; hence [a,b] in f" by A1,Def9; end; assume [a,b] in f"; then [a,b] in f~ by A1,Def9; then A13: [b,a] in f by RELAT_1:def 7; then A14: b in dom f by RELAT_1:def 4; then a = f.b by A13,Def4; then a in rng f & b = g.a by A11,A14; hence [a,b] in g by A10,Def4; end; theorem Th55: f is one-to-one implies rng f = dom(f") & dom f = rng(f") proof assume f is one-to-one; then f" = f~ by Def9; hence thesis by RELAT_1:37; end; theorem Th56: f is one-to-one & x in dom f implies x = (f").(f.x) & x = (f"*f).x proof assume A1: f is one-to-one; assume A2: x in dom f; hence x = (f").(f.x) by A1,Th54; hence thesis by A2,Th23; end; theorem Th57: f is one-to-one & y in rng f implies y = f.((f").y) & y = (f*f").y proof assume A1: f is one-to-one; assume A2: y in rng f; hence A3: y = f.((f").y) by A1,Th54; rng f = dom(f") & dom f = rng(f") by A1,Th55; hence thesis by A2,A3,Th23; end; theorem Th58: f is one-to-one implies dom(f"*f) = dom f & rng(f"*f) = dom f proof assume A1: f is one-to-one; then A2: rng f = dom(f") by Th55; then rng(f"*f) = rng(f") by RELAT_1:47; hence thesis by A1,A2,Th55,RELAT_1:46; end; theorem Th59: f is one-to-one implies dom(f*f") = rng f & rng(f*f") = rng f proof assume A1: f is one-to-one; then A2: rng(f") = dom f by Th55; then dom(f*f") = dom(f") by RELAT_1:46; hence thesis by A1,A2,Th55,RELAT_1:47; end; theorem f is one-to-one & dom f = rng g & rng f = dom g & (for x,y st x in dom f & y in dom g holds f.x = y iff g.y = x) implies g = f" proof assume that A1: f is one-to-one and A2: dom f = rng g and A3: rng f = dom g and A4: for x,y st x in dom f & y in dom g holds f.x = y iff g.y = x; A5: rng f = dom(f") by A1,Th54; y in dom g implies g.y = (f").y proof assume A6: y in dom g; then A7: g.y in dom f by A2,Def5; then f.(g.y) = y by A4,A6; hence thesis by A1,A7,Th54; end; hence g = f" by A3,A5,Th9; end; theorem Th61: f is one-to-one implies f"*f = id dom f & f*f" = id rng f proof assume A1: f is one-to-one; A2: x in dom(f"*f) implies (f"*f).x = x proof assume x in dom(f"*f); then x in dom f by A1,Th58; hence thesis by A1,Th56; end; dom(f"*f) = dom f by A1,Th58; hence f"*f = id dom f by A2,Th34; A3: x in dom(f*f") implies (f*f").x = x proof assume x in dom(f*f"); then x in rng f by A1,Th59; hence thesis by A1,Th57; end; dom(f*f") = rng f by A1,Th59; hence thesis by A3,Th34; end; theorem Th62: f is one-to-one implies f" is one-to-one proof assume A1: f is one-to-one; let y1,y2; assume y1 in dom(f") & y2 in dom(f"); then y1 in rng f & y2 in rng f by A1,Th54; then y1 = f.((f").y1) & y2 = f.((f").y2) by A1,Th57; hence thesis; end; Lm1: rng(g2) = X & f*g2 = id dom g1 & g1*f = id X implies g1 = g2 proof assume that A1: rng(g2) = X and A2: f*g2 = id dom g1 and A3: g1*f = id X; g1*(f*g2) = (g1*f)*g2 & g1*(id dom g1) = g1 & (id X)*g2 = g2 by A1,RELAT_1:55,77,79; hence thesis by A2,A3; end; theorem Th63: f is one-to-one & rng f = dom g & g*f = id dom f implies g = f" proof assume that A1: f is one-to-one and A2: rng f = dom g and A3: g*f = id dom f; f*f" = id rng f & rng(f") = dom f by A1,Th55,Th61; hence thesis by A2,A3,Lm1; end; theorem f is one-to-one & rng g = dom f & f*g = id rng f implies g = f" proof assume that A1: f is one-to-one and A2: rng g = dom f and A3: f*g = id rng f; f"*f = id dom f & dom(f") = rng f by A1,Th55,Th61; hence g = f" by A2,A3,Lm1; end; theorem f is one-to-one implies (f")" = f proof assume A1: f is one-to-one; then A2: dom f = rng(f") & rng f = dom(f") by Th55; then f" is one-to-one & f*f" = id dom(f") & f"*f = id rng(f") by A1,Th61,Th62; hence thesis by A2,Th63; end; theorem f is one-to-one & g is one-to-one implies (g*f)" = f"*g" proof assume that A1: f is one-to-one and A2: g is one-to-one; A3: g*f is one-to-one by A1,A2,Th46; y in rng(g*f) iff y in dom(f"*g") proof thus y in rng(g*f) implies y in dom(f"*g") proof assume y in rng(g*f); then consider x such that A4: x in dom(g*f) and A5: y = (g*f).x by Def5; A6: x in dom f & f.x in dom g & y = g.(f.x) by A4,A5,Th21,Th22; then y in rng g by Def5; then A7: y in dom(g") by A2,Th54; (g").(g.(f.x)) = (g"*g).(f.x) by A6,Th23 .= (id dom g).(f.x) by A2,Th61 .= f.x by A6,Th34; then (g").y in rng f by A6,Def5; then (g").y in dom(f") by A1,Th54; hence thesis by A7,Th21; end; assume y in dom(f"*g"); then A8: y in dom(g") & (g").y in dom(f") by Th21; then y in rng g by A2,Th54; then consider z such that A9: z in dom g and A10: y = g.z by Def5; (g").(g.z) in rng f & g.z in dom(g") by A1,A8,A10,Th54; then (g"*g).z in rng f by A9,Th23; then (id dom g).z in rng f by A2,Th61; then z in rng f by A9,Th34; then consider x such that A11: x in dom f and A12: z = f.x by Def5; x in dom(g*f) & y = (g*f).x by A9,A10,A11,A12,Th21,Th23; hence thesis by Def5; end; then A13: rng(g*f) = dom(f"*g") by TARSKI:2; x in dom((f"*g")*(g*f)) iff x in dom(g*f) proof thus x in dom((f"*g")*(g*f)) implies x in dom(g*f) by Th21; assume A14: x in dom(g*f); then (g*f).x in rng(g*f) by Def5; hence thesis by A13,A14,Th21; end; then A15: dom((f"*g")*(g*f)) = dom(g*f) by TARSKI:2; x in dom(g*f) implies ((f"*g")*(g*f)).x = x proof assume A16: x in dom(g*f); then A17: f.x in dom g by Th21; A18: x in dom f by A16,Th21; (g*f).x in rng(g*f) by A16,Def5; then A19: g.(f.x) in dom(f"*g") by A13,A16,Th22; thus ((f"*g")*(g*f)).x = (f"*g").((g*f).x) by A15,A16,Th22 .= (f"*g").(g.(f.x)) by A16,Th22 .= (f").((g").(g.(f.x))) by A19,Th22 .= (f").((g"*g).(f.x)) by A17,Th23 .= (f").((id dom g).(f.x)) by A2,Th61 .= (f").(f.x) by A17,Th34 .= x by A1,A18,Th56; end; then (f"*g")*(g*f) = id dom(g*f) by A15,Th34; hence thesis by A3,A13,Th63; end; theorem (id X)" = (id X) proof A1: id X is one-to-one by Th52; dom id X = X by RELAT_1:71; then (id X)"*(id X) = id X & dom((id X)") = rng id X & rng id X = X by A1,Th55,Th61,RELAT_1:71; hence thesis by Th44; end; definition let f,X; cluster f|X -> Function-like; coherence proof let x,y1,y2; assume [x,y1] in f|X & [x,y2] in f|X; then [x,y1] in f & [x,y2] in f by RELAT_1:def 11; hence y1 = y2 by Def1; end; end; theorem Th68: g = f|X iff dom g = dom f /\ X & for x st x in dom g holds g.x = f.x proof hereby assume A1: g = f|X; hence A2: dom g = dom f /\ X by RELAT_1:90; A3: g c= f by A1,RELAT_1:88; let x; assume A4: x in dom g; then A5: [x,g.x] in g by Def4; x in dom f by A2,A4,XBOOLE_0:def 3; hence g.x = f.x by A3,A5,Def4; end; assume that A6: dom g = dom f /\ X and A7: for x st x in dom g holds g.x = f.x; now let x,y; hereby assume A8: [x,y] in g; then A9: x in dom g by RELAT_1:def 4; hence x in X by A6,XBOOLE_0:def 3; A10: x in dom f by A6,A9,XBOOLE_0:def 3; y = g.x by A8,A9,Def4 .= f.x by A7,A9; hence [x,y] in f by A10,Def4; end; assume A11: x in X; assume A12: [x,y] in f; then A13: x in dom f by RELAT_1:def 4; then A14: x in dom g by A6,A11,XBOOLE_0:def 3; y = f.x by A12,A13,Def4 .= g.x by A7,A14; hence [x,y] in g by A14,Def4; end; hence g = f|X by RELAT_1:def 11; end; canceled; theorem x in dom(f|X) implies (f|X).x = f.x by Th68; theorem x in dom f /\ X implies (f|X).x = f.x proof assume x in dom f /\ X; then x in dom(f|X) by Th68; hence thesis by Th68; end; Lm2: x in dom(f|X) iff x in dom f & x in X proof dom(f|X) = dom f /\ X by Th68; hence thesis by XBOOLE_0:def 3; end; theorem Th72: x in X implies (f|X).x = f.x proof assume A1: x in X; per cases; suppose x in dom f; then x in dom(f|X) by A1,Lm2; hence thesis by Th68; suppose A2: not x in dom f; then not x in dom(f|X) by Lm2; hence (f|X).x = {} by Def4 .= f.x by A2,Def4; end; theorem x in dom f & x in X implies f.x in rng(f|X) proof assume A1: x in dom f & x in X; then x in dom f /\ X by XBOOLE_0:def 3; then x in dom(f|X) & (f|X).x = f.x by A1,Th68,Th72; hence thesis by Def5; end; canceled 2; theorem dom(f|X) c= dom f & rng(f|X) c= rng f by RELAT_1:89,99; canceled 5; theorem X c= Y implies (f|X)|Y = f|X & (f|Y)|X = f|X by RELAT_1:102,103; canceled; theorem f is one-to-one implies f|X is one-to-one proof assume A1: f is one-to-one; let x1,x2; assume A2: x1 in dom(f|X) & x2 in dom(f|X); then x1 in dom f /\ X & x2 in dom f /\ X by Th68; then x1 in dom f & x2 in dom f & (f|X).x1 = f.x1 & (f|X).x2 = f.x2 by A2,Th68,XBOOLE_0:def 3; hence thesis by A1,Def8; end; definition let Y,f; cluster Y|f -> Function-like; coherence proof let x,y1,y2; assume [x,y1] in Y|f & [x,y2] in Y|f; then [x,y1] in f & [x,y2] in f by RELAT_1:def 12; hence y1 = y2 by Def1; end; end; theorem Th85: g = Y|f iff (for x holds x in dom g iff x in dom f & f.x in Y) & (for x st x in dom g holds g.x = f.x) proof hereby assume A1: g = Y|f; hereby let x; hereby assume x in dom g; then A2: [x,g.x] in g by Def4; then A3: [x,g.x] in f by A1,RELAT_1:def 12; hence x in dom f by RELAT_1:def 4; then f.x = g.x by A3,Def4; hence f.x in Y by A1,A2,RELAT_1:def 12; end; assume x in dom f; then A4: [x,f.x] in f by Def4; assume f.x in Y; then [x,f.x] in g by A1,A4,RELAT_1:def 12; hence x in dom g by RELAT_1:def 4; end; let x; assume x in dom g; then [x,g.x] in g by Def4; then A5: [x,g.x] in f by A1,RELAT_1:def 12; then x in dom f by RELAT_1:def 4; hence f.x = g.x by A5,Def4; end; assume that A6: for x holds x in dom g iff x in dom f & f.x in Y and A7: for x st x in dom g holds g.x = f.x; now let x,y; hereby assume A8: [x,y] in g; then A9: x in dom g by RELAT_1:def 4; then A10: y = g.x by A8,Def4 .= f.x by A7,A9; hence y in Y by A6,A9; x in dom f by A6,A9; hence [x,y] in f by A10,Def4; end; assume A11: y in Y; assume A12: [x,y] in f; then A13: y = f.x by Th8; x in dom f by A12,RELAT_1:def 4; then A14: x in dom g by A6,A11,A13; then y = g.x by A7,A13; hence [x,y] in g by A14,Def4; end; hence g = Y|f by RELAT_1:def 12; end; theorem x in dom(Y|f) iff x in dom f & f.x in Y by Th85; theorem x in dom(Y|f) implies (Y|f).x = f.x by Th85; canceled; theorem dom(Y|f) c= dom f & rng(Y|f) c= rng f proof thus dom(Y|f) c= dom f proof let x; thus thesis by Th85; end; thus thesis by RELAT_1:118; end; canceled 7; theorem X c= Y implies Y|(X|f) = X|f & X|(Y|f) = X|f by RELAT_1:129,130; canceled; theorem f is one-to-one implies Y|f is one-to-one proof assume A1: f is one-to-one; let x1,x2 such that A2: x1 in dom(Y|f) & x2 in dom(Y|f) and A3: (Y|f).x1 = (Y|f).x2; (Y|f).x1 = f.x1 & (Y|f).x2 = f.x2 & x1 in dom f & x2 in dom f by A2,Th85; hence thesis by A1,A3,Def8; end; definition let f,X; redefine canceled 2; func f.:X means :Def12: for y holds y in it iff ex x st x in dom f & x in X & y = f.x; compatibility proof let Y; hereby assume A1: Y = f.:X; let y; hereby assume y in Y; then consider x such that A2: [x,y] in f and A3: x in X by A1,RELAT_1:def 13; take x; thus A4: x in dom f by A2,RELAT_1:def 4; thus x in X by A3; thus y = f.x by A2,A4,Def4; end; given x such that A5: x in dom f and A6: x in X and A7: y = f.x; [x,y] in f by A5,A7,Def4; hence y in Y by A1,A6,RELAT_1:def 13; end; assume A8: for y holds y in Y iff ex x st x in dom f & x in X & y = f.x; now let y; hereby assume y in Y; then consider x such that A9: x in dom f and A10: x in X and A11: y = f.x by A8; take x; thus [x,y] in f by A9,A11,Def4; thus x in X by A10; end; given x such that A12: [x,y] in f and A13: x in X; A14: x in dom f by A12,RELAT_1:def 4; y = f.x by A12,Th8; hence y in Y by A8,A13,A14; end; hence Y = f.:X by RELAT_1:def 13; end; end; canceled 17; theorem Th117: x in dom f implies f.:{x} = {f.x} proof assume A1: x in dom f; y in f.:{x} iff y in {f.x} proof thus y in f.:{x} implies y in {f.x} proof assume y in f.:{x}; then consider z such that z in dom f and A2: z in {x} and A3: y = f.z by Def12; z = x by A2,TARSKI:def 1; hence thesis by A3,TARSKI:def 1; end; assume y in {f.x}; then y = f.x & x in {x} by TARSKI:def 1; hence y in f.:{x} by A1,Def12; end; hence thesis by TARSKI:2; end; theorem x1 in dom f & x2 in dom f implies f.:{x1,x2} = {f.x1,f.x2} proof assume A1: x1 in dom f & x2 in dom f; y in f.:{x1,x2} iff y = f.x1 or y = f.x2 proof thus y in f.:{x1,x2} implies y = f.x1 or y = f.x2 proof assume y in f.:{x1,x2}; then ex x st x in dom f & x in {x1,x2} & y = f.x by Def12; hence y = f.x1 or y = f.x2 by TARSKI:def 2; end; assume A2: y = f.x1 or y = f.x2; x1 in {x1,x2} & x2 in {x1,x2} by TARSKI:def 2; hence thesis by A1,A2,Def12; end; hence thesis by TARSKI:def 2; end; canceled; theorem (Y|f).:X c= f.:X proof let y; assume y in (Y|f).:X; then consider x such that A1: x in dom(Y|f) and A2: x in X and A3: y = (Y|f).x by Def12; y = f.x & x in dom f by A1,A3,Th85; hence y in f.:X by A2,Def12; end; theorem Th121: f is one-to-one implies f.:(X1 /\ X2) = f.:X1 /\ f.:X2 proof assume A1: f is one-to-one; A2: f.:(X1 /\ X2)c=f.:X1 /\ f.:X2 by RELAT_1:154; f.:X1 /\ f.:X2 c= f.:(X1 /\ X2) proof let y; assume y in f.:X1 /\ f.:X2; then A3: y in f.:X1 & y in f.:X2 by XBOOLE_0:def 3; then consider x1 such that A4: x1 in dom f and A5: x1 in X1 and A6: y = f.x1 by Def12; consider x2 such that A7: x2 in dom f and A8: x2 in X2 and A9: y = f.x2 by A3,Def12; x1 = x2 by A1,A4,A6,A7,A9,Def8; then x1 in X1 /\ X2 by A5,A8,XBOOLE_0:def 3; hence thesis by A4,A6,Def12; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem (for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2) implies f is one-to-one proof assume A1: for X1,X2 holds f.:(X1 /\ X2) = f.:X1 /\ f.:X2; given x1,x2 such that A2: x1 in dom f & x2 in dom f and A3: f.x1 = f.x2 and A4: x1 <> x2; A5: f.:{x1} = {f.x1} & f.:{x2} = {f.x2} & {x1} misses {x2} by A2,A4,Th117,ZFMISC_1:17; then {x1} /\ {x2} = {} by XBOOLE_0:def 7; then f.:({x1}/\{x2}) = {} & f.x1 in f.:{x1} & f.:({x1}/\{x2}) = f.:{x1}/\f.: {x2} & f.:{x1} /\ f.:{x2} = f.:{x1} by A1,A3,A5,RELAT_1:149,TARSKI:def 1; hence contradiction; end; theorem f is one-to-one implies f.:(X1 \ X2) = f.:X1 \ f.:X2 proof assume A1: f is one-to-one; A2: f.:X1 \ f.: X2 c= f.:(X1 \ X2) by RELAT_1:155; f.:(X1 \ X2) c= f.:X1 \ f.:X2 proof let y; assume y in f.:(X1\X2); then consider x such that A3: x in dom f and A4: x in X1\X2 and A5: y = f.x by Def12; A6: x in X1 & not x in X2 by A4,XBOOLE_0:def 4; then A7: y in f.:X1 by A3,A5,Def12; now assume y in f.:X2; then ex z st z in dom f & z in X2 & y = f.z by Def12; hence contradiction by A1,A3,A5,A6,Def8; end; hence thesis by A7,XBOOLE_0:def 4; end; hence thesis by A2,XBOOLE_0:def 10; end; theorem (for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2) implies f is one-to-one proof assume A1: for X1,X2 holds f.:(X1 \ X2) = f.:X1 \ f.:X2; given x1,x2 such that A2: x1 in dom f & x2 in dom f and A3: f.x1 = f.x2 and A4: x1 <> x2; f.:{x1} = {f.x1} & f.:{x2} = {f.x2} & {x1} \ {x2} = {x1} by A2,A4,Th117,ZFMISC_1:20; then f.:({x1}\{x2}) = f.:{x1} & f.x1 in f.:{x1} & f.:({x1}\{x2}) = f.:{x1}\f.:{x2} & f.:{x1} \ f.:{x2} = {} by A1,A3,TARSKI:def 1,XBOOLE_1:37; hence contradiction; end; theorem X misses Y & f is one-to-one implies f.:X misses f.:Y proof assume X /\ Y = {} & f is one-to-one; then f.:(X /\ Y) = {} & f.:(X /\ Y) = f.:X /\ f.:Y by Th121,RELAT_1:149; hence thesis by XBOOLE_0:def 7; end; theorem (Y|f).:X = Y /\ f.:X proof y in (Y|f).:X iff y in Y /\ f.:X proof thus y in (Y|f).:X implies y in Y /\ f.:X proof assume y in (Y|f).:X; then consider x such that A1: x in dom(Y|f) and A2: x in X and A3: y = (Y|f).x by Def12; y = f.x & x in dom f by A1,A3,Th85; then y in f.:X & y in Y by A1,A2,Def12,Th85; hence thesis by XBOOLE_0:def 3; end; assume A4: y in Y /\ f.:X; then y in f.:X by XBOOLE_0:def 3; then consider x such that A5: x in dom f and A6: x in X and A7: y = f.x by Def12; y in Y by A4,XBOOLE_0:def 3; then A8: x in dom(Y|f) by A5,A7,Th85; then (Y|f).x = f.x by Th85; hence thesis by A6,A7,A8,Def12; end; hence thesis by TARSKI:2; end; definition let f,Y; redefine func f"Y means :Def13: for x holds x in it iff x in dom f & f.x in Y; compatibility proof let X; hereby assume A1: X = f"Y; let x; hereby assume x in X; then consider y such that A2: [x,y] in f and A3: y in Y by A1,RELAT_1:def 14; thus x in dom f by A2,RELAT_1:def 4; thus f.x in Y by A2,A3,Th8; end; assume that A4: x in dom f and A5: f.x in Y; [x,f.x] in f by A4,Th8; hence x in X by A1,A5,RELAT_1:def 14; end; assume A6: for x holds x in X iff x in dom f & f.x in Y; now let x; hereby assume A7: x in X; take y = f.x; x in dom f by A6,A7; hence [x,y] in f by Def4; thus y in Y by A6,A7; end; given y such that A8: [x,y] in f and A9: y in Y; A10: x in dom f by A8,RELAT_1:def 4; y = f.x by A8,Th8; hence x in X by A6,A9,A10; end; hence X = f"Y by RELAT_1:def 14; end; end; canceled 10; theorem f"(Y1 /\ Y2) = f"Y1 /\ f"Y2 proof x in f"(Y1 /\ Y2) iff x in f"Y1 /\ f"Y2 proof (x in f"Y1 iff f.x in Y1 & x in dom f) & (x in f"Y2 iff f.x in Y2 & x in dom f) & (x in f"(Y1 /\ Y2) iff f.x in Y1 /\ Y2 & x in dom f) & (x in f"Y1 /\ f"Y2 iff x in f"Y1 & x in f"Y2) & (f.x in Y1 /\ Y2 iff f.x in Y1 & f.x in Y2) by Def13,XBOOLE_0:def 3; hence thesis; end; hence thesis by TARSKI:2; end; theorem f"(Y1 \ Y2) = f"Y1 \ f"Y2 proof x in f"(Y1 \ Y2) iff x in f"Y1 \ f"Y2 proof (x in f"Y1 iff f.x in Y1 & x in dom f) & (x in f"Y2 iff f.x in Y2 & x in dom f) & (x in f"(Y1 \ Y2) iff f.x in Y1 \ Y2 & x in dom f) & (x in f"Y1 \ f"Y2 iff x in f"Y1 & not x in f"Y2) & (f.x in Y1 \ Y2 iff f.x in Y1 & not f.x in Y2) by Def13,XBOOLE_0:def 4; hence thesis; end; hence thesis by TARSKI:2; end; theorem (R|X)"Y = X /\ (R"Y) proof hereby let x; assume x in (R|X)"Y; then consider y such that A1: [x,y] in R|X and A2: y in Y by RELAT_1:def 14; R|X c= R by RELAT_1:88; then A3: x in R"Y by A1,A2,RELAT_1:def 14; x in X by A1,RELAT_1:def 11; hence x in X /\ (R"Y) by A3,XBOOLE_0:def 3; end; let x; assume A4: x in X /\ (R"Y); then A5: x in X by XBOOLE_0:def 3; x in R"Y by A4,XBOOLE_0:def 3; then consider y such that A6: [x,y] in R and A7: y in Y by RELAT_1:def 14; [x,y] in R|X by A5,A6,RELAT_1:def 11; hence x in (R|X)"Y by A7,RELAT_1:def 14; end; canceled 2; theorem Th142: y in rng R iff R"{y} <> {} proof thus y in rng R implies R"{y} <> {} proof assume y in rng R; then consider x such that A1: [x,y] in R by RELAT_1:def 5; y in {y} by TARSKI:def 1; hence R"{y} <> {} by A1,RELAT_1:def 14; end; assume R"{y} <> {}; then consider x such that A2: x in R"{y} by XBOOLE_0:def 1; consider z such that A3: [x,z] in R and A4: z in {y} by A2,RELAT_1:def 14; z = y by A4,TARSKI:def 1; hence y in rng R by A3,RELAT_1:def 5; end; theorem (for y st y in Y holds R"{y} <> {}) implies Y c= rng R proof assume A1: for y st y in Y holds R"{y} <> {}; let y; assume y in Y; then R"{y} <> {} by A1; hence y in rng R by Th142; end; theorem Th144: (for y st y in rng f ex x st f"{y} = {x}) iff f is one-to-one proof thus (for y st y in rng f ex x st f"{y} = {x}) implies f is one-to-one proof assume A1: for y st y in rng f ex x st f"{y} = {x}; let x1,x2; assume A2: x1 in dom f & x2 in dom f; then A3: f.x1 in rng f & f.x2 in rng f by Def5; then consider y1 such that A4: f"{f.x1} = {y1} by A1; consider y2 such that A5: f"{f.x2} = {y2} by A1,A3; f.x1 in {f.x1} & f.x2 in {f.x2} by TARSKI:def 1; then x1 in {y1} & x2 in {y2} by A2,A4,A5,Def13; then y1 = x1 & y2 = x2 by TARSKI:def 1; hence thesis by A4,A5,ZFMISC_1:6; end; assume A6: f is one-to-one; let y; assume y in rng f; then consider x such that A7: x in dom f and A8: y = f.x by Def5; take x; z in f"{y} iff z = x proof thus z in f"{y} implies z = x proof assume z in f"{y}; then z in dom f & f.z in {y} by Def13; then z in dom f & f.z = y by TARSKI:def 1; hence thesis by A6,A7,A8,Def8; end; y in {y} by TARSKI:def 1; hence thesis by A7,A8,Def13; end; hence thesis by TARSKI:def 1; end; theorem Th145: f.:(f"Y) c= Y proof let y; assume y in f.:(f"Y); then ex x st x in dom f & x in f"Y & y = f.x by Def12; hence y in Y by Def13; end; theorem X c= dom R implies X c= R"(R.:X) proof assume A1:X c= dom R; let x; assume A2: x in X; then consider Rx being set such that A3: [x,Rx] in R by A1,RELAT_1:def 4; Rx in R.:X by A2,A3,RELAT_1:def 13; hence x in R"(R.:X) by A3,RELAT_1:def 14; end; theorem Y c= rng f implies f.:(f"Y) = Y proof assume A1: Y c= rng f; thus f.:(f"Y) c= Y by Th145; let y; assume A2: y in Y; then consider x such that A3: x in dom f & y = f.x by A1,Def5; x in f"Y by A2,A3,Def13; hence y in f.:(f"Y) by A3,Def12; end; theorem f.:(f"Y) = Y /\ f.:(dom f) proof f.:(f"Y) c= Y & f.:(f"(Y)) c= f.:(dom f) by Th145,RELAT_1:147; hence f.:(f"Y) c= Y /\ f.:(dom f) by XBOOLE_1:19; let y; assume A1: y in Y /\ f.:(dom f); then y in f.:(dom f) by XBOOLE_0:def 3; then consider x such that A2: x in dom f and x in dom f and A3: y = f.x by Def12; y in Y by A1,XBOOLE_0:def 3; then x in f"Y by A2,A3,Def13; hence y in f.:(f"Y) by A2,A3,Def12; end; theorem Th149: f.:(X /\ f"Y) c= (f.:X) /\ Y proof let y; assume y in f.:(X /\ f"Y); then consider x such that A1: x in dom f and A2: x in X /\ f"Y and A3: y = f.x by Def12; x in X & x in f"Y by A2,XBOOLE_0:def 3; then y in f.:X & y in Y by A1,A3,Def12,Def13; hence y in (f.:X) /\ Y by XBOOLE_0:def 3; end; theorem f.:(X /\ f"Y) = (f.:X) /\ Y proof thus f.:(X /\ f"Y)c=(f.:X) /\ Y by Th149; let y; assume y in (f.:X) /\ Y; then A1: y in f.:X & y in Y by XBOOLE_0:def 3; then consider x such that A2: x in dom f and A3: x in X and A4: y = f.x by Def12; x in f"Y by A1,A2,A4,Def13; then x in X /\ f"Y by A3,XBOOLE_0:def 3; hence y in f.:(X /\ f"Y) by A2,A4,Def12; end; theorem X /\ R"Y c= R"(R.:X /\ Y) proof let x; assume A1: x in X /\ R"Y; then A2: x in X by XBOOLE_0:def 3; x in R"Y by A1,XBOOLE_0:def 3; then consider Rx being set such that A3: [x,Rx] in R and A4: Rx in Y by RELAT_1:def 14; Rx in R.:X by A2,A3,RELAT_1:def 13; then Rx in R.:X /\ Y by A4,XBOOLE_0:def 3; hence thesis by A3,RELAT_1:def 14; end; theorem f is one-to-one implies f"(f.:X) c= X proof assume A1: f is one-to-one; let x; assume x in f"(f.:X); then A2: f.x in f.:X & x in dom f by Def13; then ex z st z in dom f & z in X & f.x = f.z by Def12; hence thesis by A1,A2,Def8; end; theorem (for X holds f"(f.:X) c= X) implies f is one-to-one proof assume A1: for X holds f"(f.:X) c= X; given x1,x2 such that A2: x1 in dom f & x2 in dom f and A3: f.x1 = f.x2 and A4: x1 <> x2; A5: f.:{x1} = {f.x1} & f.:{x2} = {f.x2} by A2,Th117; then f.:{x1} <> {} & f.:{x2} <> {} & f.x1 in rng f & f.x2 in rng f by A2,Def5; then f"(f.:{x1}) <> {} & f"(f.:{x2}) <> {} & f"(f.:{x1}) c= {x1} & f"(f.:{x2}) c= {x2} by A1,A5,Th142; then f"(f.:{x1}) = {x1} & f"(f.:{x2}) = {x2} by ZFMISC_1:39; hence contradiction by A3,A4,A5,ZFMISC_1:6; end; theorem f is one-to-one implies f.:X = (f")"X proof assume A1: f is one-to-one; y in f.:X iff y in (f")"X proof thus y in f.:X implies y in (f")"X proof assume y in f.:X; then consider x such that A2: x in dom f and A3: x in X and A4: y = f.x by Def12; y in rng f by A2,A4,Def5; then y in dom(f") & (f").(f.x) = x by A1,A2,Th54; hence y in (f")"X by A3,A4,Def13; end; assume y in (f")"X; then A5: y in dom(f") & (f").y in X by Def13; then y in rng(f) by A1,Th54; then consider x such that A6: x in dom(f) and A7: y = f.x by Def5; (f").y = x by A1,A6,A7,Th56; hence y in f.:X by A5,A6,A7,Def12; end; hence thesis by TARSKI:2; end; theorem f is one-to-one implies f"Y = (f").:Y proof assume A1: f is one-to-one; x in f"Y iff x in (f").:Y proof thus x in f"Y implies x in (f").:Y proof assume x in f"Y; then x in dom f & f.x in Y by Def13; then x in dom f & f.x in rng(f) & f.x in Y by Def5; then (f").(f.x) = x & f.x in dom(f") & f.x in Y by A1,Th54; hence x in (f").:Y by Def12; end; assume x in (f").:Y; then consider y such that A2: y in dom(f") and A3: y in Y and A4: x = (f").y by Def12; dom(f") = rng f by A1,Th54; then y = f.x & x in dom f by A1,A2,A4,Th54; hence x in f"Y by A3,Def13; end; hence thesis by TARSKI:2; end; :: SUPLEMENT theorem Y = rng f & dom g = Y & dom h = Y & g*f = h*f implies g = h proof assume that A1: Y = rng f and A2: dom g = Y and A3: dom h = Y and A4: g*f = h*f; y in Y implies g.y = h.y proof assume y in Y; then consider x such that A5: x in dom f and A6: y = f.x by A1,Def5; (g*f).x = g.y & (h*f).x = h.y by A5,A6,Th23; hence thesis by A4; end; hence thesis by A2,A3,Th9; end; theorem f.:X1 c= f.:X2 & X1 c= dom f & f is one-to-one implies X1 c= X2 proof assume that A1: f.:X1 c= f.:X2 and A2: X1 c= dom f and A3: f is one-to-one; let x; assume A4: x in X1; then f.x in f.:X1 by A2,Def12; then ex x2 st x2 in dom f & x2 in X2 & f.x = f.x2 by A1,Def12; hence thesis by A2,A3,A4,Def8; end; theorem f"Y1 c= f"Y2 & Y1 c= rng f implies Y1 c= Y2 proof assume that A1: f"Y1 c= f"Y2 and A2: Y1 c= rng f; let y; assume A3: y in Y1; then consider x such that A4: x in dom f and A5: y = f.x by A2,Def5; x in f"Y1 by A3,A4,A5,Def13; hence thesis by A1,A5,Def13; end; theorem f is one-to-one iff for y ex x st f"{y} c= {x} proof (for y ex x st f"{y} c= {x}) iff (for y st y in rng f ex x st f"{y} = {x}) proof thus (for y ex x st f"{y} c= {x}) implies (for y st y in rng f ex x st f"{y} = {x}) proof assume A1: for y ex x st f"{y} c= {x}; let y; assume A2: y in rng f; consider x such that A3: f"{y} c= {x} by A1; take x; consider x1 such that A4: x1 in dom f and A5: y = f.x1 by A2,Def5; f.x1 in {y} by A5,TARSKI:def 1; then f"{y} <> {} by A4,Def13; hence thesis by A3,ZFMISC_1:39; end; assume A6: for y st y in rng f ex x st f"{y} = {x}; let y; A7: now assume y in rng f; then consider x such that A8: f"{y} = {x} by A6; take x; thus f"{y} c= {x} by A8; end; now assume A9: not y in rng f; consider x; take x; rng f misses {y} by A9,ZFMISC_1:56; then f"{y} = {} by RELAT_1:173; hence f"{y} c= {x} by XBOOLE_1:2; end; hence thesis by A7; end; hence thesis by Th144; end; theorem rng R c= dom S implies R"X c= (R*S)"(S.:X) proof assume A1: rng R c= dom S; let x; assume x in R"X; then consider Rx being set such that A2: [x,Rx] in R and A3: Rx in X by RELAT_1:def 14; Rx in rng R by A2,RELAT_1:def 5; then consider SRx being set such that A4: [Rx,SRx] in S by A1,RELAT_1:def 4; A5: SRx in S.:X by A3,A4,RELAT_1:def 13; [x,SRx] in R*S by A2,A4,RELAT_1:def 8; hence thesis by A5,RELAT_1:def 14; end;

Back to top