let X be set ; for f being Function st f <> {} & X <> {} holds
product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
let f be Function; ( f <> {} & X <> {} implies product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent )
defpred S1[ object , object ] means ex g being Function-yielding Function st
( $1 = g & $2 = <:g:> );
assume that
A1:
f <> {}
and
A2:
X <> {}
; product (Funcs (X,f)), Funcs (X,(product f)) are_equipotent
A3:
for x being object st x in product (Funcs (X,f)) holds
ex y being object st S1[x,y]
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
S1[x,F . x] ) )
from CLASSES1:sch 1(A3);
take
F
; WELLORD2:def 4 ( F is one-to-one & dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product 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;
( g in product (Funcs (X,f)) implies ( dom <:g:> = X & rng g = rng g & rng <:g:> c= product f ) )
A9:
dom (Funcs (X,f)) = dom f
by Def8;
assume A10:
g in product (Funcs (X,f))
;
( dom <:g:> = X & rng g = rng g & rng <:g:> c= product f )
then A11:
dom g = dom (Funcs (X,f))
by CARD_3:9;
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;
rng <:g:> c= product f
let y be
object ;
TARSKI:def 3 ( not y in rng <:g:> or y in product f )
assume
y in rng <:g:>
;
y in product f
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 for z being object st z in dom f holds
h . z in f . zlet z be
object ;
( z in dom f implies h . z in f . z )assume A18:
z in dom f
;
h . z in f . zthen 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;
verum end;
hence
y in product f
by A17, CARD_3:def 5;
verum
end;
thus
F is one-to-one
( dom F = product (Funcs (X,f)) & rng F = Funcs (X,(product f)) )proof
let x,
y be
object ;
FUNCT_1:def 4 ( not x in dom F or not y in dom F or not F . x = F . y or x = y )
assume that A24:
x in dom F
and A25:
y in dom F
and A26:
F . x = F . y
and A27:
x <> y
;
contradiction
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 for z being object st z in dom f holds
gx . z = gy . zlet z be
object ;
( z in dom f implies gx . z = gy . z )assume A35:
z in dom f
;
gx . z = gy . zthen 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 for b being object st b in X holds
hx . b = hy . blet b be
object ;
( b in X implies hx . b = hy . b )assume A40:
b in X
;
hx . b = hy . breconsider 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;
verum end; hence
gx . z = gy . z
by A38, A37;
verum end;
hence
contradiction
by A27, A30, A28, A32, A34, A33, FUNCT_1:2;
verum
end;
thus
dom F = product (Funcs (X,f))
by A7; rng F = Funcs (X,(product f))
thus
rng F c= Funcs (X,(product f))
XBOOLE_0:def 10 Funcs (X,(product f)) c= rng F
let y be object ; TARSKI:def 3 ( not y in Funcs (X,(product f)) or y in rng F )
assume
y in Funcs (X,(product f))
; y in rng 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
then reconsider h = h as Function-yielding Function ;
set g = <:h:>;
A53:
meet (doms h) = dom <:h:>
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 <:h:> = dom f
by A2, A53, Th23;
A55:
now for z being object st z in dom f holds
<:h:> . z in (Funcs (X,f)) . zlet z be
object ;
( z in dom f implies <:h:> . z in (Funcs (X,f)) . z )assume A56:
z in dom f
;
<:h:> . z in (Funcs (X,f)) . zreconsider i =
<:h:> . z as
Function ;
A57:
dom i = X
by A48, A54, A56, Th26;
rng i c= f . z
proof
let x be
object ;
TARSKI:def 3 ( not x in rng i or x in f . z )
assume
x in rng i
;
x in f . z
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
x in f . z
by A56, A59, A61;
verum
end; then
<:h:> . z in Funcs (
X,
(f . z))
by A57, FUNCT_2:def 2;
hence
<:h:> . z in (Funcs (X,f)) . z
by A56, Def8;
verum end;
A62:
meet (doms <:h:>) = dom <:<:h:>:>
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:
<:h:> in product (Funcs (X,f))
by A54, A55, CARD_3:def 5;
then A66:
ex g9 being Function-yielding Function st
( <:h:> = g9 & F . <:h:> = <:g9:> )
by A7;
dom (uncurry' h) = [:(dom f),(dom h):]
by A63, FUNCT_5:26;
then A67:
(uncurry' h) | [:(meet (doms h)),(dom h):] = uncurry' h
by A53, A54;
A68:
( uncurry' h = ~ (uncurry h) & curry (~ (uncurry h)) = curry' (uncurry h) )
by FUNCT_5:def 3, FUNCT_5:def 4;
dom <:<:h:>:> = X
by A8, A65;
then A69:
(uncurry h) | [:(meet (doms <:h:>)),(dom <:h:>):] = uncurry h
by A48, A54, A64, A62;
uncurry' (curry' (uncurry h)) = uncurry h
by A64, FUNCT_5:49;
then
<:<:h:>:> = h
by A1, A63, A67, A69, A68, FUNCT_5:48;
hence
y in rng F
by A7, A47, A65, A66, FUNCT_1:def 3; verum