:: Cartesian Product of Functions
:: by Grzegorz Bancerek
::
:: Received September 30, 1991
:: Copyright (c) 1991-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies FUNCT_1, SUBSET_1, FUNCT_2, XBOOLE_0, CARD_3, RELAT_1, FUNCOP_1,
TARSKI, ZFMISC_1, FUNCT_5, PARTFUN1, SETFAM_1, FINSEQ_4, MCART_1,
FUNCT_6, NAT_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1,
XTUPLE_0, MCART_1, SETFAM_1, FUNCT_2, BINOP_1, PARTFUN1, FUNCT_3,
WELLORD2, FUNCOP_1, FUNCT_4, FUNCT_5, ORDINAL1, CARD_3;
constructors ENUMSET1, SETFAM_1, PARTFUN1, WELLORD2, BINOP_1, FUNCT_3,
FUNCOP_1, FUNCT_4, FUNCT_5, CARD_3, RELSET_1, FINSET_1, DOMAIN_1,
XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCT_2, FUNCOP_1, RELSET_1,
XTUPLE_0, FUNCT_5, CARD_3;
requirements BOOLE, SUBSET;
definitions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0, FUNCOP_1;
equalities BINOP_1, FUNCOP_1;
expansions TARSKI, FUNCT_1, WELLORD2, XBOOLE_0;
theorems TARSKI, ZFMISC_1, FUNCT_1, SETFAM_1, FUNCT_2, FUNCOP_1, CARD_1,
CARD_3, FUNCT_4, FUNCT_5, PARTFUN1, WELLORD2, RELAT_1, XBOOLE_0,
XTUPLE_0;
schemes FUNCT_1, PARTFUN1, CARD_3, CLASSES1;
begin
reserve x,y,y1,y2,z,a,b for object, X,Y,Z,V1,V2 for set,
f,g,h,h9,f1,f2 for Function,
i for Nat,
P for Permutation of X,
D,D1,D2,D3 for non empty set,
d1 for Element of D1,
d2 for Element of D2,
d3 for Element of D3;
theorem Th1:
product f c= Funcs(dom f, Union f)
proof
let x be object;
assume x in product f;
then consider g such that
A1: x = g and
A2: dom g = dom f and
A3: for x being object st x in dom f holds g.x in f.x by CARD_3:def 5;
rng g c= Union f
proof
let y be object;
A4: Union f = union rng f by CARD_3:def 4;
assume y in rng g;
then consider z being object such that
A5: z in dom g & y = g.z by FUNCT_1:def 3;
y in f.z & f.z in rng f by A2,A3,A5,FUNCT_1:def 3;
hence thesis by A4,TARSKI:def 4;
end;
hence thesis by A1,A2,FUNCT_2:def 2;
end;
begin
theorem Th2:
x in dom ~f implies ex y,z being object st x = [y,z]
proof
assume
A1: x in dom ~f;
ex X,Y st dom ~f c= [:X,Y:] by FUNCT_4:44;
hence thesis by A1,RELAT_1:def 1;
end;
theorem Th3:
~([:X,Y:] --> z) = [:Y,X:] --> z
proof
A1: dom ([:X,Y:] --> z) = [:X,Y:];
then
A2: dom ~([:X,Y:] --> z) = [:Y,X:] by FUNCT_4:46;
A3: now
let x be object;
assume
A4: x in [:Y,X:];
then consider y1,y2 being object such that
A5: x = [y2,y1] and
A6: [y1,y2] in [:X,Y:] by A1,A2,FUNCT_4:def 2;
A7: ([:X,Y:] --> z).(y1,y2) = z by A6,FUNCOP_1:7;
([:Y,X:] --> z).(y2,y1) = z by A4,A5,FUNCOP_1:7;
then (~([:X,Y:] --> z)).(y2,y1) = ([:Y,X:] --> z).(y2,y1) by A1,A6,A7,
FUNCT_4:def 2;
hence (~([:X,Y:] --> z)).x = ([:Y,X:] --> z).x by A5;
end;
thus thesis by A2,A3;
end;
theorem Th4:
curry f = curry' ~f & uncurry f = ~uncurry' f
proof
A1: dom curry ~~f = proj1 dom ~~f by FUNCT_5:def 1;
A2: dom curry f = proj1 dom f by FUNCT_5:def 1;
A3: dom curry ~~f = dom curry f
proof
thus dom curry ~~f c= dom curry f
proof
let x be object;
assume x in dom curry ~~f;
then consider y being object such that
A4: [x,y] in dom ~~f by A1,XTUPLE_0:def 12;
[y,x] in dom ~f by A4,FUNCT_4:42;
then [x,y] in dom f by FUNCT_4:42;
hence thesis by A2,XTUPLE_0:def 12;
end;
let x be object;
assume x in dom curry f;
then consider y being object such that
A5: [x,y] in dom f by A2,XTUPLE_0:def 12;
[y,x] in dom ~f by A5,FUNCT_4:42;
then [x,y] in dom ~~f by FUNCT_4:42;
hence thesis by A1,XTUPLE_0:def 12;
end;
A6: curry' ~f = curry ~~f by FUNCT_5:def 3;
now
let x be object;
assume
A7: x in dom curry f;
reconsider g = (curry f).x, h = (curry' ~f).x as Function;
A8: dom g = proj2 (dom f /\ [:{x},proj2 dom f:]) by A7,FUNCT_5:31;
A9: dom h = proj1 (dom ~f /\ [:proj1 dom ~f,{x}:]) by A6,A3,A7,FUNCT_5:34;
A10: dom g = dom h
proof
thus dom g c= dom h
proof
let a be object;
assume a in dom g;
then consider b being object such that
A11: [b,a] in dom f /\ [:{x},proj2 dom f:] by A8,XTUPLE_0:def 13;
[b,a] in [:{x},proj2 dom f:] by A11,XBOOLE_0:def 4;
then
A12: [a,b] in [:proj2 dom f,{x}:] by ZFMISC_1:88;
[b,a] in dom f by A11,XBOOLE_0:def 4;
then
A13: [a,b] in dom ~f by FUNCT_4:42;
proj2 dom f = proj1 dom ~f by FUNCT_5:17;
then [a,b] in dom ~f /\ [:proj1 dom ~f,{x}:] by A13,A12,XBOOLE_0:def 4;
hence thesis by A9,XTUPLE_0:def 12;
end;
let a be object;
assume a in dom h;
then consider b being object such that
A14: [a,b] in dom ~f /\ [:proj1 dom ~f,{x}:] by A9,XTUPLE_0:def 12;
[a,b] in [:proj1 dom ~f,{x}:] by A14,XBOOLE_0:def 4;
then
A15: [b,a] in [:{x},proj1 dom ~f:] by ZFMISC_1:88;
[a,b] in dom ~f by A14,XBOOLE_0:def 4;
then
A16: [b,a] in dom f by FUNCT_4:42;
proj2 dom f = proj1 dom ~f by FUNCT_5:17;
then [b,a] in dom f /\ [:{x},proj2 dom f:] by A16,A15,XBOOLE_0:def 4;
hence thesis by A8,XTUPLE_0:def 13;
end;
now
let a be object;
assume
A17: a in dom g;
then
A18: [x,a] in dom f & g.a = f.(x,a) by A7,FUNCT_5:31;
h.a = (~f).(a,x) by A6,A3,A7,A10,A17,FUNCT_5:34;
hence g.a = h.a by A18,FUNCT_4:def 2;
end;
hence (curry f).x = (curry' ~f).x by A10;
end;
hence curry f = curry' ~f by A6,A3;
A19: dom uncurry f = dom ~~uncurry f
proof
thus dom uncurry f c= dom ~~uncurry f
proof
let a be object;
assume
A20: a in dom uncurry f;
then consider x,g,y such that
A21: a = [x,y] and
x in dom f and
g = f.x and
y in dom g by FUNCT_5:def 2;
[y,x] in dom ~uncurry f by A20,A21,FUNCT_4:42;
hence thesis by A21,FUNCT_4:42;
end;
let a be object;
assume a in dom ~~uncurry f;
then ex x,y being object st a = [y,x] & [x,y] in dom ~uncurry f
by FUNCT_4:def 2;
hence thesis by FUNCT_4:42;
end;
A22: now
let a be object;
assume a in dom ~~uncurry f;
then consider x,y being object such that
A23: a = [y,x] and
A24: [x,y] in dom ~uncurry f by FUNCT_4:def 2;
(~uncurry f).(x,y) = (uncurry f).(y,x) & (~uncurry f).(x,y) = (~~
uncurry f). (y,x) by A24,FUNCT_4:43,def 2;
hence (uncurry f).a = (~~uncurry f).a by A23;
end;
uncurry' f = ~uncurry f by FUNCT_5:def 4;
hence thesis by A19,A22;
end;
theorem
[:X,Y:] <> {} implies curry ([:X,Y:] --> z) = X --> (Y --> z) & curry'
([:X,Y:] --> z) = Y --> (X --> z)
proof
assume
A1: [:X,Y:] <> {};
A2: dom ([:X,Y:] --> z) = [:X,Y:];
A4: now
let x be object;
assume
A5: x in Y;
then consider f such that
A6: (curry' ([:X,Y:] --> z)).x = f & dom f = X and
rng f c= rng ([:X,Y:] --> z) and
A7: for y st y in X holds f.y = ([:X,Y:] --> z).(y,x) by A1,A2,FUNCT_5:32;
A8: now
let y be object;
assume
A9: y in X;
then
A10: f.y = ([:X,Y:] --> z).(y,x) by A7;
(X --> z).y = z & [y,x] in [:X,Y:] by A5,A9,FUNCOP_1:7,ZFMISC_1:87;
hence f.y = (X --> z).y by A10,FUNCOP_1:7;
end;
(Y --> (X --> z)).x = X --> z by A5,FUNCOP_1:7;
hence (curry' ([:X,Y:] --> z)).x = (Y --> (X --> z)).x by A6,A8;
end;
A12: now
let x be object;
assume
A13: x in X;
then consider f such that
A14: (curry ([:X,Y:] --> z)).x = f & dom f = Y and
rng f c= rng ([:X,Y:] --> z) and
A15: for y st y in Y holds f.y = ([:X,Y:] --> z).(x,y) by A1,A2,FUNCT_5:29;
A16: now
let y be object;
assume
A17: y in Y;
then
A18: f.y = ([:X,Y:] --> z).(x,y) by A15;
(Y --> z).y = z & [x,y] in [:X,Y:] by A13,A17,FUNCOP_1:7,ZFMISC_1:87;
hence f.y = (Y --> z).y by A18,FUNCOP_1:7;
end;
(X --> (Y --> z)).x = Y --> z by A13,FUNCOP_1:7;
hence (curry ([:X,Y:] --> z)).x = (X --> (Y --> z)).x by A14,A16;
end;
dom (X --> (Y --> z)) = X & dom curry ([:X,Y:] --> z) = X
by A1,A2,FUNCT_5:24;
hence curry ([:X,Y:] --> z) = X --> (Y --> z) by A12;
dom (Y --> (X --> z)) = Y & dom curry' ([:X,Y:] --> z) = Y
by A1,A2,FUNCT_5:24;
hence thesis by A4;
end;
theorem
uncurry (X --> (Y --> z)) = [:X,Y:] --> z & uncurry' (X --> (Y --> z))
= [:Y,X:] --> z
proof
A1: dom (X --> (Y --> z)) = X;
A2: dom (Y --> z) = Y;
rng (Y --> z) c= {z} by FUNCOP_1:13;
then (Y --> z) in Funcs (Y,{z}) by A2,FUNCT_2:def 2;
then rng (X --> (Y --> z)) c= {Y --> z} & {(Y --> z)} c= Funcs (Y,{z}) by
FUNCOP_1:13,ZFMISC_1:31;
then rng (X --> (Y --> z)) c= Funcs (Y,{z});
then
A3: dom uncurry (X --> (Y --> z)) = [:X,Y:] by A1,FUNCT_5:26;
A4: now
let x be object;
assume
A5: x in [:X,Y:];
then consider y1,g,y2 such that
A6: x = [y1,y2] and
A7: y1 in X & g = (X --> (Y --> z)).y1 and
A8: y2 in dom g by A1,A3,FUNCT_5:def 2;
A9: g = Y --> z by A7,FUNCOP_1:7;
then (Y --> z).y2 = z by A8,FUNCOP_1:7;
then z = (uncurry (X --> (Y --> z))).(y1,y2) by A1,A7,A8,A9,FUNCT_5:38;
hence (uncurry (X --> (Y --> z))).x = ([:X,Y:] --> z).x by A5,A6,FUNCOP_1:7
;
end;
thus uncurry (X --> (Y --> z)) = [:X,Y:] --> z by A3,A4;
then ~uncurry (X --> (Y --> z)) = [:Y,X:] --> z by Th3;
hence thesis by FUNCT_5:def 4;
end;
theorem Th7:
x in dom f & g = f.x implies rng g c= rng uncurry f & rng g c= rng uncurry' f
proof
assume
A1: x in dom f & g = f.x;
thus rng g c= rng uncurry f
proof
let y be object;
assume y in rng g;
then ex z being object st z in dom g & y = g.z by FUNCT_1:def 3;
hence thesis by A1,FUNCT_5:38;
end;
let y be object;
assume y in rng g;
then ex z being object st z in dom g & y = g.z by FUNCT_1:def 3;
hence thesis by A1,FUNCT_5:39;
end;
theorem Th8:
dom uncurry (X --> f) = [:X,dom f:] & rng uncurry (X --> f) c=
rng f & dom uncurry' (X --> f) = [:dom f,X:] & rng uncurry' (X --> f) c= rng f
proof
f in Funcs(dom f, rng f) by FUNCT_2:def 2;
then rng (X --> f) c= {f} & {f} c= Funcs(dom f, rng f) by FUNCOP_1:13
,ZFMISC_1:31;
then dom (X --> f) = X & rng (X --> f) c= Funcs(dom f, rng f);
hence thesis by FUNCT_5:26,41;
end;
theorem
X <> {} implies rng uncurry (X --> f) = rng f & rng uncurry' (X --> f)
= rng f
proof
set x = the Element of X;
assume
A1: X <> {};
then dom (X --> f) = X & (X --> f).x = f by FUNCOP_1:7;
hence rng uncurry (X --> f) c= rng f & rng f c= rng uncurry (X --> f) & rng
uncurry' (X --> f) c= rng f & rng f c= rng uncurry' (X --> f) by A1,Th7,Th8;
end;
theorem Th10:
[:X,Y:] <> {} & f in Funcs([:X,Y:],Z) implies curry f in Funcs(X
,Funcs(Y,Z)) & curry' f in Funcs(Y,Funcs(X,Z))
proof
assume
A1: [:X,Y:] <> {};
assume f in Funcs([:X,Y:],Z);
then
A2: ex g st f = g & dom g = [:X,Y:] & rng g c= Z by FUNCT_2:def 2;
then rng curry f c= Funcs(Y,rng f) & Funcs(Y,rng f) c= Funcs(Y,Z) by
FUNCT_5:35,56;
then
A3: rng curry f c= Funcs(Y,Z);
rng curry' f c= Funcs(X,rng f) & Funcs(X,rng f) c= Funcs(X,Z) by A2,
FUNCT_5:35,56;
then
A4: rng curry' f c= Funcs(X,Z);
dom curry f = X & dom curry' f = Y by A1,A2,FUNCT_5:24;
hence thesis by A3,A4,FUNCT_2:def 2;
end;
theorem Th11:
f in Funcs(X,Funcs(Y,Z)) implies uncurry f in Funcs([:X,Y:],Z) &
uncurry' f in Funcs([:Y,X:],Z)
proof
assume f in Funcs(X,Funcs(Y,Z));
then
A1: ex g st f = g & dom g = X & rng g c= Funcs(Y,Z) by FUNCT_2:def 2;
then
A2: dom uncurry f = [:X,Y:] & dom uncurry' f = [:Y,X:] by FUNCT_5:26;
rng uncurry f c= Z & rng uncurry' f c= Z by A1,FUNCT_5:41;
hence thesis by A2,FUNCT_2:def 2;
end;
theorem
(curry f in Funcs(X,Funcs(Y,Z)) or curry' f in Funcs(Y,Funcs(X,Z))) &
dom f c= [:V1,V2:] implies f in Funcs([:X,Y:],Z)
proof
assume curry f in Funcs(X,Funcs(Y,Z)) or curry' f in Funcs(Y,Funcs(X,Z));
then
A1: uncurry curry f in Funcs([:X,Y:],Z) or uncurry' curry' f in Funcs([:X,Y
:],Z) by Th11;
assume dom f c= [:V1,V2:];
hence thesis by A1,FUNCT_5:50;
end;
theorem
(uncurry f in Funcs([:X,Y:],Z) or uncurry' f in Funcs([:Y,X:],Z)) &
rng f c= PFuncs(V1,V2) & dom f = X implies f in Funcs(X,Funcs(Y,Z))
proof
assume that
A1: uncurry f in Funcs([:X,Y:],Z) or uncurry' f in Funcs([:Y,X:],Z) and
A2: rng f c= PFuncs(V1,V2) and
A3: dom f = X;
A4: uncurry' f = ~uncurry f by FUNCT_5:def 4;
A5: (ex g st uncurry f = g & dom g = [:X,Y:] & rng g c= Z) or ex g st
uncurry' f = g & dom g = [:Y,X:] & rng g c= Z by A1,FUNCT_2:def 2;
then
A6: dom uncurry' f = [:Y,X:] by A4,FUNCT_4:46;
rng f c= Funcs(Y,Z)
proof
let y be object;
assume
A7: y in rng f;
then consider x being object such that
A8: x in dom f and
A9: y = f.x by FUNCT_1:def 3;
ex g st y = g & dom g c= V1 & rng g c= V2 by A2,A7,PARTFUN1:def 3;
then reconsider h = y as Function;
A10: dom h = Y
proof
thus dom h c= Y
proof
let z be object;
assume z in dom h;
then [z,x] in dom uncurry' f by A8,A9,FUNCT_5:39;
hence thesis by A6,ZFMISC_1:87;
end;
let z be object;
assume z in Y;
then [z,x] in [:Y,X:] by A3,A8,ZFMISC_1:87;
then [x,z] in dom uncurry f by A4,A6,FUNCT_4:42;
then consider y1,f1,y2 such that
A11: [x,z] = [y1,y2] and
y1 in dom f and
A12: f1 = f.y1 & y2 in dom f1 by FUNCT_5:def 2;
x = y1 by A11,XTUPLE_0:1;
hence thesis by A9,A11,A12,XTUPLE_0:1;
end;
rng h c= Z
proof
let z be object;
assume z in rng h;
then ex y1 being object st y1 in dom h & z = h.y1 by FUNCT_1:def 3;
then z in rng uncurry f & z in rng uncurry' f by A8,A9,FUNCT_5:38,39;
hence thesis by A5;
end;
hence thesis by A10,FUNCT_2:def 2;
end;
hence thesis by A3,FUNCT_2:def 2;
end;
theorem
f in PFuncs([:X,Y:],Z) implies curry f in PFuncs(X,PFuncs(Y,Z)) &
curry' f in PFuncs(Y,PFuncs(X,Z))
proof
assume f in PFuncs([:X,Y:],Z);
then
A1: ex g st f = g & dom g c= [:X,Y:] & rng g c= Z by PARTFUN1:def 3;
then proj1 [:X,Y:] c= X & proj1 dom f c= proj1 [:X,Y:] by FUNCT_5:10
,XTUPLE_0:8;
then proj1 dom f c= X;
then
A2: PFuncs(proj1 dom f,rng f) c= PFuncs(X,Z) by A1,PARTFUN1:50;
proj2 [:X,Y:] c= Y & proj2 dom f c= proj2 [:X,Y:] by A1,FUNCT_5:10,XTUPLE_0:9
;
then proj2 dom f c= Y;
then
rng curry f c= PFuncs(proj2 dom f,rng f) & PFuncs(proj2 dom f,rng f) c=
PFuncs(Y,Z) by A1,FUNCT_5:36,PARTFUN1:50;
then
A3: rng curry f c= PFuncs(Y,Z);
rng curry' f c= PFuncs(proj1 dom f,rng f) by FUNCT_5:36;
then
A4: rng curry' f c= PFuncs(X,Z) by A2;
dom curry f c= X & dom curry' f c= Y by A1,FUNCT_5:25;
hence thesis by A3,A4,PARTFUN1:def 3;
end;
theorem Th15:
f in PFuncs(X,PFuncs(Y,Z)) implies uncurry f in PFuncs([:X,Y:],Z
) & uncurry' f in PFuncs([:Y,X:],Z)
proof
assume f in PFuncs(X,PFuncs(Y,Z));
then
A1: ex g st f = g & dom g c= X & rng g c= PFuncs(Y,Z) by PARTFUN1:def 3;
then dom uncurry f c= [:dom f,Y:] & [:dom f,Y:] c= [:X,Y:] by FUNCT_5:37
,ZFMISC_1:96;
then
A2: dom uncurry f c= [:X,Y:];
dom uncurry' f c= [:Y,dom f:] & [:Y,dom f:] c= [:Y,X:] by A1,FUNCT_5:37
,ZFMISC_1:96;
then
A3: dom uncurry' f c= [:Y,X:];
rng uncurry f c= Z & rng uncurry' f c= Z by A1,FUNCT_5:40;
hence thesis by A2,A3,PARTFUN1:def 3;
end;
theorem
(curry f in PFuncs(X,PFuncs(Y,Z)) or curry' f in PFuncs(Y,PFuncs(X,Z))
) & dom f c= [:V1,V2:] implies f in PFuncs([:X,Y:],Z)
proof
assume
curry f in PFuncs(X,PFuncs(Y,Z)) or curry' f in PFuncs(Y,PFuncs(X,Z) );
then
A1: uncurry curry f in PFuncs([:X,Y:],Z) or uncurry' curry' f in PFuncs([:X,
Y:],Z) by Th15;
assume dom f c= [:V1,V2:];
hence thesis by A1,FUNCT_5:50;
end;
theorem
(uncurry f in PFuncs([:X,Y:],Z) or uncurry' f in PFuncs([:Y,X:],Z)) &
rng f c= PFuncs(V1,V2) & dom f c= X implies f in PFuncs(X,PFuncs(Y,Z))
proof
assume that
A1: uncurry f in PFuncs([:X,Y:],Z) or uncurry' f in PFuncs([:Y,X:],Z) and
A2: rng f c= PFuncs(V1,V2) and
A3: dom f c= X;
A4: (ex g st uncurry f = g & dom g c= [:X,Y:] & rng g c= Z) or ex g st
uncurry' f = g & dom g c= [:Y,X:] & rng g c= Z by A1,PARTFUN1:def 3;
uncurry' f = ~uncurry f by FUNCT_5:def 4;
then
A5: dom uncurry' f c= [:Y,X:] by A4,FUNCT_4:45;
rng f c= PFuncs(Y,Z)
proof
let y be object;
assume
A6: y in rng f;
then consider x being object such that
A7: x in dom f & y = f.x by FUNCT_1:def 3;
ex g st y = g & dom g c= V1 & rng g c= V2 by A2,A6,PARTFUN1:def 3;
then reconsider h = y as Function;
A8: rng h c= Z
proof
let z be object;
assume z in rng h;
then ex y1 being object st y1 in dom h & z = h.y1 by FUNCT_1:def 3;
then z in rng uncurry f & z in rng uncurry' f by A7,FUNCT_5:38,39;
hence thesis by A4;
end;
dom h c= Y
proof
let z be object;
assume z in dom h;
then [z,x] in dom uncurry' f by A7,FUNCT_5:39;
hence thesis by A5,ZFMISC_1:87;
end;
hence thesis by A8,PARTFUN1:def 3;
end;
hence thesis by A3,PARTFUN1:def 3;
end;
begin
definition
::$CD
end;
::$CT 4
definition
let f be Function-yielding Function;
func doms f -> Function means
: Def1:
dom it = dom f & for x being object st x in dom f holds it.x = proj1 (f.x);
existence
proof
deffunc F(object) = proj1 (f.$1);
ex F be Function st dom F = dom f &
for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A1: dom f1 = dom f and
A2: for x being object st x in dom f holds f1.x = proj1 (f.x) and
A3: dom f2 = dom f and
A4: for x being object st x in dom f holds f2.x = proj1 (f.x);
now
let x be object;
assume
A5: x in dom f;
then f1.x = proj1 (f.x) by A2;
hence f1.x = f2.x by A4,A5;
end;
hence thesis by A1,A3;
end;
func rngs f -> Function means
: Def2:
dom it = dom f & for x being object st x in dom f holds it.x = proj2 (f.x);
existence
proof
deffunc F(object) = proj2 (f.$1);
ex F be Function st dom F = dom f &
for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A6: dom f1 = dom f and
A7: for x being object st x in dom f holds f1.x = proj2 (f.x) and
A8: dom f2 = dom f and
A9: for x being object st x in dom f holds f2.x = proj2 (f.x);
now
let x be object;
assume
A10: x in dom f;
then f1.x = proj2 (f.x) by A7;
hence f1.x = f2.x by A9,A10;
end;
hence thesis by A6,A8;
end;
end;
definition
let f be Function;
func meet f -> set equals
meet rng f;
correctness;
end;
theorem Th18:
for f being Function-yielding Function holds
x in dom f & g = f.x implies x in dom doms f & (doms f).x = dom
g & x in dom rngs f & (rngs f).x = rng g
by Def1,Def2;
theorem
doms {} = {} & rngs {} = {}
by Def1,Def2,RELAT_1:38;
theorem Th20:
doms (X --> f) = X --> dom f & rngs (X --> f) = X --> rng f
proof
A1: dom (X --> dom f) = X &
dom doms (X --> f) = dom (X --> f ) by Def1;
A2: dom (X --> f) = X & (X --> f)"rng (X --> f) = dom (X --> f) by RELAT_1:134;
now
let x be object;
assume
A3: x in X;
then (X --> f).x = f & (X --> dom f).x = dom f by FUNCOP_1:7;
hence (doms (X --> f)).x = (X --> dom f).x by A2,A3,Def1;
end;
hence doms (X --> f) = X --> dom f by A1;
A4: now
let x be object;
assume
A5: x in X;
then (X --> f).x = f & (X --> rng f).x = rng f by FUNCOP_1:7;
hence (rngs (X --> f)).x = (X --> rng f).x by A2,A5,Def2;
end;
dom (X --> rng f) = X &
dom rngs (X --> f) = dom (X --> f ) by Def2;
hence thesis by A4;
end;
theorem Th21:
f <> {} implies
for x being object holds
x in meet f iff for y being object st y in dom f holds x in f.y
proof
assume
A1: f <> {};
let x be object;
thus x in meet f implies for y being object st y in dom f holds x in f.y
proof
assume
A2: x in meet f;
let y be object;
assume y in dom f;
then f.y in rng f by FUNCT_1:def 3;
then meet f c= f.y by SETFAM_1:3;
hence thesis by A2;
end;
assume
A3: for y being object st y in dom f holds x in f.y;
now
let z be set;
assume z in rng f;
then ex y being object st y in dom f & z = f.y by FUNCT_1:def 3;
hence x in z by A3;
end;
hence thesis by A1,SETFAM_1:def 1;
end;
theorem
Union ({} --> Y) = {} & meet ({} --> Y) = {}
proof
union rng ({} --> Y) = {} by ZFMISC_1:2;
hence thesis by CARD_3:def 4,SETFAM_1:def 1;
end;
theorem Th23:
X <> {} implies Union (X --> Y) = Y & meet (X --> Y) = Y
proof
assume X <> {};
then
A1: rng (X --> Y) = {Y} by FUNCOP_1:8;
then union rng (X --> Y) = Y by ZFMISC_1:25;
hence thesis by A1,CARD_3:def 4,SETFAM_1:10;
end;
definition
let f be Function, x, y be object;
func f..(x,y) -> set equals
(uncurry f).(x,y);
correctness;
end;
theorem
x in X & y in dom f implies (X --> f)..(x,y) = f.y
proof
A1: x in X implies (X --> f).x = f by FUNCOP_1:7;
dom (X --> f) = X;
hence thesis by A1,FUNCT_5:38;
end;
begin
definition
let f be Function-yielding Function;
func <:f:> -> Function equals
curry ((uncurry' f)|([:meet doms f, dom f:] qua set));
correctness;
end;
theorem Th25:
for f being Function-yielding Function holds
dom <:f:> = meet doms f & rng <:f:> c= product rngs f
proof let f be Function-yielding Function;
set f9 = (uncurry' f)|([:meet doms f, dom f:] qua set);
dom ((uncurry' f)|([:meet doms f, dom f:] qua set)) c= [:meet doms f,
dom f:] by RELAT_1:58;
hence
A1: dom <:f:> c= meet doms f by FUNCT_5:25;
A2: dom doms f = dom f by Def1;
thus meet doms f c= dom <:f:>
proof
set y = the Element of rng doms f;
let x be object;
assume
A3: x in meet doms f;
then
A4: rng doms f <> {} by SETFAM_1:def 1;
then
A5: x in y by A3,SETFAM_1:def 1;
consider z being object such that
A6: z in dom doms f and
A7: y = (doms f).z by A4,FUNCT_1:def 3;
reconsider g = f.z as Function;
A8: z in dom f by A2,A6;
then y = dom g by A7,Th18;
then
A9: [x,z] in dom uncurry' f by A8,A5,FUNCT_5:39;
[x,z] in [:meet doms f, dom f:] by A3,A8,ZFMISC_1:87;
then [x,z] in dom (uncurry' f) /\ [:meet doms f, dom f:] by A9,
XBOOLE_0:def 4;
then [x,z] in dom ((uncurry' f)|([:meet doms f, dom f:] qua set)) by
RELAT_1:61;
then
x in proj1 dom ((uncurry' f)|([:meet doms f, dom f:] qua set))
by XTUPLE_0:def 12;
hence thesis by FUNCT_5:def 1;
end;
A10: dom rngs f = dom f by Def2;
thus rng <:f:> c= product rngs f
proof
let y be object;
A11: dom f9 = dom (uncurry' f) /\ [:meet doms f, dom f:] by RELAT_1:61;
A12: uncurry' f = ~(uncurry f) by FUNCT_5:def 4;
assume y in rng <:f:>;
then consider x being object such that
A13: x in dom <:f:> and
A14: y = <:f:>.x by FUNCT_1:def 3;
reconsider g = y as Function by A14;
A15: dom g = proj2 (dom f9 /\ [:{x},proj2 dom f9:]) by A13,A14,FUNCT_5:31;
A16: dom g = dom rngs f
proof
thus dom g c= dom rngs f
proof
let z be object;
assume z in dom g;
then [x,z] in dom f9 by A13,A14,FUNCT_5:31;
then [x,z] in dom uncurry' f by A11,XBOOLE_0:def 4;
then [z,x] in dom uncurry f by A12,FUNCT_4:42;
then consider y1, h, y2 such that
A17: [z,x] = [y1,y2] and
A18: y1 in dom f and
h = f.y1 and
y2 in dom h by FUNCT_5:def 2;
A19: z = y1 by A17,XTUPLE_0:1;
thus thesis by A10,A18,A19;
end;
let z be object;
A20: x in {x} by TARSKI:def 1;
assume
A21: z in dom rngs f;
reconsider h = f.z as Function;
A22: z in dom f by A10,A21;
then dom h = (doms f).z by Th18;
then dom h in rng doms f by A2,A10,A21,FUNCT_1:def 3;
then x in dom h by A1,A13,SETFAM_1:def 1;
then [z,x] in dom uncurry f by A22,FUNCT_5:def 2;
then
A23: [x,z] in dom uncurry' f by A12,FUNCT_4:42;
[x,z] in [:meet doms f, dom f:] by A1,A13,A22,ZFMISC_1:87;
then
A24: [x,z] in dom f9 by A11,A23,XBOOLE_0:def 4;
then z in proj2 dom f9 by XTUPLE_0:def 13;
then [x,z] in [:{x},proj2 dom f9:] by A20,ZFMISC_1:87;
then [x,z] in dom f9 /\ [:{x},proj2 dom f9:] by A24,XBOOLE_0:def 4;
hence thesis by A15,XTUPLE_0:def 13;
end;
now
let z be object;
assume
A25: z in dom rngs f;
reconsider h = f.z as Function;
A26: z in dom f by A10,A25;
then dom h = (doms f).z by Th18;
then dom h in rng doms f by A2,A10,A25,FUNCT_1:def 3;
then
A27: x in dom h by A1,A13,SETFAM_1:def 1;
then
A28: h.x in rng h by FUNCT_1:def 3;
g.z = f9.(x,z) & [x,z] in dom f9 by A13,A14,A16,A25,FUNCT_5:31;
then (uncurry' f).(x,z) = g.z by FUNCT_1:47;
then g.z = h.x by A26,A27,FUNCT_5:39;
hence g.z in (rngs f).z by A26,A28,Th18;
end;
hence thesis by A16,CARD_3:def 5;
end;
end;
registration let f be Function-yielding Function;
cluster <:f:> ->Function-yielding;
coherence;
end;
::$CT
theorem Th26:
for f being Function-yielding Function holds
x in dom <:f:> & g = <:f:>.x implies dom g = dom f &
for y st y in dom g holds [y,x] in dom uncurry f & g.y = (uncurry f).(y,x)
proof let f being Function-yielding Function;
A1: rng <:f:> c= product rngs f & dom rngs f = dom f by Def2,Th25;
assume
A2: x in dom <:f:> & g = <:f:>.x;
then g in rng <:f:> by FUNCT_1:def 3;
hence dom g = dom f by A1,CARD_3:9;
let y such that
A3: y in dom g;
A4: [x,y] in dom ((uncurry' f)|([:meet doms f, dom f:] qua set)) by A2,A3,
FUNCT_5:31;
then [x,y] in dom (uncurry' f) /\ [:meet doms f, dom f:] by RELAT_1:61;
then
A5: [x,y] in dom uncurry' f by XBOOLE_0:def 4;
g.y = ((uncurry' f)|([:meet doms f, dom f:] qua set)).(x,y) by A2,A3,
FUNCT_5:31;
then
A6: g.y = (uncurry' f).(x,y) by A4,FUNCT_1:47;
~(uncurry f) = uncurry' f by FUNCT_5:def 4;
hence thesis by A6,A5,FUNCT_4:42,43;
end;
theorem Th27:
for f being Function-yielding Function st x in dom <:f:>
for g st g in rng f holds x in dom g
proof let f be Function-yielding Function;
assume
A1: x in dom <:f:>;
let g;
assume g in rng f;
then consider y being object such that
A2: y in dom f & g = f.y by FUNCT_1:def 3;
y in dom doms f & (doms f).y = dom g by A2,Th18;
then dom g in rng doms f by FUNCT_1:def 3;
then
A3: meet rng doms f c= dom g by SETFAM_1:3;
meet doms f = dom <:f:> by Th25;
hence thesis by A1,A3;
end;
theorem
for x being object, f being Function-yielding Function st
g in rng f &
for g st g in rng f holds x in dom g
holds x in dom <:f :>
proof let x be object, f be Function-yielding Function;
assume that
A1: g in rng f and
A2: for g st g in rng f holds x in dom g;
ex y being object st y in dom f & g = f.y by A1,FUNCT_1:def 3;
then
A3: doms f <> {} by Th18;
A4: now
let y be object;
assume y in dom doms f;
then
A5: y in dom f by Def1;
reconsider g = f.y as Function;
A6: y in dom f by A5;
then g in rng f by FUNCT_1:def 3;
then x in dom g by A2;
hence x in (doms f).y by A6,Th18;
end;
dom <:f:> = meet doms f by Th25;
hence thesis by A3,A4,Th21;
end;
theorem Th29:
for f being Function-yielding Function
st x in dom f & g = f.x & y in dom <:f:> & h = <:f:>.y
holds g.y = h.x
proof let f be Function-yielding Function;
assume that
A1: x in dom f & g = f.x and
A2: y in dom <:f:> and
A3: h = <:f:>.y;
dom h = dom f by A2,A3,Th26;
then x in dom h by A1;
then
A4: h.x = (uncurry f).(x,y) by A2,A3,Th26;
g in rng f by A1,FUNCT_1:def 3;
then y in dom g by A2,Th27;
hence thesis by A1,A4,FUNCT_5:38;
end;
theorem
for f being Function-yielding Function
st x in dom f & f.x is Function & y in dom <:f:>
holds f..(x,y) = <:f:>..( y, x )
proof let f be Function-yielding Function;
assume that
A1: x in dom f and
f.x is Function and
A2: y in dom <:f:>;
reconsider g = f.x, h = <:f:>.y as Function;
A3: dom h = dom f by A2,Th26;
A4: g in rng f by A1,FUNCT_1:def 3;
A5: x in dom h by A1,A3;
y in dom g by A2,A4,Th27;
hence f..(x,y) = g.y by A1,FUNCT_5:38
.= h.x by A1,A2,Th29
.= <:f:>..(y,x) by A2,A5,FUNCT_5:38;
end;
definition
let f be Function-yielding Function;
func Frege f -> Function means
: Def6:
dom it = product doms f & for g st g
in product doms f ex h st it.g = h & dom h = dom f & for x st x in
dom h holds h.x = (uncurry f).(x,g.x);
existence
proof
defpred P[object,object] means
ex g,h st $1 = g & $2 = h & dom h = dom f &
for z st z in dom h holds h.z = (uncurry f).(z,g.z);
A1: for x being object st x in product doms f ex y being object st P[x,y]
proof
let x be object;
assume x in product doms f;
then consider g such that
A2: x = g and
dom g = dom doms f and
for x being object st x in dom doms f holds g.x in (doms f).x
by CARD_3:def 5;
deffunc F(object) = (uncurry f).[$1,g.$1];
consider h such that
A3: dom h = dom f & for z being object st z in dom f holds
h.z = F(z) from FUNCT_1:sch 3;
reconsider y = h as set;
take y, g, h;
thus thesis by A2,A3;
end;
consider F being Function such that
A4: dom F = product doms f &
for x being object st x in product doms f holds P[x,F.x]
from CLASSES1:sch 1(A1);
take F;
thus dom F = product doms f by A4;
let g;
assume g in product doms f;
then
ex g1,h being Function st g = g1 & F.g = h & dom h = dom f
& for z st z in dom h holds h.z = (uncurry f).(z,g1.z) by A4;
hence thesis;
end;
uniqueness
proof
let f1,f2 be Function such that
A5: dom f1 = product doms f and
A6: for g st g in product doms f ex h st f1.g = h & dom h =
dom f & for x st x in dom h holds h.x = (uncurry f).(x,g.x) and
A7: dom f2 = product doms f and
A8: for g st g in product doms f ex h st f2.g = h & dom h =
dom f & for x st x in dom h holds h.x = (uncurry f).(x,g.x);
now
let x be object;
assume
A9: x in product doms f;
then consider g such that
A10: x = g and
dom g = dom doms f and
for x being object st x in dom doms f holds g.x in (doms f).x
by CARD_3:def 5;
consider h2 being Function such that
A11: f2.g = h2 and
A12: dom h2 = dom f and
A13: for y st y in dom h2 holds h2.y = (uncurry f).(y,g.y) by A8,A9,A10;
consider h1 being Function such that
A14: f1.g = h1 and
A15: dom h1 = dom f and
A16: for y st y in dom h1 holds h1.y = (uncurry f).(y,g.y) by A6,A9,A10;
now
let z be object;
assume
A17: z in dom f;
then h1.z = (uncurry f).(z,g.z) by A15,A16;
hence h1.z = h2.z by A12,A13,A17;
end;
hence f1.x = f2.x by A10,A14,A15,A11,A12,FUNCT_1:2;
end;
hence thesis by A5,A7;
end;
end;
theorem
for f being Function-yielding Function
st g in product doms f & x in dom g
holds (Frege f)..(g,x) = f..(x,g.x)
proof let f be Function-yielding Function;
assume that
A1: g in product doms f and
A2: x in dom g;
A3: dom g = dom doms f by A1,CARD_3:9;
A4: dom doms f = dom f by Def1;
consider h such that
A5: (Frege f).g = h and
A6: dom h = dom f and
A7: for x st x in dom h holds h.x = (uncurry f).(x,g.x) by A1,Def6;
dom Frege f = product doms f by Def6;
hence (Frege f)..(g,x) = h.x by A1,A2,A5,A6,A3,A4,FUNCT_5:38
.= f..(x,g.x) by A2,A6,A7,A3,A4;
end;
Lm1: for f being Function-yielding Function holds
rng Frege f c= product rngs f
proof let f be Function-yielding Function;
let x be object;
assume x in rng Frege f;
then consider y being object such that
A1: y in dom Frege f and
A2: x = (Frege f).y by FUNCT_1:def 3;
A3: dom Frege f = product doms f by Def6;
then consider g such that
A4: y = g and
dom g = dom doms f and
A5: for z being object st z in dom doms f holds g.z in (doms f).z
by A1,CARD_3:def 5;
consider h such that
A6: (Frege f).g = h and
A7: dom h = dom f and
A8: for z st z in dom h holds h.z = (uncurry f).(z,g.z) by A1,A3,A4,Def6;
A9: dom rngs f = dom f by Def2;
A10: dom doms f = dom f by Def1;
now
let z be object;
assume
A11: z in dom rngs f;
reconsider t = f.z as Function;
A12: g.z in (doms f). z by A5,A9,A10,A11;
A13: z in dom f by A9,A11;
then
A14: (rngs f).z = rng t by Th18;
A15: (doms f).z = dom t by A13,Th18;
then
A16: t.(g.z) in rng t by A12,FUNCT_1:def 3;
t.(g.z) = (uncurry f).(z,g.z) by A13,A12,A15,FUNCT_5:38;
hence h.z in (rngs f).z by A7,A8,A9,A11,A14,A16;
end;
hence thesis by A2,A4,A6,A7,A9,CARD_3:def 5;
end;
theorem
for f being Function-yielding Function
st x in dom f & g = f.x & h in product doms f & h9 = (Frege f).h
holds h.x in dom g & h9.x = g.(h.x) & h9 in product rngs f
proof let f be Function-yielding Function;
assume that
A1: x in dom f & g = f.x and
A2: h in product doms f and
A3: h9 = (Frege f).h;
A4: x in dom f by A1;
A5: dom doms f = dom f by Def1;
( ex f2 st h = f2 & dom f2 = dom doms f &
for x being object st x in dom doms f holds
f2.x in (doms f).x)& (doms f).x = dom g by A1,A2,Th18,CARD_3:def 5;
hence
A6: h.x in dom g by A5,A4;
ex f1 st (Frege f).h = f1 & dom f1 = dom f & for x st x in
dom f1 holds f1.x = (uncurry f).(x,h.x) by A2,Def6;
hence h9.x = (uncurry f).(x,h.x) by A3,A4
.= g.(h.x) by A1,A6,FUNCT_5:38;
A7: rng Frege f c= product rngs f by Lm1;
dom Frege f = product doms f by Def6;
then h9 in rng Frege f by A2,A3,FUNCT_1:def 3;
hence thesis by A7;
end;
Lm2: for f being Function-yielding Function holds
product rngs f c= rng Frege f
proof let f be Function-yielding Function;
let x be object;
deffunc F(object) = (doms f).$1;
assume x in product rngs f;
then consider g such that
A1: x = g and
A2: dom g = dom rngs f and
A3: for y being object st y in dom rngs f holds g.y in (rngs f).y
by CARD_3:def 5;
defpred P[object,object] means ex f1 st f1 = f.$1 & f1.$2 = g.$1;
consider h such that
A4: dom h = dom f & for x being object st x in dom f for y being object
holds y in h.x iff y in F(x) & P[x,y] from CARD_3:sch 2;
A5: product doms f = dom Frege f by Def6;
A6: dom doms f = dom f by Def1;
A7: dom rngs f = dom f by Def2;
A8: now
let X;
assume X in rng h;
then consider x being object such that
A9: x in dom h and
A10: X = h.x by FUNCT_1:def 3;
reconsider fx = f.x as Function;
A11: x in dom f by A4,A9;
then
A12: (rngs f).x = rng fx by Th18;
g.x in (rngs f).x by A3,A7,A4,A9;
then
A13: ex y being object st y in dom fx & g.x = fx.y by A12,FUNCT_1:def 3;
(doms f).x = dom fx by A11,Th18;
hence X <> {} by A4,A9,A10,A13;
end;
A14: now
assume dom f <> {};
then reconsider D = rng h as non empty set by A4,RELAT_1:42;
consider Ch being Function such that
A15: dom Ch = D and
A16: for x being set st x in D holds Ch.x in x by A8,FUNCT_1:111;
A17: dom (Ch*h) = dom h by A15,RELAT_1:27;
now
let y be object;
assume
A18: y in dom doms f;
then (Ch*h).y = Ch.(h.y) & h.y in rng h by A6,A4,A17,FUNCT_1:12,def 3;
then (Ch*h).y in h.y by A16;
hence (Ch*h).y in (doms f).y by A6,A4,A18;
end;
then
A19: Ch*h in product doms f by A6,A4,A17,CARD_3:def 5;
then consider h1 being Function such that
A20: (Frege f).(Ch*h) = h1 and
A21: dom h1 = dom f and
A22: for x st x in dom h1 holds h1.x = (uncurry f).(x,(Ch*h).x) by Def6;
now
let z be object;
assume
A23: z in dom f;
then
A24: h1.z = (uncurry f).(z,(Ch*h).z) by A21,A22;
(Ch*h).z = Ch.( h.z ) & h.z in rng h by A4,A17,A23,FUNCT_1:12,def 3;
then
A25: (Ch*h).z in h.z by A16;
then consider f1 such that
A26: f1 = f.z and
A27: f1.((Ch*h).z) = g.z by A4,A23;
A28: (Ch*h).z in (doms f).z by A4,A23,A25;
A29: z in dom f by A23;
then (doms f).z = dom f1 by A26,Th18;
hence h1.z = g.z by A29,A24,A26,A27,A28,FUNCT_5:38;
end;
then x = h1 by A1,A2,A7,A21,FUNCT_1:2;
hence thesis by A5,A19,A20,FUNCT_1:def 3;
end;
now
assume
A30: dom f = {};
then
A31: g = {} by A2,Def2;
dom Frege f = {{}} by A6,A5,A30,CARD_3:10,RELAT_1:41;
then
A32: {} in dom Frege f by TARSKI:def 1;
then consider h such that
A33: (Frege f).{} = h and
A34: dom h = dom f and
for x st x in dom h holds h.x = (uncurry f).(x,{} .x) by A5,Def6;
h = {} by A30,A34;
hence thesis by A1,A31,A32,A33,FUNCT_1:def 3;
end;
hence thesis by A14;
end;
theorem Th33:
for f being Function-yielding Function holds
rng Frege f = product rngs f
by Lm1,Lm2;
theorem Th34:
for f being Function-yielding Function
st not {} in rng f
holds (Frege f is one-to-one iff for g st g in
rng f holds g is one-to-one)
proof let f be Function-yielding Function;
set h0 = the Element of product doms f;
A1: dom doms f = dom f by Def1;
assume
A2: not {} in rng f;
now
assume {} in rng doms f;
then consider x being object such that
A3: x in dom doms f and
A4: {} = (doms f).x by FUNCT_1:def 3;
A5: x in dom f by A3,Def1;
reconsider g = f.x as Function;
A6: x in dom f by A5;
then
A7: g in rng f by FUNCT_1:def 3;
{} = dom g by A4,A6,Th18;
hence contradiction by A2,A7,RELAT_1:41;
end;
then product doms f <> {} by CARD_3:26;
then consider h such that
h0 = h and
dom h = dom doms f and
A8: for x being object st x in dom doms f holds h.x in (doms f).x
by CARD_3:def 5;
A9: dom Frege f = product doms f by Def6;
thus Frege f is one-to-one implies for g st g in rng f holds g is one-to-one
proof
deffunc G(object) = h.$1;
assume
A10: for x,y being object
st x in dom Frege f & y in dom Frege f & (Frege f).x = (
Frege f).y holds x = y;
let g;
assume g in rng f;
then consider z being object such that
A11: z in dom f & g = f.z by FUNCT_1:def 3;
defpred P[object] means $1 = z;
let x,y be object;
deffunc F(object) = x;
consider h1 being Function such that
A12: dom h1 = dom f & for a being object st a in dom f holds
(P[a] implies h1.a = F(a)) & (not P[a] implies h1.a = G(a)) from PARTFUN1:sch 1
;
assume that
A13: x in dom g and
A14: y in dom g and
A15: g.x = g.y;
now
let a be object;
assume
A16: a in dom doms f;
then
A17: a <> z implies h1.a = h.a by A1,A12;
a = z implies h1.a = x by A1,A12,A16;
hence h1.a in (doms f).a by A8,A11,A13,A16,A17,Th18;
end;
then
A18: h1 in product doms f by A1,A12,CARD_3:def 5;
then consider g1 being Function such that
A19: (Frege f).h1 = g1 and
A20: dom g1 = dom f and
A21: for x st x in dom g1 holds g1.x = (uncurry f).(x,h1.x) by Def6;
defpred P[object] means $1 = z;
deffunc G(object) = h.$1;
deffunc F(object) = y;
consider h2 being Function such that
A22: dom h2 = dom f & for a being object st a in dom f holds
(P[a] implies h2.a = F(a)) & (not P[a] implies h2.a = G(a))
from PARTFUN1:sch 1;
now
let a be object;
assume
A23: a in dom doms f;
then
A24: a <> z implies h2.a = h.a by A1,A22;
a = z implies h2.a = y by A1,A22,A23;
hence h2.a in (doms f).a by A8,A11,A14,A23,A24,Th18;
end;
then
A25: h2 in product doms f by A1,A22,CARD_3:def 5;
then consider g2 being Function such that
A26: (Frege f).h2 = g2 and
A27: dom g2 = dom f and
A28: for x st x in dom g2 holds g2.x = (uncurry f).(x,h2.x) by Def6;
now
let a be object;
assume
A29: a in dom f;
then
A30: g2.a = (uncurry f).(a,h2.a) by A27,A28;
A31: g1.a = (uncurry f).(a,h1.a) by A20,A21,A29;
per cases;
suppose
A32: a <> z;
then h1.a = h.a by A12,A29;
hence g1.a = g2.a by A22,A29,A30,A31,A32;
end;
suppose
A33: a = z;
then h1.a = x by A12,A29;
then
A34: g1.a = g.x by A11,A13,A31,A33,FUNCT_5:38;
h2.a = y by A22,A29,A33;
hence g1.a = g2.a by A11,A14,A15,A30,A33,A34,FUNCT_5:38;
end;
end;
then g1 = g2 by A20,A27;
then
A35: h1 = h2 by A9,A10,A18,A19,A25,A26;
A36: z in dom f by A11;
then h1.z = x by A12;
hence thesis by A36,A22,A35;
end;
assume
A37: for g st g in rng f holds g is one-to-one;
let x,y be object;
assume that
A38: x in dom Frege f and
A39: y in dom Frege f and
A40: (Frege f).x = (Frege f).y;
consider g2 being Function such that
A41: y = g2 and
A42: dom g2 = dom doms f and
A43: for x being object st x in dom doms f holds g2.x in (doms f).x
by A9,A39,CARD_3:def 5;
consider g1 being Function such that
A44: x = g1 and
A45: dom g1 = dom doms f and
A46: for x being object st x in dom doms f holds g1.x in (doms f).x
by A9,A38,CARD_3:def 5;
consider h2 being Function such that
A47: (Frege f).g2 = h2 and
A48: dom h2 = dom f & for x st x in dom h2 holds h2.x = (
uncurry f).(x,g2.x) by A9,A39,A41,Def6;
consider h1 being Function such that
A49: (Frege f).g1 = h1 and
A50: dom h1 = dom f & for x st x in dom h1 holds h1.x = (
uncurry f).(x,g1.x) by A9,A38,A44,Def6;
now
let a be object;
assume
A51: a in dom f;
reconsider g = f.a as Function;
A52: a in dom f by A51;
then
A53: dom g = (doms f).a by Th18;
then
A54: g2.a in dom g by A1,A43,A51;
A55: g1.a in dom g by A1,A46,A51,A53;
h2.a = (uncurry f).(a,g2.a) by A48,A51;
then
A56: h2.a = g.(g2.a) by A52,A54,FUNCT_5:38;
g in rng f by A52,FUNCT_1:def 3;
then
A57: g is one-to-one by A37;
h1.a = (uncurry f).(a,g1.a) by A50,A51;
then h1.a = g.(g1.a) by A52,A55,FUNCT_5:38;
hence g1.a = g2.a by A40,A44,A41,A49,A47,A55,A54,A56,A57;
end;
hence thesis by A1,A44,A45,A41,A42,FUNCT_1:2;
end;
begin
theorem
<:{}:> = {} & Frege{} = {} .--> {}
proof
A1: dom doms {} = {}" {} by Def1,RELAT_1:38;
then
A2: product doms {} = {{}} by CARD_3:10,RELAT_1:41;
A3: now
let x be object;
assume
A4: x in {{}};
then
A5: x = {} by TARSKI:def 1;
then
ex h st (Frege{}).{} = h & dom h = dom {} & for x st x in
dom h holds h.x = (uncurry {}).(x,{} .x) by A2,A4,Def6;
hence (Frege{}).x = {} by A5;
end;
A6: meet({} qua set) = {} by SETFAM_1:def 1;
rng doms {} = {} by A1,RELAT_1:38,41;
then dom <:{}:> = {} by A6,Th25;
hence <:{}:> = {};
dom Frege{} = product doms {} by Def6;
hence thesis by A2,A3,FUNCOP_1:11;
end;
theorem
X <> {} implies dom <:X --> f:> = dom f & for x st x in dom f holds <:
X --> f:>.x = X --> f.x
proof
assume
A1: X <> {};
thus
A2: dom <:X --> f:> = meet doms (X --> f) by Th25
.= meet (X --> dom f) by Th20
.= dom f by A1,Th23;
A3: rng <:X --> f:> c= product rngs (X --> f) & rngs (X --> f) = X --> rng f
by Th20,Th25;
let x;
assume
A4: x in dom f;
then <:X --> f:>.x in rng <:X --> f:> by A2,FUNCT_1:def 3;
then consider g such that
A5: <:X --> f:>.x = g and
A6: dom g = dom (X --> rng f) and
for y being object st y in dom (X --> rng f) holds g.y in (X --> rng f).y
by A3,
CARD_3:def 5;
A7: dom g = X by A6;
A8: dom (X --> f) = X;
A9: now
let y be object;
assume
A10: y in X;
then g.y = (uncurry (X --> f)).(y,x) & (X --> f).y = f by A2,A4,A5,A7,Th26,
FUNCOP_1:7;
then g.y = f.x by A4,A8,A10,FUNCT_5:38;
hence g.y = (X --> f.x).y by A10,FUNCOP_1:7;
end;
thus thesis by A5,A7,A9;
end;
theorem
dom Frege(X-->f) = Funcs(X,dom f) & rng Frege(X-->f) = Funcs(X,rng f)
& for g st g in Funcs(X,dom f) holds (Frege(X-->f)).g = f*g
proof
A1: product (X --> dom f) = Funcs(X, dom f) by CARD_3:11;
A2: doms (X --> f) = X --> dom f by Th20;
rngs (X --> f) = X --> rng f & product (X --> rng f) = Funcs(X, rng f)
by Th20,CARD_3:11;
hence dom Frege(X-->f) = Funcs(X,dom f) & rng Frege(X-->f) = Funcs(X,rng f)
by A2,A1,Def6,Th33;
let g;
assume
A3: g in Funcs(X,dom f);
then consider h such that
A4: (Frege(X-->f)).g = h and
A5: dom h = dom (X --> f) and
A6: for x st x in dom h holds h.x = (uncurry (X --> f)).(x,g.x) by A2,A1,Def6;
A7: dom h = X by A5;
A8: ex g9 being Function st g = g9 & dom g9 = X & rng g9 c= dom f by A3,
FUNCT_2:def 2;
then
A9: dom (f*g) = X by RELAT_1:27;
A10: dom (X --> f) = X;
now
let x be object;
assume
A11: x in X;
then
A12: h.x = (uncurry (X --> f)).(x,g.x) & (X --> f).x = f by A6,A7,FUNCOP_1:7;
g.x in rng g & (f*g).x = f.(g.x) by A8,A9,A11,FUNCT_1:12,def 3;
hence (f*g).x = h.x by A8,A10,A11,A12,FUNCT_5:38;
end;
hence thesis by A4,A7,A9,FUNCT_1:2;
end;
theorem Th38:
dom f = X & dom g = X & (for x st x in X holds f.x,g.x
are_equipotent) implies product f,product g are_equipotent
proof
assume that
A1: dom f = X and
A2: dom g = X and
A3: for x st x in X holds f.x,g.x are_equipotent;
defpred P[object,object] means
ex f1 st $2 = f1 & f1 is one-to-one & dom f1 = f.$1
& rng f1 = g.$1;
A4: for x being object st x in X ex y being object st P[x,y]
proof
let x be object;
assume x in X;
then f.x,g.x are_equipotent by A3;
then ex h st h is one-to-one & dom h = f.x & rng h = g.x;
hence thesis;
end;
consider h such that
A5: dom h = X &
for x being object st x in X holds P[x,h.x] from CLASSES1:sch 1(A4);
h is Function-yielding
proof let x be object;
assume x in dom h;
then P[x,h.x] by A5;
hence h.x is Function;
end;
then reconsider h as Function-yielding Function;
A6: now
let x be object;
assume
A7: x in X;
then
ex f1 st h.x = f1 & f1 is one-to-one & dom f1 = f.x & rng f1 = g.x by A5;
hence (rngs h).x = g.x by A5,A7,Th18;
end;
A8: dom h = X by A5;
then dom rngs h = X by Def2;
then
A9: rngs h = g by A2,A6;
A10: now
let x be object;
assume
A11: x in X;
then
ex f1 st h.x = f1 & f1 is one-to-one & dom f1 = f.x & rng f1 = g.x by A5;
hence (doms h).x = f.x by A5,A11,Th18;
end;
dom doms h = X by A8,Def1;
then
A12: doms h = f by A1,A10;
now
per cases;
suppose
{} in rng h;
then consider x being object such that
A13: x in X and
A14: {} = h.x by A5,FUNCT_1:def 3;
A15: ex f1 st {} = f1 & f1 is one-to-one & dom f1 = f.x & rng f1 = g.x
by A5,A13,A14;
then {} in rng f by A1,A13,FUNCT_1:def 3;
then
A16: product f = {} by CARD_3:26;
{} in rng g by A2,A13,A15,FUNCT_1:def 3,RELAT_1:38;
hence thesis by A16,CARD_3:26;
end;
suppose
A17: not {} in rng h;
A18: now
let f1;
assume f1 in rng h;
then consider x being object such that
A19: x in X and
A20: f1 = h.x by A5,FUNCT_1:def 3;
ex f1 st h.x = f1 & f1 is one-to-one & dom f1 = f.x & rng f1 = g.
x by A5,A19;
hence f1 is one-to-one by A20;
end;
thus thesis
proof
take Frege h;
thus thesis by A12,A9,A17,A18,Def6,Th33,Th34;
end;
end;
end;
hence thesis;
end;
theorem Th39:
dom f = dom h & dom g = rng h & h is one-to-one & (for x st x in
dom h holds f.x, g.(h.x) are_equipotent) implies product f,product g
are_equipotent
proof
set X = dom f;
assume that
A1: dom f = dom h and
A2: dom g = rng h and
A3: h is one-to-one and
A4: for x st x in dom h holds f.x,g.(h.x) are_equipotent;
A5: h*(h") = id dom g by A2,A3,FUNCT_1:39;
A6: dom (g*h) = dom f by A1,A2,RELAT_1:27;
now
let x;
assume
A7: x in dom f;
then f.x,g.(h.x) are_equipotent by A1,A4;
hence f.x,(g*h).x are_equipotent by A6,A7,FUNCT_1:12;
end;
then
A8: product f,product (g*h) are_equipotent by A6,Th38;
defpred P[object,object] means ex f1 st $1 = f1 & $2 = f1*(h");
A9: for x being object st x in product (g*h) ex y being object st P[x,y]
proof
let x be object;
assume x in product (g*h);
then ex f1 st x = f1 & dom f1 = dom (g*h) &
for y being object st y in dom (g*h) holds
f1.y in (g*h).y by CARD_3:def 5;
then consider f1 such that
A10: x = f1;
f1*(h") = f1*(h");
hence thesis by A10;
end;
consider F being Function such that
A11: dom F = product (g*h) &
for x being object st x in product (g*h) holds P[x,F.x]
from CLASSES1:sch 1(A9);
A12: rng (h") = X by A1,A3,FUNCT_1:33;
A13: F is one-to-one
proof
let x,y be object;
assume that
A14: x in dom F and
A15: y in dom F and
A16: F.x = F.y;
consider g2 being Function such that
A17: y = g2 and
A18: F.y = g2*(h") by A11,A15;
A19: dom g2 = X by A6,A11,A15,A17,CARD_3:9;
consider g1 being Function such that
A20: x = g1 and
A21: F.x = g1*(h") by A11,A14;
dom g1 = X by A6,A11,A14,A20,CARD_3:9;
hence thesis by A12,A16,A20,A21,A17,A18,A19,FUNCT_1:86;
end;
A22: (g*h)*(h") = g*(h*(h")) & g*id dom g = g by RELAT_1:36,52;
A23: product g c= rng F
proof
let x be object;
assume x in product g;
then consider f1 such that
A24: x = f1 and
A25: dom f1 = dom g and
A26: for z being object st z in dom g holds f1.z in g.z by CARD_3:def 5;
A27: dom (f1*h) = X by A1,A2,A25,RELAT_1:27;
now
let z be object;
assume
A28: z in X;
then
A29: h.z in dom g by A1,A2,FUNCT_1:def 3;
A30: (h").(h.z) = z by A1,A3,A28,FUNCT_1:34;
(f1*h).z = f1.(h.z) by A27,A28,FUNCT_1:12;
then (f1*h).z in ((g*h)*(h")).(h.z) by A5,A22,A26,A29;
hence (f1*h).z in (g*h).z by A5,A22,A29,A30,FUNCT_1:12;
end;
then
A31: f1*h in product (g*h) by A6,A27,CARD_3:def 5;
then ex f2 st f1*h = f2 & F.(f1*h) = f2*(h") by A11;
then F.(f1*h) = f1*id dom g by A5,RELAT_1:36
.= x by A24,A25,RELAT_1:51;
hence thesis by A11,A31,FUNCT_1:def 3;
end;
A32: dom (h") = rng h by A3,FUNCT_1:33;
rng F c= product g
proof
let x be object;
assume x in rng F;
then consider y being object such that
A33: y in dom F and
A34: x = F.y by FUNCT_1:def 3;
consider f1 such that
A35: y = f1 and
A36: dom f1 = X and
A37: for z being object st z in X holds f1.z in (g*h).z
by A6,A11,A33,CARD_3:def 5;
A38: dom (f1*(h")) = dom g by A2,A12,A32,A36,RELAT_1:27;
A39: now
let z be object;
assume
A40: z in dom g;
then
A41: (h").z in X by A2,A12,A32,FUNCT_1:def 3;
g.z = (g*h).((h").z) & (f1*(h")).z = f1.((h").z) by A5,A22,A38,A40,
FUNCT_1:12;
hence (f1*(h")).z in g.z by A37,A41;
end;
ex f1 st y = f1 & F.y = f1*(h") by A11,A33;
hence thesis by A34,A35,A38,A39,CARD_3:def 5;
end;
then rng F = product g by A23;
then product (g*h),product g are_equipotent by A11,A13;
hence thesis by A8,WELLORD2:15;
end;
theorem
dom f = X implies product f,product (f*P) are_equipotent
proof
assume
A1: dom f = X;
A2: rng P = X by FUNCT_2:def 3;
dom P = X by FUNCT_2:52;
then
A3: dom (f*P) = X by A1,A2,RELAT_1:27;
A4: rng (P") = X by FUNCT_2:def 3;
A5: dom (P") = X by FUNCT_2:52;
now
let x;
assume
A6: x in dom (P");
then P".x in X by A4,FUNCT_1:def 3;
then (f*P).(P".x) = f.(P.(P".x)) by A3,FUNCT_1:12
.= f.x by A5,A2,A6,FUNCT_1:35;
hence f.x,(f*P).(P".x) are_equipotent;
end;
hence thesis by A1,A5,A4,A3,Th39;
end;
begin
definition
let f,X;
func Funcs(f,X) -> Function means
:Def7:
dom it = dom f & for x being object st x in dom f holds it.x = Funcs(f.x,X);
existence
proof
deffunc F(object) = Funcs(f.$1,X);
consider F be Function such that
A1: dom F = dom f &
for x being object st x in dom f holds F.x = F(x) from FUNCT_1:sch 3;
take F;
thus thesis by A1;
end;
uniqueness
proof
let f1,f2 such that
A2: dom f1 = dom f and
A3: for x being object st x in dom f holds f1.x = Funcs(f.x,X) and
A4: dom f2 = dom f and
A5: for x being object st x in dom f holds f2.x = Funcs(f.x,X);
now
let x be object;
assume
A6: x in dom f;
then f1.x = Funcs(f.x,X) by A3;
hence f1.x = f2.x by A5,A6;
end;
hence thesis by A2,A4;
end;
end;
theorem
not {} in rng f implies Funcs(f,{}) = dom f --> {}
proof
assume
A1: not {} in rng f;
A2: now
let x be object;
assume
x in dom f;
then
A4: f.x <> {} by A1,FUNCT_1:def 3;
thus (dom f --> {}).x = {}
.= Funcs(f.x,{}) by A4;
end;
dom (dom f --> {}) = dom f;
hence thesis by A2,Def7;
end;
theorem
Funcs({},X) = {}
proof
dom Funcs({},X) = dom {} by Def7;
hence thesis;
end;
theorem
Funcs(X --> Y, Z) = X --> Funcs(Y,Z)
proof
A1: X = dom (X --> Y);
A2: now
let x be object;
assume
A3: x in X;
then Funcs(X --> Y, Z).x = Funcs((X --> Y).x,Z) by A1,Def7;
hence Funcs(X --> Y, Z).x = Funcs(Y,Z) by A3,FUNCOP_1:7;
end;
dom Funcs(X --> Y, Z) = dom (X --> Y) by Def7;
hence thesis by A2,FUNCOP_1:11;
end;
Lm3: for x,y,z being object holds
[x,y] in dom f & g = (curry f).x & z in dom g implies [x,z] in dom f
proof let x,y,z be object;
assume [x,y] in dom f;
then x in proj1 dom f by XTUPLE_0:def 12;
then
A1: ex g9 being Function st (curry f).x = g9 & dom g9 = proj2 (dom f /\ [:{x
},proj2 dom f:]) & for y st y in dom g9 holds g9.y = f.(x,y) by FUNCT_5:def 1
;
assume g = (curry f).x & z in dom g;
then consider y being object such that
A2: [y,z] in dom f /\ [:{x}, proj2 dom f:] by A1,XTUPLE_0:def 13;
[y,z] in [:{x}, proj2 dom f:] by A2,XBOOLE_0:def 4;
then
A3: y in {x} by ZFMISC_1:87;
[y,z] in dom f by A2,XBOOLE_0:def 4;
hence thesis by A3,TARSKI:def 1;
end;
theorem
Funcs(Union disjoin f,X),product Funcs(f,X) are_equipotent
proof
defpred P[object,object] means
ex g,h st $1 = g & $2 = h & dom h = dom f & for y
st y in dom f holds (f.y = {} implies h.y = {}) & (f.y <> {} implies h.y = (
curry' g).y);
A1: for x being object st x in Funcs(Union disjoin f, X)
ex z being object st P[x,z]
proof
defpred P[object] means f.$1 = {};
deffunc F(object) = {};
let x be object;
assume x in Funcs(Union disjoin f, X);
then consider g such that
A2: x = g and
dom g = Union disjoin f and
rng g c= X by FUNCT_2:def 2;
deffunc G(object) = (curry' g).$1;
consider h such that
A3: dom h = dom f &
for y being object st y in dom f holds (P[y] implies h.y =
F(y)) & (not P[y] implies h.y = G(y)) from PARTFUN1:sch 1;
take z = h, g, h;
thus
x = g & z = h & dom h = dom f & for y
st y in dom f holds (f.y = {} implies h.y = {}) &
(f.y <> {} implies h.y = (
curry' g).y) by A2,A3;
end;
consider F being Function such that
A4: dom F = Funcs(Union disjoin f, X) &
for x being object st x in Funcs(Union
disjoin f, X) holds P[x,F.x] from CLASSES1:sch 1(A1);
take F;
thus F is one-to-one
proof
let x,y be object;
assume that
A5: x in dom F and
A6: y in dom F and
A7: F.x = F.y;
A8: ex f2 being Function st y = f2 & dom f2 = Union disjoin f & rng f2 c=
X by A4,A6,FUNCT_2:def 2;
consider g1,h1 being Function such that
A9: x = g1 and
A10: F.x = h1 and
dom h1 = dom f and
A11: for y st y in dom f holds (f.y = {} implies h1.y = {}) & (f.y <>
{} implies h1.y = (curry' g1).y) by A4,A5;
consider g2,h2 being Function such that
A12: y = g2 and
A13: F.y = h2 and
dom h2 = dom f and
A14: for y st y in dom f holds (f.y = {} implies h2.y = {}) & (f.y <>
{} implies h2.y = (curry' g2).y) by A4,A6;
A15: ex f1 being Function st x = f1 & dom f1 = Union disjoin f & rng f1 c=
X by A4,A5,FUNCT_2:def 2;
now
let z be object;
assume
A16: z in Union disjoin f;
then
A17: z = [z`1,z`2] by CARD_3:22;
A18: z`2 in dom f & z`1 in f.(z`2) by A16,CARD_3:22;
then
A19: h2.z`2 = (curry' g2).z`2 by A14;
then reconsider
g91 = h1.z`2, g92 = h2.z`2 as Function by A7,A10,A13;
A20: g2.(z`1,z`2) = g92.z`1 by A8,A12,A16,A17,A19,FUNCT_5:22;
h1.z`2 = (curry' g1).z`2 by A11,A18;
then g1.(z`1,z`2) = g91.z`1 by A15,A9,A16,A17,FUNCT_5:22;
hence g1.z = g2.z by A7,A10,A13,A17,A20;
end;
hence thesis by A15,A8,A9,A12,FUNCT_1:2;
end;
thus dom F = Funcs(Union disjoin f, X) by A4;
thus rng F c= product Funcs(f,X)
proof
let y be object;
assume y in rng F;
then consider x being object such that
A21: x in dom F and
A22: y = F.x by FUNCT_1:def 3;
consider g,h such that
A23: x = g and
A24: F.x = h and
A25: dom h = dom f and
A26: for y st y in dom f holds (f.y = {} implies h.y = {}) & (f.y <>
{} implies h.y = (curry' g).y) by A4,A21;
A27: ex f1 being Function st x = f1 & dom f1 = Union disjoin f & rng f1 c=
X by A4,A21,FUNCT_2:def 2;
A28: now
let z be object;
assume z in dom Funcs(f,X);
then
A29: z in dom f by Def7;
then
A30: Funcs(f,X).z = Funcs(f.z,X) by Def7;
A31: now
set a = the Element of f.z;
assume
A32: f.z <> {};
[a,z]`1 = a & [a,z]`2 = z;
then
A33: [a,z] in Union disjoin f by A29,A32,CARD_3:22;
reconsider k = (curry' g).z as Function;
A34: z in dom curry' g by A23,A27,A33,FUNCT_5:21;
then rng k c= rng g by FUNCT_5:34;
then
A35: rng k c= X by A23,A27;
A36: dom k = proj1 (dom g /\ [:proj1 dom g,{z}:]) by A34,FUNCT_5:34;
A37: dom k = f.z
proof
thus dom k c= f.z
proof
let b be object;
assume b in dom k;
then consider c being object such that
A38: [b,c] in dom g /\ [:proj1 dom g,{z}:] by A36,XTUPLE_0:def 12;
[b,c] in [:proj1 dom g,{z}:] by A38,XBOOLE_0:def 4;
then
A39: c in {z} by ZFMISC_1:87;
A40: [b,c]`1 = b & [b,c]`2 = c;
[b,c] in dom g by A38,XBOOLE_0:def 4;
then b in f.c by A23,A27,A40,CARD_3:22;
hence thesis by A39,TARSKI:def 1;
end;
let b be object such that
A41: b in f.z;
A42: z in {z} by TARSKI:def 1;
[b,z]`1 = b & [b,z]`2 = z;
then
A43: [b,z] in dom g by A23,A27,A29,A41,CARD_3:22;
then b in proj1 dom g by XTUPLE_0:def 12;
then [b,z] in [:proj1 dom g,{z}:] by A42,ZFMISC_1:87;
then [b,z] in dom g /\ [:proj1 dom g,{z}:] by A43,XBOOLE_0:def 4;
hence thesis by A36,XTUPLE_0:def 12;
end;
h.z = k by A26,A29,A32;
hence h.z in Funcs(f,X).z by A30,A35,A37,FUNCT_2:def 2;
end;
now
assume f.z = {};
then h.z = {} & Funcs(f,X).z = {{}} by A26,A29,A30,FUNCT_5:57;
hence h.z in Funcs(f,X).z by TARSKI:def 1;
end;
hence h.z in Funcs(f,X).z by A31;
end;
dom h = dom Funcs(f,X) by A25,Def7;
hence thesis by A22,A24,A28,CARD_3:def 5;
end;
let x be object;
assume x in product Funcs(f,X);
then consider s being Function such that
A44: x = s and
A45: dom s = dom Funcs(f,X) and
A46: for z being object st z in dom Funcs(f,X) holds s.z in Funcs(f,X).z
by CARD_3:def 5;
A47: dom s = dom f by A45,Def7;
A48: uncurry' s = ~uncurry s by FUNCT_5:def 4;
A49: dom uncurry' s = Union disjoin f
proof
thus dom uncurry' s c= Union disjoin f
proof
let z be object;
assume
A50: z in dom uncurry' s;
then consider z1, z2 being object such that
A51: z = [z1,z2] by A48,Th2;
A52: z`1 = z1 & z`2 = z2 by A51;
[z2,z1] in dom uncurry s by A48,A50,A51,FUNCT_4:42;
then consider a being object, u being Function, b being object
such that
A53: [z2,z1] = [a,b] and
A54: a in dom s and
A55: u = s.a and
A56: b in dom u by FUNCT_5:def 2;
A57: [a,b]`1 = a & [z2,z1]`1 = z2;
u in Funcs(f,X).a & Funcs(f,X).a = Funcs(f.a,X) by A45,A46,A47,A54,A55
,Def7;
then
A58: ex j being Function st u = j & dom j = f.z2 & rng j c= X by A53,A57,
FUNCT_2:def 2;
[a,b]`2 = b & [z2,z1]`2 = z1;
hence thesis by A47,A51,A53,A54,A56,A52,A57,A58,CARD_3:22;
end;
let z be object;
assume
A59: z in Union disjoin f;
then
A60: z`1 in f.z`2 & z = [z`1,z`2] by CARD_3:22;
A61: z`2 in dom f by A59,CARD_3:22;
then
s.z`2 in Funcs(f,X).z`2 & Funcs(f,X).z`2 = Funcs(f.z`2,X) by A45,A46,A47
,Def7;
then ex j being Function st s.z`2 = j & dom j = f.z`2 & rng j c= X by
FUNCT_2:def 2;
hence thesis by A47,A61,A60,FUNCT_5:39;
end;
rng uncurry' s c= X
proof
let d be object;
assume d in rng uncurry' s;
then consider z being object such that
A62: z in dom uncurry' s and
A63: d = (uncurry' s).z by FUNCT_1:def 3;
consider z1, z2 being object such that
A64: z = [z1,z2] by A48,A62,Th2;
[z2,z1] in dom uncurry s by A48,A62,A64,FUNCT_4:42;
then consider a being object, u being Function, b being object such that
A65: [z2,z1] = [a,b] and
A66: a in dom s & u = s.a and
A67: b in dom u by FUNCT_5:def 2;
A68: [a,b]`1 = a & [z2,z1]`1 = z2;
u in Funcs(f,X).a & Funcs(f,X).a = Funcs(f.a,X) by A45,A46,A47,A66,Def7;
then
A69: ex j being Function st u = j & dom j = f.z2 & rng j c= X by A65,A68,
FUNCT_2:def 2;
A70: [a,b]`2 = b & [z2,z1]`2 = z1;
(uncurry' s).(b,a) = u.b by A66,A67,FUNCT_5:39;
then d in rng u by A63,A64,A65,A67,A68,A70,FUNCT_1:def 3;
hence thesis by A69;
end;
then
A71: uncurry' s in dom F by A4,A49,FUNCT_2:def 2;
then consider g,h such that
A72: uncurry' s = g and
A73: F.uncurry' s = h and
A74: dom h = dom f and
A75: for y st y in dom f holds (f.y = {} implies h.y = {}) & (f.y <> {}
implies h.y = (curry' g).y) by A4;
now
let z be object;
assume
A76: z in dom f;
then s.z in Funcs(f,X).z & Funcs(f,X).z = Funcs(f.z,X) by A45,A46,A47,Def7;
then consider v being Function such that
A77: s.z = v and
A78: dom v = f.z and
rng v c= X by FUNCT_2:def 2;
A79: now
set a = the Element of f.z;
assume
A80: f.z <> {};
then
A81: [a,z] in dom uncurry' s by A47,A76,A77,A78,FUNCT_5:39;
reconsider j = (curry' uncurry' s).z as Function;
A82: j = (curry ~uncurry' s).z by FUNCT_5:def 3;
A83: ~uncurry' s = uncurry s by Th4;
then
A84: [z,a] in dom uncurry s by A81,FUNCT_4:42;
A85: dom j = dom v
proof
thus dom j c= dom v
proof
let b be object;
assume b in dom j;
then [z,b] in dom uncurry s by A82,A83,A84,Lm3;
then consider
a1 being object, g1 being Function, a2 being object such that
A86: [z,b] = [a1,a2] and
a1 in dom s and
A87: g1 = s.a1 & a2 in dom g1 by FUNCT_5:def 2;
z = a1 by A86,XTUPLE_0:1;
hence thesis by A77,A86,A87,XTUPLE_0:1;
end;
let b be object;
assume b in dom v;
then [z,b] in dom uncurry s by A47,A76,A77,FUNCT_5:38;
hence thesis by A82,A83,FUNCT_5:20;
end;
now
let b be object;
assume b in f.z;
then
A88: [z,b] in dom uncurry s by A78,A82,A83,A84,A85,Lm3;
then consider a1 being object, g1 being Function, a2 being object
such that
A89: [z,b] = [a1,a2] and
A90: a1 in dom s & g1 = s.a1 & a2 in dom g1 by FUNCT_5:def 2;
A91: j.b = (uncurry s).(z,b) by A82,A83,A88,FUNCT_5:20;
z = a1 & b = a2 by A89,XTUPLE_0:1;
hence j.b = v.b by A77,A90,A91,FUNCT_5:38;
end;
then v = j by A78,A85;
hence s.z = h.z by A72,A75,A76,A77,A80;
end;
f.z = {} implies s.z = {} & h.z = {} by A75,A76,A77,A78;
hence s.z = h.z by A79;
end;
then h = s by A47,A74;
hence thesis by A44,A71,A73,FUNCT_1:def 3;
end;
definition
let X,f;
func Funcs(X,f) -> Function means
: Def8:
dom it = dom f & for x being object st x in dom f holds it.x = Funcs(X,f.x);
existence
proof
deffunc F(object) = Funcs(X,f.$1);
ex F be Function st dom F = dom f &
for x being object st x in dom f holds F.x = F(
x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let f1,f2 such that
A1: dom f1 = dom f and
A2: for x being object st x in dom f holds f1.x = Funcs(X,f.x) and
A3: dom f2 = dom f and
A4: for x being object st x in dom f holds f2.x = Funcs(X,f.x);
now
let x be object;
assume
A5: x in dom f;
then f1.x = Funcs(X,f.x) by A2;
hence f1.x = f2.x by A4,A5;
end;
hence thesis by A1,A3;
end;
end;
Lm4: f <> {} & X <> {} implies product Funcs(X,f),Funcs(X,product f)
are_equipotent
proof
defpred P[object,object] means
ex g being Function-yielding Function st $1 = g & $2 = <:g:>;
assume that
A1: f <> {} and
A2: X <> {};
A3: for x being object st x in product Funcs(X,f) ex y being object st P[x,y]
proof
let x be object;
assume x in product Funcs(X,f);
then consider g such that
A4: x = g & dom g = dom Funcs(X,f) &
for x being object st x in dom Funcs(X,f)
holds g.x in Funcs(X,f).x by CARD_3:def 5;
g is Function-yielding
proof let x be object;
assume
A5: x in dom g;
then
A6: g.x in Funcs(X,f).x by A4;
x in dom f by A5,A4,Def8;
then g.x in Funcs(X,f.x) by A6,Def8;
hence g.x is Function;
end;
then reconsider g = x as Function-yielding Function by A4;
reconsider y = <:g:> as set;
take y, g;
thus thesis;
end;
consider F being Function such that
A7: dom F = product Funcs(X,f) &
for x being object st x in product Funcs(X,f) holds P[x,F.x]
from CLASSES1:sch 1(A3);
take F;
A8:
for g being Function-yielding Function
st g in product Funcs(X,f)
holds dom <:g:> = X & rng g = rng g & rng <:g:> c= product f
proof let g be Function-yielding Function;
A9: dom Funcs(X,f) = dom f by Def8;
assume
A10: g in product Funcs(X,f);
then
A11: dom g = dom Funcs(X,f) by CARD_3:9;
A12: now
let z be object;
assume
A13: z in dom f;
then g.z in Funcs(X,f).z & Funcs(X,f).z = Funcs(X,f.z) by A10,A9,Def8,
CARD_3:9;
then ex h st g.z = h & dom h = X & rng h c= f.z by FUNCT_2:def 2;
hence (dom f --> X).z = proj1 (g.z) by A13,FUNCOP_1:7;
end;
dom (dom f --> X) = dom f;
then doms g = dom f --> X by A11,A9,A12,Def1;
then meet doms g = X by A1,Th23;
hence
A14: dom <:g:> = X & rng g = rng g by Th25;
let y be object;
assume y in rng <:g:>;
then consider x being object such that
A15: x in dom <:g:> and
A16: y = <:g:>.x by FUNCT_1:def 3;
reconsider h = y as Function by A16;
A17: dom h = dom f by A11,A9,A15,A16,Th26;
now
let z be object;
assume
A18: z in dom f;
then
A19: (uncurry g).(z,x) = h.z by A15,A16,A17,Th26;
g.z in Funcs(X,f).z & Funcs(X,f).z = Funcs(X,f.z) by A10,A9,A18,Def8,
CARD_3:9;
then consider j being Function such that
A20: g.z = j and
A21: dom j = X and
A22: rng j c= f.z by FUNCT_2:def 2;
A23: j.x in rng j by A14,A15,A21,FUNCT_1:def 3;
(uncurry g).(z,x) = j.x by A11,A9,A14,A15,A18,A20,A21,FUNCT_5:38;
hence h.z in f.z by A22,A19,A23;
end;
hence thesis by A17,CARD_3:def 5;
end;
thus F is one-to-one
proof
let x,y be object;
assume that
A24: x in dom F and
A25: y in dom F and
A26: F.x = F.y and
A27: x <> y;
consider gy being Function-yielding Function such that
A28: y = gy and
A29: F.y = <:gy:> by A7,A25;
consider gx being Function-yielding Function such that
A30: x = gx and
A31: F.x = <:gx:> by A7,A24;
A32: dom gx = dom Funcs(X,f) by A7,A24,A30,CARD_3:9;
A33: dom Funcs(X,f) = dom f by Def8;
A34: dom gy = dom Funcs(X,f) by A7,A25,A28,CARD_3:9;
now
let z be object;
assume
A35: z in dom f;
then
A36: Funcs(X,f).z = Funcs(X,f.z) by Def8;
gy.z in Funcs(X,f).z by A7,A25,A28,A33,A35,CARD_3:9;
then consider hy being Function such that
A37: gy.z = hy & dom hy = X and
rng hy c= f.z by A36,FUNCT_2:def 2;
gx.z in Funcs(X,f).z by A7,A24,A30,A33,A35,CARD_3:9;
then consider hx being Function such that
A38: gx.z = hx & dom hx = X and
rng hx c= f.z by A36,FUNCT_2:def 2;
A39: dom <:gx:> = X by A7,A8,A24,A30;
now
let b be object;
assume
A40: b in X;
reconsider fx = <:gx:>.b as Function;
A41: (uncurry gx).(z,b) = hx.b & (uncurry gy).(z,b) = hy.b by A32,A34,A33
,A35,A38,A37,A40,FUNCT_5:38;
A42: dom fx = dom gx by A39,A40,Th26;
then fx.z = (uncurry gx).(z,b) by A32,A33,A35,A39,A40,Th26;
hence hx.b = hy.b by A26,A31,A29,A32,A33,A35,A39,A40,A42,A41,Th26;
end;
hence gx.z = gy.z by A38,A37;
end;
hence thesis by A27,A30,A28,A32,A34,A33,FUNCT_1:2;
end;
thus dom F = product Funcs(X,f) by A7;
thus rng F c= Funcs(X, product f)
proof
let y be object;
assume y in rng F;
then consider x being object such that
A43: x in dom F and
A44: y = F.x by FUNCT_1:def 3;
consider g being Function-yielding Function such that
A45: x = g and
A46: y = <:g:> by A7,A43,A44;
dom <:g:> = X & rng <:g:> c= product f by A7,A8,A43,A45;
hence thesis by A46,FUNCT_2:def 2;
end;
let y be object;
assume y in Funcs(X, product f);
then consider h being Function such that
A47: y = h and
A48: dom h = X and
A49: rng h c= product f by FUNCT_2:def 2;
h is Function-yielding
proof let x be object;
assume x in dom h;
then h.x in rng h by FUNCT_1:3;
then h.x is Element of product f by A49;
hence thesis;
end;
then reconsider h as Function-yielding Function;
set g = <:h:>;
A50: now
let z be object;
assume
A51: z in X;
then h.z in rng h by A48,FUNCT_1:def 3;
then
A52: ex j being Function st h.z = j & dom j = dom f &
for x being object st x in dom f
holds j.x in f.x by A49,CARD_3:def 5;
thus (X --> dom f).z = dom f by A51,FUNCOP_1:7
.= (doms h).z by A48,A51,A52,Th18;
end;
A53: meet doms h = dom g by Th25;
dom doms h = dom h & dom (dom h --> dom f) = dom h by Def1;
then X --> dom f = doms h by A48,A50;
then
A54: dom g = dom f by A2,A53,Th23;
A55: now
let z be object;
assume
A56: z in dom f;
reconsider i = g.z as Function;
A57: dom i = X by A48,A54,A56,Th26;
rng i c= f.z
proof
let x be object;
assume x in rng i;
then consider a being object such that
A58: a in dom i and
A59: x = i.a by FUNCT_1:def 3;
h.a in rng h by A48,A57,A58,FUNCT_1:def 3;
then consider j being Function such that
A60: h.a = j & dom j = dom f and
A61: for x being object st x in dom f holds j.x in f.x by A49,CARD_3:def 5;
i.a = (uncurry h).(a,z) by A54,A56,A58,Th26
.= j.z by A48,A56,A57,A58,A60,FUNCT_5:38;
hence thesis by A56,A59,A61;
end;
then g.z in Funcs(X,f.z) by A57,FUNCT_2:def 2;
hence g.z in Funcs(X,f).z by A56,Def8;
end;
A62: meet doms g = dom <:g:> by Th25;
product f c= Funcs(dom f, Union f) by Th1;
then
A63: rng h c= Funcs(dom f, Union f) by A49;
then
A64: dom uncurry h = [:dom h, dom f:] by FUNCT_5:26;
dom f = dom Funcs(X,f) by Def8;
then
A65: g in product Funcs(X,f) by A54,A55,CARD_3:def 5;
then
A66: ex g9 being Function-yielding Function st g = g9 & F.g = <:g9:> by A7;
dom uncurry' h = [:dom f, dom h:] by A63,FUNCT_5:26;
then
A67: (uncurry' h)|([:meet doms h, dom h:] qua set) = uncurry' h by A53,A54;
A68: uncurry' h = ~uncurry h & curry ~uncurry h = curry' uncurry h by
FUNCT_5:def 3,def 4;
dom <:g:> = X by A8,A65;
then
A69: (uncurry h)|([:meet doms g, dom g:] qua set) = uncurry h by A48,A54,A64
,A62;
uncurry' curry' uncurry h = uncurry h by A64,FUNCT_5:49;
then <:g:> = h by A1,A63,A67,A69,A68,FUNCT_5:48;
hence thesis by A7,A47,A65,A66,FUNCT_1:def 3;
end;
theorem Th45:
Funcs({},f) = dom f --> {{}}
proof
A1: now
let x be object;
assume x in dom f;
hence Funcs({},f).x = Funcs({} qua set,f.x) by Def8
.= {{}} by FUNCT_5:57;
end;
dom Funcs({},f) = dom f by Def8;
hence thesis by A1,FUNCOP_1:11;
end;
theorem Th46:
Funcs(X,{}) = {}
proof
dom Funcs(X,{}) = dom {} by Def8;
hence thesis;
end;
theorem
Funcs(X, Y --> Z) = Y --> Funcs(X,Z)
proof
A1: Y = dom (Y --> Z);
A2: now
let x be object;
assume
A3: x in Y;
then Funcs(X, Y --> Z).x = Funcs(X, (Y --> Z).x) by A1,Def8;
hence Funcs(X, Y --> Z).x = Funcs(X,Z) by A3,FUNCOP_1:7;
end;
dom Funcs(X, Y --> Z) = dom (Y --> Z) by Def8;
hence thesis by A2,FUNCOP_1:11;
end;
theorem
product Funcs(X,f),Funcs(X, product f) are_equipotent
proof
A1: Funcs(X, product {}) = {X --> {}} by CARD_3:10,FUNCT_5:59;
A2: product Funcs({},f) = product (dom f --> {{}}) by Th45
.= Funcs(dom f, {{}}) by CARD_3:11
.= {dom f --> {}} by FUNCT_5:59;
A3: Funcs({} qua set, product f) = {{}} & product Funcs(X,{}) = {{}} by Th46,
CARD_3:10,FUNCT_5:57;
X <> {} & f <> {} implies thesis by Lm4;
hence thesis by A2,A3,A1,CARD_1:28;
end;
begin :: Addenda
:: from PRALG_2
definition
let f be Function;
func commute f -> Function-yielding Function equals
curry' uncurry f;
coherence;
end;
theorem
for f be Function, x be set st x in dom (commute f) holds (commute f).
x is Function;
theorem Th50:
for A,B,C be set, f be Function st A <> {} & B <> {} & f in
Funcs(A,Funcs(B,C)) holds commute f in Funcs(B,Funcs(A,C))
proof
let A,B,C be set, f be Function;
assume A <> {} & B <> {} & f in Funcs(A,Funcs(B,C));
then [:A,B:] <> {} & uncurry f in Funcs([:A,B:],C) by Th11,ZFMISC_1:90;
hence thesis by Th10;
end;
theorem
for A,B,C be set, f be Function st A <> {} & B <> {} & f in Funcs(A,
Funcs(B,C)) for g,h be Function, x,y be set st x in A & y in B & f.x = g & (
commute f).y = h holds h.x = g.y & dom h = A & dom g = B & rng h c= C & rng g
c= C
proof
let A,B,C be set, f be Function;
assume that
A1: A <> {} & B <> {} and
A2: f in Funcs(A,Funcs(B,C));
set uf = uncurry f;
set cf = commute f;
let g,h be Function, x,y be set;
assume that
A3: x in A and
A4: y in B and
A5: f.x = g and
A6: (commute f).y = h;
commute f in Funcs(B,Funcs(A,C)) by A1,A2,Th50;
then
A7: ex g be Function st g = cf & dom g = B & rng g c= Funcs(A,C) by
FUNCT_2:def 2;
then cf.y in rng cf by A4,FUNCT_1:def 3;
then
A8: ex t be Function st t = h & dom t = A & rng t c= C by A6,A7,FUNCT_2:def 2;
A9: ex g be Function st g = f & dom g = A & rng g c= Funcs(B,C) by A2,
FUNCT_2:def 2;
then f.x in rng f by A3,FUNCT_1:def 3;
then
A10: ex t be Function st t = g & dom t = B & rng t c= C by A5,A9,FUNCT_2:def 2;
then [x,y] in dom uf & uf.(x,y) = g.y by A3,A4,A5,A9,FUNCT_5:38;
hence thesis by A6,A10,A8,FUNCT_5:22;
end;
theorem
for A,B,C be set, f be Function st A <> {} & B <> {} & f in Funcs(A,
Funcs(B,C)) holds commute commute f = f
proof
let A,B,C be set, f be Function;
assume that
A1: A <> {} & B <> {} and
A2: f in Funcs(A,Funcs(B,C));
A3: ex g be Function st g = f & dom g = A & rng g c= Funcs(B,C) by A2,
FUNCT_2:def 2;
set cf = commute f;
A4: commute f in Funcs(B,Funcs(A,C)) by A1,A2,Th50;
then commute cf in Funcs(A,Funcs(B,C)) by A1,Th50;
then
A5: ex h be Function st h = commute cf & dom h = A & rng h c= Funcs(B,C) by
FUNCT_2:def 2;
A6: ex g be Function st g = cf & dom g = B & rng g c= Funcs(A,C) by A4,
FUNCT_2:def 2;
for x being object st x in A holds f.x = (commute cf).x
proof
set ccf = commute cf, uf = uncurry f, ucf = uncurry cf;
let x be object;
assume
A7: x in A;
then f.x in rng f by A3,FUNCT_1:def 3;
then consider g be Function such that
A8: g = f.x & dom g = B and
rng g c= C by A3,FUNCT_2:def 2;
ccf.x in rng ccf by A5,A7,FUNCT_1:def 3;
then consider h be Function such that
A9: h = ccf.x and
A10: dom h = B and
rng h c= C by A5,FUNCT_2:def 2;
A11: for y st y in B for h be Function st h = cf.y holds x in dom h & h.x = g.y
proof
let y;
assume y in B;
then
A12: [x,y] in dom uf & uf.(x,y) = g.y by A3,A7,A8,FUNCT_5:38;
let h be Function;
assume h = cf.y;
hence thesis by A12,FUNCT_5:22;
end;
A13: for y st y in B holds [y,x] in dom ucf & ucf.(y,x) = g.y
proof
let y;
reconsider h = cf.y as Function;
assume
A14: y in B;
then x in dom h & h.x = g.y by A11;
hence thesis by A6,A14,FUNCT_5:38;
end;
for y being object st y in B holds h.y = g.y
proof
let y be object;
assume y in B;
then [y,x] in dom ucf & ucf.(y,x) = g.y by A13;
hence thesis by A9,FUNCT_5:22;
end;
hence thesis by A8,A9,A10,FUNCT_1:2;
end;
hence thesis by A3,A5;
end;
theorem
commute {} = {} by FUNCT_5:42,43;
:: from EXTENS_1
theorem
for f be Function-yielding Function holds dom doms f = dom f by Def1;
theorem
for f be Function-yielding Function holds dom rngs f = dom f by Def2;