Copyright (c) 1989 Association of Mizar Users
environ
vocabulary FUNCT_1, RELAT_1, BOOLE;
notation TARSKI, XBOOLE_0, RELAT_1, FUNCT_1;
constructors TARSKI, SUBSET_1, FUNCT_1, XBOOLE_0;
clusters FUNCT_1, XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;
definitions TARSKI, FUNCT_1, RELAT_1, XBOOLE_0;
theorems TARSKI, XBOOLE_0, ZFMISC_1, FUNCT_1, RELAT_1, XBOOLE_1;
begin
reserve X,Y,p,x,x1,x2,y,y1,y2,z,z1,z2 for set;
reserve f,g,h for Function;
canceled 5;
theorem Th6:
for G being set st G c= f holds G is Function
proof let G be set such that
A1: p in G implies p in f;
now
thus p in G implies ex x,y st [x,y] = p
proof assume p in G; then p in f by A1;
hence thesis by RELAT_1:def 1;
end;
let x,y1,y2;
assume [x,y1] in G & [x,y2] in G;
then [x,y1] in f & [x,y2] in f by A1;
hence y1 = y2 by FUNCT_1:def 1;
end;
hence thesis by FUNCT_1:2;
end;
canceled;
theorem
f c= g iff
dom f c= dom g & (for x st x in dom f holds f.x = g.x)
proof
thus f c= g implies
dom f c= dom g & (for x st x in dom f holds f.x = g.x)
proof assume
A1: f c= g;
hence dom f c= dom g by RELAT_1:25;
let x;
assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 4;
hence thesis by A1,FUNCT_1:8;
end;
assume that
A2: dom f c= dom g and
A3: (for x st x in dom f holds f.x = g.x);
let x,y;
assume [x,y] in f;
then y = f.x & x in dom f by FUNCT_1:8;
then y = g.x & x in dom g by A2,A3;
hence [x,y] in g by FUNCT_1:def 4;
end;
theorem
dom f = dom g & f c= g implies f = g
proof assume that
A1: dom f = dom g and
A2: f c= g;
[x,y] in f iff [x,y] in g
proof thus [x,y] in f implies [x,y] in g by A2;
assume
A3: [x,y] in g;
then x in dom f by A1,RELAT_1:def 4;
then [x,f.x] in f by FUNCT_1:8;
hence thesis by A2,A3,FUNCT_1:def 1;
end;
hence f = g by RELAT_1:def 2;
end;
Lm1:
rng f /\ rng h = {} & x in dom f & y in dom h implies f.x <> h.y
proof assume
A1: rng f /\ rng h = {};
assume x in dom f & y in dom h;
then f.x in rng f & h.y in rng h by FUNCT_1:def 5;
hence thesis by A1,XBOOLE_0:def 3;
end;
canceled 2;
theorem
[x,z] in (g*f) implies [x,f.x] in f & [f.x,z] in g
proof assume [x,z] in (g*f);
then ex y st [x,y] in f & [y,z] in g by RELAT_1:def 8;
hence thesis by FUNCT_1:8;
end;
theorem
h c= f implies g*h c= g*f & h*g c= f*g by RELAT_1:48,49;
canceled;
theorem Th15:
{[x,y]} is Function
proof
now
thus p in {[x,y]} implies ex x,y st [x,y] = p
proof assume p in {[x,y]};
then p = [x,y] by TARSKI:def 1;
hence thesis;
end;
let z,y1,y2;
assume [z,y1] in {[x,y]} & [z,y2] in {[x,y]};
then [z,y1] = [x,y] & [z,y2] = [x,y] by TARSKI:def 1;
hence y1 = y2 by ZFMISC_1:33;
end;
hence thesis by FUNCT_1:2;
end;
Lm2:
[x,y] in {[x1,y1]} implies x = x1 & y = y1
proof assume [x,y] in {[x1,y1]};
then [x,y] = [x1,y1] by TARSKI:def 1;
hence x = x1 & y = y1 by ZFMISC_1:33;
end;
theorem
f = {[x,y]} implies f.x = y
proof assume f = {[x,y]};
then [x,y] in f by TARSKI:def 1;
hence f.x = y by FUNCT_1:8;
end;
canceled;
theorem
dom f = {x} implies f = {[x,f.x]}
proof assume
A1: dom f = {x};
reconsider g = {[x,f.x]} as Function by Th15;
[y,z] in f iff [y,z] in g
proof
thus [y,z] in f implies [y,z] in g
proof assume [y,z] in f;
then y in {x} & z in rng f & rng f = {f.x}
by A1,FUNCT_1:14,RELAT_1:def 4,def 5;
then y = x & z = f.x by TARSKI:def 1;
hence [y,z] in g by TARSKI:def 1;
end;
assume [y,z] in g;
then y = x & z = f.x & x in dom f by A1,Lm2,TARSKI:def 1;
hence [y,z] in f by FUNCT_1:def 4;
end;
hence thesis by RELAT_1:def 2;
end;
theorem
{[x1,y1],[x2,y2]} is Function iff (x1 = x2 implies y1 = y2)
proof
thus {[x1,y1],[x2,y2]} is Function & x1 = x2 implies y1 = y2
proof assume
A1: {[x1,y1],[x2,y2]} is Function;
[x1,y1] in {[x1,y1],[x2,y2]} & [x2,y2] in
{[x1,y1],[x2,y2]} by TARSKI:def 2;
hence thesis by A1,FUNCT_1:def 1;
end;
assume
A2: x1 = x2 implies y1 = y2;
now
thus p in {[x1,y1],[x2,y2]} implies ex x,y st [x,y] = p
proof assume p in {[x1,y1],[x2,y2]};
then p = [x1,y1] or p = [x2,y2] by TARSKI:def 2;
hence thesis;
end;
let x,z1,z2;
assume A3: [x,z1] in {[x1,y1],[x2,y2]} & [x,z2] in {[x1,y1],[x2,y2]};
A4: [x,z1] = [x1,y1] & [x,z2] = [x1,y1] or [x,z1] = [x2,y2] & [x,z2] = [x2,y2]
implies z1 = y1 & z2 = y1 or z1 = y2 & z2 = y2 by ZFMISC_1:33;
now assume [x,z1] = [x1,y1] & [x,z2] = [x2,y2] or
[x,z1] = [x2,y2] & [x,z2] = [x1,y1];
then x = x1 & x = x2 & (z1 = y1 & z2 = y2 or z1 = y2 & z2 = y1)
by ZFMISC_1:33;
hence z1 = z2 by A2;
end;
hence z1 = z2 by A3,A4,TARSKI:def 2;
end;
hence thesis by FUNCT_1:2;
end;
canceled 5;
theorem Th25:
f is one-to-one iff
for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2
proof
thus f is one-to-one implies
for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2
proof assume
A1: f is one-to-one;
let x1,x2,y;
assume [x1,y] in f & [x2,y] in f;
then x1 in dom f & x2 in dom f & f.x1 = y & f.x2 = y by FUNCT_1:8;
hence thesis by A1,FUNCT_1:def 8;
end;
assume
A2: for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2;
let x1,x2;
assume x1 in dom f & x2 in dom f & f.x1 = f.x2;
then [x1,f.x1] in f & [x2,f.x1] in f by FUNCT_1:8;
hence thesis by A2;
end;
theorem Th26:
g c= f & f is one-to-one implies g is one-to-one
proof assume that
A1: g c= f and
A2: f is one-to-one;
for x1,x2,y st [x1,y] in g & [x2,y] in g holds x1 = x2 by A1,A2,Th25;
hence thesis by Th25;
end;
theorem Th27:
f /\ X is Function & X /\ f is Function
proof f /\ X c= f & X /\ f c= f by XBOOLE_1:17;
hence thesis by Th6;
end;
theorem
h = f /\ g
implies dom h c= dom f /\ dom g & rng h c= rng f /\ rng g
by RELAT_1:14,27;
theorem
h = f /\ g & x in dom h implies h.x = f.x & h.x = g.x
proof assume
A1: h = f /\ g;
set y = h.x;
assume x in dom h;
then [x,y] in h by FUNCT_1:def 4;
then [x,y] in f & [x,y] in g by A1,XBOOLE_0:def 3;
hence thesis by FUNCT_1:8;
end;
theorem
(f is one-to-one or g is one-to-one) & h = f /\ g
implies h is one-to-one
proof f /\ g c= f & f /\ g c= g & f /\ g is Function by Th27,XBOOLE_1:17;
hence thesis by Th26;
end;
theorem
dom f misses dom g implies f \/ g is Function
proof assume
A1: dom f /\ dom g = {};
now
thus p in f \/ g implies ex x,y st [x,y] = p
proof assume p in f \/ g;
then p in f or p in g by XBOOLE_0:def 2;
hence thesis by RELAT_1:def 1;
end;
let x,y1,y2;
A2: not (x in dom f & x in dom g) by A1,XBOOLE_0:def 3;
assume [x,y1] in f \/ g;
then A3: [x,y1] in f or [x,y1] in g by XBOOLE_0:def 2;
assume [x,y2] in f \/ g;
then [x,y2] in f or [x,y2] in g by XBOOLE_0:def 2;
hence y1 = y2 by A2,A3,FUNCT_1:def 1,RELAT_1:def 4;
end;
hence thesis by FUNCT_1:2;
end;
theorem
f c= h & g c= h implies f \/ g is Function
proof assume f c= h & g c= h;
then f \/ g c= h by XBOOLE_1:8;
hence thesis by Th6;
end;
Lm3:
h = f \/ g implies (x in dom h iff x in dom f or x in dom g)
proof assume
A1: h = f \/ g;
thus x in dom h implies x in dom f or x in dom g
proof assume x in dom h;
then [x,h.x] in h by FUNCT_1:def 4;
then [x,h.x] in f or [x,h.x] in g by A1,XBOOLE_0:def 2;
hence thesis by RELAT_1:def 4;
end;
assume x in dom f or x in dom g;
then [x,f.x] in f or [x,g.x] in g by FUNCT_1:def 4;
then [x,f.x] in h or [x,g.x] in h by A1,XBOOLE_0:def 2;
hence x in dom h by RELAT_1:def 4;
end;
theorem
h = f \/ g implies dom h = dom f \/ dom g & rng h = rng f \/ rng g
by RELAT_1:13,26;
theorem Th34:
x in dom f & h = f \/ g implies h.x = f.x
proof assume x in dom f;
then [x,f.x] in f by FUNCT_1:def 4;
then h = f \/ g implies [x,f.x] in h by XBOOLE_0:def 2;
hence thesis by FUNCT_1:8;
end;
theorem
x in dom g & h = f \/ g implies h.x = g.x
proof assume x in dom g;
then [x,g.x] in g by FUNCT_1:def 4;
then h = f \/ g implies [x,g.x] in h by XBOOLE_0:def 2;
hence thesis by FUNCT_1:8;
end;
theorem
x in dom h & h = f \/ g implies h.x = f.x or h.x = g.x
proof assume x in dom h;
then [x,h.x] in h by FUNCT_1:def 4;
then h = f \/ g
implies [x,h.x] in f or [x,h.x] in g by XBOOLE_0:def 2;
hence thesis by FUNCT_1:8;
end;
theorem
f is one-to-one & g is one-to-one & h = f \/ g & rng f misses rng g
implies h is one-to-one
proof
assume that
A1: f is one-to-one & g is one-to-one and
A2: h = f \/ g and
A3: rng f /\ rng g = {};
now let x1,x2;
assume that
A4: x1 in dom h & x2 in dom h and
A5: h.x1 = h.x2;
(x1 in dom f & x2 in dom f implies h.x1 = f.x1 & h.x2 = f.x2) &
(x1 in dom g & x2 in dom g implies h.x1 = g.x1 & h.x2 = g.x2)
by A2,Th34;
then A6: x1 in dom f & x2 in dom f or x1 in dom g & x2 in dom g implies x1
= x2
by A1,A5,FUNCT_1:def 8;
now assume x1 in dom f & x2 in dom g or x1 in dom g & x2 in dom f;
then h.x1 = f.x1 & h.x2 = g.x2 & f.x1 <> g.x2 or
h.x1 = g.x1 & h.x2 = f.x2 & f.x2 <> g.x1 by A2,A3,Lm1,Th34;
hence x1 = x2 by A5;
end;
hence x1 = x2 by A2,A4,A6,Lm3;
end;
hence h is one-to-one by FUNCT_1:def 8;
end;
theorem
f \ X is Function
proof f \ X c= f by XBOOLE_1:36; hence thesis by Th6; end;
canceled 7;
theorem Th46:
f = {} implies f is one-to-one
proof assume f = {};
then for x1,x2,y st [x1,y] in f & [x2,y] in f holds x1 = x2;
hence thesis by Th25;
end;
theorem
f is one-to-one implies for x,y holds [y,x] in f" iff [x,y] in f
proof assume
A1: f is one-to-one;
let x,y;
dom(f") = rng(f) by A1,FUNCT_1:55;
then y in dom(f") & x = (f").y iff x in dom f & y = f.x by A1,FUNCT_1:54;
hence thesis by FUNCT_1:8;
end;
canceled;
theorem
f = {} implies f" = {}
proof assume f = {};
then rng f = {} & f is one-to-one by Th46,RELAT_1:60;
then dom(f") = {} by FUNCT_1:55;
hence thesis by RELAT_1:64;
end;
canceled 2;
theorem
x in dom f & x in X iff [x,f.x] in f|X
proof x in dom f iff [x,f.x] in f by FUNCT_1:def 4,RELAT_1:def 4;
hence thesis by RELAT_1:def 11;
end;
canceled;
theorem
((f|X)*h) c= (f*h) & (g*(f|X)) c= (g*f) by RELAT_1:92,93;
canceled 9;
theorem
g c= f implies f|dom g = g
proof assume
A1: g c= f;
then (g|dom g) c= (f|dom g) by RELAT_1:105;
then A2: g c= (f|dom g) by RELAT_1:97;
[x,y] in (f|dom g) implies [x,y] in g
proof assume
A3: [x,y] in (f|dom g);
then x in dom g by RELAT_1:def 11;
then A4: [x,g.x] in g by FUNCT_1:def 4;
then [x,g.x] in f & [x,y] in f by A1,A3,RELAT_1:def 11;
hence thesis by A4,FUNCT_1:def 1;
end;
then (f|dom g) c= g by RELAT_1:def 3;
hence thesis by A2,XBOOLE_0:def 10;
end;
canceled 2;
theorem
x in dom f & f.x in Y iff [x,f.x] in Y|f
proof x in dom f iff [x,f.x] in f by FUNCT_1:def 4,RELAT_1:def 4;
hence thesis by RELAT_1:def 12;
end;
canceled;
theorem
((Y|f)*h) c= (f*h) & (g*(Y|f)) c= (g*f) by RELAT_1:121,122;
canceled 9;
theorem
g c= f & f is one-to-one implies rng g|f = g
proof assume
A1: g c= f;
then (rng g|g) c= (rng g|f) by RELAT_1:132;
then A2: g c= (rng g|f) by RELAT_1:125;
assume
A3: f is one-to-one;
[x,y] in (rng g|f) implies [x,y] in g
proof assume
A4: [x,y] in (rng g|f);
then y in rng g by RELAT_1:def 12;
then consider x1 such that
A5: [x1,y] in g by RELAT_1:def 5;
[x1,y] in f & [x,y] in f by A1,A4,A5,RELAT_1:def 12;
hence thesis by A3,A5,Th25;
end;
then (rng g|f) c= g by RELAT_1:def 3;
hence thesis by A2,XBOOLE_0:def 10;
end;
canceled 7;
theorem
x in f"Y iff [x,f.x] in f & f.x in Y
proof
thus x in f"Y implies [x,f.x] in f & f.x in Y
proof assume x in f"Y;
then ex y st [x,y] in f & y in Y by RELAT_1:def 14;
hence thesis by FUNCT_1:8;
end;
thus thesis by RELAT_1:def 14;
end;