let F, G be Function; ( F,G are_fiberwise_equipotent iff ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )
thus
( F,G are_fiberwise_equipotent implies ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) )
( ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H ) implies F,G are_fiberwise_equipotent )proof
assume A1:
F,
G are_fiberwise_equipotent
;
ex H being Function st
( dom H = dom F & rng H = dom G & H is one-to-one & F = G * H )
defpred S1[
set ,
set ]
means ( $2 is
Function & ( for
f being
Function st $2
= f holds
(
dom f = F " {$1} &
rng f = G " {$1} &
f is
one-to-one ) ) );
A2:
for
x being
set st
x in rng F holds
ex
y being
set st
S1[
x,
y]
consider W being
Function such that A7:
(
dom W = rng F & ( for
x being
set st
x in rng F holds
S1[
x,
W . x] ) )
from CLASSES1:sch 1(A2);
defpred S2[
set ,
set ]
means for
H being
Function st
H = W . (F . $1) holds
$2
= H . $1;
set df =
dom F;
set dg =
dom G;
A8:
for
x being
set st
x in dom F holds
ex
y being
set st
(
y in dom G &
S2[
x,
y] )
consider IT being
Function such that A16:
(
dom IT = dom F &
rng IT c= dom G & ( for
x being
set st
x in dom F holds
S2[
x,
IT . x] ) )
from WELLORD2:sch 1(A8);
take
IT
;
( dom IT = dom F & rng IT = dom G & IT is one-to-one & F = G * IT )
thus
dom IT = dom F
by A16;
( rng IT = dom G & IT is one-to-one & F = G * IT )
dom G c= rng IT
proof
let x be
set ;
TARSKI:def 3 ( not x in dom G or x in rng IT )
assume A18:
x in dom G
;
x in rng IT
then A19:
G . x in rng G
by FUNCT_1:def 5;
A20:
rng F = rng G
by A1, Th83;
then reconsider f =
W . (G . x) as
Function by A7, A19;
A21:
dom f = F " {(G . x)}
by A7, A19, A20;
A22:
rng f = G " {(G . x)}
by A7, A19, A20;
G . x in {(G . x)}
by TARSKI:def 1;
then
x in rng f
by A18, A22, FUNCT_1:def 13;
then consider z being
set such that A25:
z in dom f
and A26:
f . z = x
by FUNCT_1:def 5;
A27:
z in dom F
by A21, A25, FUNCT_1:def 13;
F . z in {(G . x)}
by A21, A25, FUNCT_1:def 13;
then
F . z = G . x
by TARSKI:def 1;
then
IT . z = x
by A16, A26, A27;
hence
x in rng IT
by A16, A27, FUNCT_1:def 5;
verum
end;
hence
rng IT = dom G
by A16, XBOOLE_0:def 10;
( IT is one-to-one & F = G * IT )
now let x,
y be
set ;
( x in dom IT & y in dom IT & IT . x = IT . y implies x = y )assume that A32:
x in dom IT
and A33:
y in dom IT
and A34:
IT . x = IT . y
;
x = yA35:
F . x in rng F
by A16, A32, FUNCT_1:def 5;
A36:
F . y in rng F
by A16, A33, FUNCT_1:def 5;
then reconsider f1 =
W . (F . x),
f2 =
W . (F . y) as
Function by A7, A35;
A37:
(
IT . x = f1 . x &
IT . y = f2 . y )
by A16, A32, A33;
A38:
dom f1 = F " {(F . x)}
by A7, A35;
A39:
rng f1 = G " {(F . x)}
by A7, A35;
A40:
f1 is
one-to-one
by A7, A35;
A41:
dom f2 = F " {(F . y)}
by A7, A36;
A42:
rng f2 = G " {(F . y)}
by A7, A36;
A43:
F . x in {(F . x)}
by TARSKI:def 1;
A44:
F . y in {(F . y)}
by TARSKI:def 1;
A45:
x in F " {(F . x)}
by A16, A32, A43, FUNCT_1:def 13;
A46:
y in F " {(F . y)}
by A16, A33, A44, FUNCT_1:def 13;
A47:
f1 . x in rng f1
by A38, A45, FUNCT_1:def 5;
f2 . y in rng f2
by A41, A46, FUNCT_1:def 5;
then
f1 . x in (G " {(F . x)}) /\ (G " {(F . y)})
by A34, A37, A39, A42, A47, XBOOLE_0:def 4;
then
f1 . x in G " ({(F . x)} /\ {(F . y)})
by FUNCT_1:137;
then A51:
G . (f1 . x) in {(F . x)} /\ {(F . y)}
by FUNCT_1:def 13;
then A52:
G . (f1 . x) in {(F . x)}
by XBOOLE_0:def 4;
A53:
G . (f1 . x) in {(F . y)}
by A51, XBOOLE_0:def 4;
A54:
G . (f1 . x) = F . x
by A52, TARSKI:def 1;
G . (f1 . x) = F . y
by A53, TARSKI:def 1;
hence
x = y
by A34, A37, A38, A40, A45, A46, A54, FUNCT_1:def 8;
verum end;
hence
IT is
one-to-one
by FUNCT_1:def 8;
F = G * IT
A56:
dom (G * IT) = dom F
by A16, RELAT_1:46;
hence
F = G * IT
by A56, FUNCT_1:9;
verum
end;
given H being Function such that A67:
dom H = dom F
and
A68:
rng H = dom G
and
A69:
H is one-to-one
and
A70:
F = G * H
; F,G are_fiberwise_equipotent
let x be set ; CLASSES1:def 9 card (Coim F,x) = card (Coim G,x)
set t = H | (F " {x});
A71:
H | (F " {x}) is one-to-one
by A69, FUNCT_1:84;
A72:
dom (H | (F " {x})) = F " {x}
by A67, RELAT_1:91, RELAT_1:167;
rng (H | (F " {x})) = G " {x}
proof
thus
rng (H | (F " {x})) c= G " {x}
XBOOLE_0:def 10 G " {x} c= rng (H | (F " {x}))proof
let z be
set ;
TARSKI:def 3 ( not z in rng (H | (F " {x})) or z in G " {x} )
assume
z in rng (H | (F " {x}))
;
z in G " {x}
then consider y being
set such that A75:
y in dom (H | (F " {x}))
and A76:
(H | (F " {x})) . y = z
by FUNCT_1:def 5;
F . y in {x}
by A72, A75, FUNCT_1:def 13;
then A78:
F . y = x
by TARSKI:def 1;
A79:
z = H . y
by A75, A76, FUNCT_1:70;
dom (H | (F " {x})) = (dom H) /\ (F " {x})
by RELAT_1:90;
then A81:
y in dom H
by A75, XBOOLE_0:def 4;
then A82:
z in dom G
by A68, A79, FUNCT_1:def 5;
x = G . z
by A70, A78, A79, A81, FUNCT_1:23;
then
G . z in {x}
by TARSKI:def 1;
hence
z in G " {x}
by A82, FUNCT_1:def 13;
verum
end;
let z be
set ;
TARSKI:def 3 ( not z in G " {x} or z in rng (H | (F " {x})) )
assume A85:
z in G " {x}
;
z in rng (H | (F " {x}))
then A86:
z in dom G
by FUNCT_1:def 13;
G . z in {x}
by A85, FUNCT_1:def 13;
then A88:
G . z = x
by TARSKI:def 1;
consider y being
set such that A89:
y in dom H
and A90:
H . y = z
by A68, A86, FUNCT_1:def 5;
F . y = x
by A70, A88, A89, A90, FUNCT_1:23;
then
F . y in {x}
by TARSKI:def 1;
then A93:
y in dom (H | (F " {x}))
by A67, A72, A89, FUNCT_1:def 13;
then
(H | (F " {x})) . y in rng (H | (F " {x}))
by FUNCT_1:def 5;
hence
z in rng (H | (F " {x}))
by A90, A93, FUNCT_1:70;
verum
end;
then
F " {x},G " {x} are_equipotent
by A71, A72, WELLORD2:def 4;
hence
card (Coim F,x) = card (Coim G,x)
by CARD_1:21; verum