Journal of Formalized Mathematics
Volume 3, 1991
University of Bialystok
Copyright (c) 1991 Association of Mizar Users

### Cartesian Product of Functions

by
Grzegorz Bancerek

Received September 30, 1991

MML identifier: FUNCT_6
[ Mizar article, MML identifier index ]

environ

vocabulary FUNCT_1, FUNCT_2, CARD_3, FINSEQ_1, RELAT_1, FINSEQ_2, FUNCOP_1,
PROB_1, TARSKI, FUNCT_5, BOOLE, PARTFUN1, SETFAM_1, FINSEQ_4, MCART_1,
FUNCT_6;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, NAT_1, RELAT_1,
FUNCT_1, MCART_1, FINSEQ_1, SETFAM_1, FUNCT_2, PARTFUN1, FUNCT_3,
WELLORD2, FUNCOP_1, FINSEQ_2, FUNCT_4, FUNCT_5, PROB_1, CARD_3;
constructors ENUMSET1, MCART_1, PARTFUN1, FUNCT_3, WELLORD2, FUNCOP_1, PROB_1,
FINSEQ_2, FUNCT_4, FUNCT_5, CARD_3, XBOOLE_0;
clusters SUBSET_1, RELAT_1, FUNCT_1, FUNCOP_1, FINSEQ_1, RELSET_1, ARYTM_3,
FUNCT_2, ZFMISC_1, XBOOLE_0;
requirements NUMERALS, BOOLE, SUBSET;

begin

reserve x,y,y1,y2,z,a,b,X,Y,Z,V1,V2 for set,
f,g,h,h',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 :: FUNCT_6:1
x in product <*X*> iff ex y st y in X & x = <*y*>;

theorem :: FUNCT_6:2
z in product <*X,Y*> iff ex x,y st x in X & y in Y & z = <*x,y*>;

theorem :: FUNCT_6:3
a in product <*X,Y,Z*> iff ex x,y,z st x in X & y in Y & z in
Z & a = <*x,y,z*>;

theorem :: FUNCT_6:4
product <*D*> = 1-tuples_on D;

theorem :: FUNCT_6:5
product <*D1,D2*> = { <*d1,d2*>: not contradiction };

theorem :: FUNCT_6:6
product <*D,D*> = 2-tuples_on D;

theorem :: FUNCT_6:7
product <*D1,D2,D3*> = { <*d1,d2,d3*>: not contradiction };

theorem :: FUNCT_6:8
product <*D,D,D*> = 3-tuples_on D;

theorem :: FUNCT_6:9
product (i |-> D) = i-tuples_on D;

theorem :: FUNCT_6:10
product f c= Funcs(dom f, Union f);

begin

theorem :: FUNCT_6:11
x in dom ~f implies ex y,z st x = [y,z];

theorem :: FUNCT_6:12
~([:X,Y:] --> z) = [:Y,X:] --> z;

theorem :: FUNCT_6:13
curry f = curry' ~f & uncurry f = ~uncurry' f;

theorem :: FUNCT_6:14
[:X,Y:] <> {} implies
curry ([:X,Y:] --> z) = X --> (Y --> z) &
curry' ([:X,Y:] --> z) = Y --> (X --> z);

theorem :: FUNCT_6:15
uncurry (X --> (Y --> z)) = [:X,Y:] --> z &
uncurry' (X --> (Y --> z)) = [:Y,X:] --> z;

theorem :: FUNCT_6:16
x in dom f & g = f.x implies
rng g c= rng uncurry f & rng g c= rng uncurry' f;

theorem :: FUNCT_6:17
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;

theorem :: FUNCT_6:18
X <> {} implies rng uncurry (X --> f) = rng f &
rng uncurry' (X --> f) = rng f;

theorem :: FUNCT_6:19
[: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));

theorem :: FUNCT_6:20
f in Funcs(X,Funcs(Y,Z)) implies
uncurry f in Funcs([:X,Y:],Z) & uncurry' f in Funcs([:Y,X:],Z);

theorem :: FUNCT_6:21
(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);

theorem :: FUNCT_6:22
(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));

theorem :: FUNCT_6:23
f in PFuncs([:X,Y:],Z) implies
curry f in PFuncs(X,PFuncs(Y,Z)) & curry' f in PFuncs(Y,PFuncs(X,Z));

theorem :: FUNCT_6:24
f in PFuncs(X,PFuncs(Y,Z)) implies
uncurry f in PFuncs([:X,Y:],Z) & uncurry' f in PFuncs([:Y,X:],Z);

theorem :: FUNCT_6:25
(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);

theorem :: FUNCT_6:26
(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));

begin

definition let X be set;
func SubFuncs X means
:: FUNCT_6:def 1
x in it iff x in X & x is Function;
end;

theorem :: FUNCT_6:27
SubFuncs X c= X;

theorem :: FUNCT_6:28
x in f"SubFuncs rng f iff x in dom f & f.x is Function;

theorem :: FUNCT_6:29
SubFuncs {} = {} & SubFuncs {f} = {f} & SubFuncs {f,g} = {f,g} &
SubFuncs {f,g,h} = {f,g,h};

theorem :: FUNCT_6:30
Y c= SubFuncs X implies SubFuncs Y = Y;

definition let f be Function;
func doms f -> Function means
:: FUNCT_6:def 2

dom it = f"SubFuncs rng f &
for x st x in f"SubFuncs rng f holds it.x = proj1 (f.x);
func rngs f -> Function means
:: FUNCT_6:def 3

dom it = f"SubFuncs rng f &
for x st x in f"SubFuncs rng f holds it.x = proj2 (f.x);
func meet f equals
:: FUNCT_6:def 4
meet rng f;
end;

theorem :: FUNCT_6:31
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;

theorem :: FUNCT_6:32
doms {} = {} & rngs {} = {};

theorem :: FUNCT_6:33
doms <*f*> = <*dom f*> & rngs <*f*> = <*rng f*>;

theorem :: FUNCT_6:34
doms <*f,g*> = <*dom f, dom g*> & rngs <*f,g*> = <*rng f, rng g*>;

theorem :: FUNCT_6:35
doms <*f,g,h*> = <*dom f, dom g, dom h*> &
rngs <*f,g,h*> = <*rng f, rng g, rng h*>;

theorem :: FUNCT_6:36
doms (X --> f) = X --> dom f & rngs (X --> f) = X --> rng f;

theorem :: FUNCT_6:37
f <> {} implies (x in meet f iff for y st y in dom f holds x in f.y);

theorem :: FUNCT_6:38
meet {} = {};

theorem :: FUNCT_6:39
Union <*X*> = X & meet <*X*> = X;

theorem :: FUNCT_6:40
Union <*X,Y*> = X \/ Y & meet <*X,Y*> = X /\ Y;

theorem :: FUNCT_6:41
Union <*X,Y,Z*> = X \/ Y \/ Z & meet <*X,Y,Z*> = X /\ Y /\ Z;

theorem :: FUNCT_6:42
Union ({} --> Y) = {} & meet ({} --> Y) = {};

theorem :: FUNCT_6:43
X <> {} implies Union (X --> Y) = Y & meet (X --> Y) = Y;

definition let f be Function, x, y be set;
func f..(x,y) -> set equals
:: FUNCT_6:def 5

(uncurry f).[x,y];
end;

theorem :: FUNCT_6:44
x in dom f & g = f.x & y in dom g implies f..(x,y) = g.y;

theorem :: FUNCT_6:45
x in dom f implies
<*f*>..(1,x) = f.x & <*f,g*>..(1,x) = f.x & <*f,g,h*>..(1,x) = f.x;

theorem :: FUNCT_6:46
x in dom g implies <*f,g*>..(2,x) = g.x & <*f,g,h*>..(2,x) = g.x;

theorem :: FUNCT_6:47
x in dom h implies <*f,g,h*>..(3,x) = h.x;

theorem :: FUNCT_6:48
x in X & y in dom f implies (X --> f)..(x,y) = f.y;

begin

definition let f be Function;
func <:f:> -> Function equals
:: FUNCT_6:def 6
curry ((uncurry' f)|[:meet doms f, dom f:]);
end;

theorem :: FUNCT_6:49
dom <:f:> = meet doms f & rng <:f:> c= product rngs f;

theorem :: FUNCT_6:50
x in dom <:f:> implies <:f:>.x is Function;

theorem :: FUNCT_6:51
x in dom <:f:> & g = <:f:>.x implies dom g = f"SubFuncs rng f &
for y st y in dom g holds [y,x] in dom uncurry f & g.y = (uncurry f).[y,x];

theorem :: FUNCT_6:52
x in dom <:f:> implies for g st g in rng f holds x in dom g;

theorem :: FUNCT_6:53
g in rng f & (for g st g in rng f holds x in dom g) implies x in dom <:f:>;

theorem :: FUNCT_6:54
x in dom f & g = f.x & y in dom <:f:> & h = <:f:>.y implies g.y = h.x;

theorem :: FUNCT_6:55
x in dom f & f.x is Function & y in dom <:f:> implies f..(x,y) = <:f:>..(y,x
);

definition let f be Function;
func Frege f -> Function means
:: FUNCT_6:def 7

dom it = product doms f & for g st g in product doms f ex h st
it.g = h & dom h = f"SubFuncs rng f &
for x st x in dom h holds h.x = (uncurry f).[x,g.x];
end;

theorem :: FUNCT_6:56
g in product doms f & x in dom g implies (Frege f)..(g,x) = f..(x,g.x);

theorem :: FUNCT_6:57
x in dom f & g = f.x & h in product doms f & h' = (Frege f).h implies
h.x in dom g & h'.x = g.(h.x) & h' in product rngs f;

theorem :: FUNCT_6:58
rng Frege f = product rngs f;

theorem :: FUNCT_6:59
not {} in rng f implies
(Frege f is one-to-one iff for g st g in rng f holds g is one-to-one);

begin

theorem :: FUNCT_6:60
<:{}:> = {} & Frege{} = {{}} --> {};

theorem :: FUNCT_6:61
dom <:<*h*>:> = dom h & for x st x in dom h holds <:<*h*>:>.x = <*h.x*>;

theorem :: FUNCT_6:62
dom <:<*f1,f2*>:> = dom f1 /\ dom f2 &
for x st x in dom f1 /\ dom f2 holds <:<*f1,f2*>:>.x = <*f1.x,f2.x*>;

theorem :: FUNCT_6:63
X <> {} implies dom <:X --> f:> = dom f &
for x st x in dom f holds <:X --> f:>.x = X --> f.x;

theorem :: FUNCT_6:64
dom Frege<*h*> = product <*dom h*> & rng Frege<*h*> = product <*rng h*> &
for x st x in dom h holds (Frege<*h*>).<*x*> = <*h.x*>;

theorem :: FUNCT_6:65
dom Frege<*f1,f2*> = product <*dom f1, dom f2*> &
rng Frege<*f1,f2*> = product <*rng f1, rng f2*> &
for x,y st x in dom f1 & y in dom f2 holds
(Frege<*f1,f2*>).<*x,y*> = <*f1.x, f2.y*>;

theorem :: FUNCT_6:66
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;

theorem :: FUNCT_6:67
x in dom f1 & x in dom f2 implies
for y1,y2 holds <:f1,f2:>.x = [y1,y2] iff <:<*f1,f2*>:>.x = <*y1,y2*>;

theorem :: FUNCT_6:68
x in dom f1 & y in dom f2 implies
for y1,y2 holds [:f1,f2:].[x,y] = [y1,y2] iff
(Frege<*f1,f2*>).<*x,y*> = <*y1,y2*>;

theorem :: FUNCT_6:69
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;

theorem :: FUNCT_6:70
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;

theorem :: FUNCT_6:71
dom f = X implies product f,product (f*P) are_equipotent;

begin

definition let f,X;
func Funcs(f,X) -> Function means
:: FUNCT_6:def 8
dom it = dom f & for x st x in dom f holds it.x = Funcs(f.x,X);
end;

theorem :: FUNCT_6:72
not {} in rng f implies Funcs(f,{}) = dom f --> {};

theorem :: FUNCT_6:73
Funcs({},X) = {};

theorem :: FUNCT_6:74
Funcs(<*X*>,Y) = <*Funcs(X,Y)*>;

theorem :: FUNCT_6:75
Funcs(<*X,Y*>,Z) = <*Funcs(X,Z), Funcs(Y,Z)*>;

theorem :: FUNCT_6:76
Funcs(X --> Y, Z) = X --> Funcs(Y,Z);

theorem :: FUNCT_6:77
Funcs(Union disjoin f,X),product Funcs(f,X) are_equipotent;

definition let X,f;
func Funcs(X,f) -> Function means
:: FUNCT_6:def 9

dom it = dom f & for x st x in dom f holds it.x = Funcs(X,f.x);
end;

theorem :: FUNCT_6:78
Funcs({},f) = dom f --> {{}};

theorem :: FUNCT_6:79
Funcs(X,{}) = {};

theorem :: FUNCT_6:80
Funcs(X,<*Y*>) = <*Funcs(X,Y)*>;

theorem :: FUNCT_6:81
Funcs(X,<*Y,Z*>) = <*Funcs(X,Y), Funcs(X,Z)*>;

theorem :: FUNCT_6:82
Funcs(X, Y --> Z) = Y --> Funcs(X,Z);

theorem :: FUNCT_6:83
product Funcs(X,f),Funcs(X, product f) are_equipotent;