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]
proof
let x be
set ;
( x in rng F implies ex y being set st S1[x,y] )
assume
x in rng F
;
ex y being set st S1[x,y]
A3:
card (Coim F,x) = card (Coim G,x)
by A1, Def9;
A4:
F " {x},
G " {x} are_equipotent
by A3, CARD_1:21;
consider H being
Function such that A5:
(
H is
one-to-one &
dom H = F " {x} &
rng H = G " {x} )
by A4, WELLORD2:def 4;
take
H
;
S1[x,H]
thus
H is
Function
;
for f being Function st H = f holds
( dom f = F " {x} & rng f = G " {x} & f is one-to-one )
let g be
Function;
( H = g implies ( dom g = F " {x} & rng g = G " {x} & g is one-to-one ) )
assume A6:
g = H
;
( dom g = F " {x} & rng g = G " {x} & g is one-to-one )
thus
(
dom g = F " {x} &
rng g = G " {x} &
g is
one-to-one )
by A5, A6;
verum
end;
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] )
proof
let x be
set ;
( x in dom F implies ex y being set st
( y in dom G & S2[x,y] ) )
assume A9:
x in dom F
;
ex y being set st
( y in dom G & S2[x,y] )
A10:
F . x in rng F
by A9, FUNCT_1:def 5;
reconsider f =
W . (F . x) as
Function by A7, A10;
A11:
(
dom f = F " {(F . x)} &
rng f = G " {(F . x)} )
by A7, A10;
take y =
f . x;
( y in dom G & S2[x,y] )
A12:
F . x in {(F . x)}
by TARSKI:def 1;
A13:
x in F " {(F . x)}
by A9, A12, FUNCT_1:def 13;
A14:
f . x in G " {(F . x)}
by A11, A13, FUNCT_1:def 5;
thus
y in dom G
by A14, FUNCT_1:def 13;
S2[x,y]
let g be
Function;
( g = W . (F . x) implies y = g . x )
assume A15:
g = W . (F . x)
;
y = g . x
thus
y = g . x
by A15;
verum
end;
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 )
A17:
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
A19:
G . x in rng G
by A18, FUNCT_1:def 5;
A20:
rng F = rng G
by A1, Th83;
reconsider f =
W . (G . x) as
Function by A7, A19, A20;
A21:
dom f = F " {(G . x)}
by A7, A19, A20;
A22:
rng f = G " {(G . x)}
by A7, A19, A20;
A23:
G . x in {(G . x)}
by TARSKI:def 1;
A24:
x in rng f
by A18, A22, A23, FUNCT_1:def 13;
consider z being
set such that A25:
z in dom f
and A26:
f . z = x
by A24, FUNCT_1:def 5;
A27:
z in dom F
by A21, A25, FUNCT_1:def 13;
A28:
F . z in {(G . x)}
by A21, A25, FUNCT_1:def 13;
A29:
F . z = G . x
by A28, TARSKI:def 1;
A30:
IT . z = x
by A16, A26, A27, A29;
thus
x in rng IT
by A16, A27, A30, FUNCT_1:def 5;
verum
end;
thus
rng IT = dom G
by A16, A17, XBOOLE_0:def 10;
( IT is one-to-one & F = G * IT )
A31:
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;
reconsider f1 =
W . (F . x),
f2 =
W . (F . y) as
Function by A7, A35, A36;
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;
A48:
f2 . y in rng f2
by A41, A46, FUNCT_1:def 5;
A49:
f1 . x in (G " {(F . x)}) /\ (G " {(F . y)})
by A34, A37, A39, A42, A47, A48, XBOOLE_0:def 4;
A50:
f1 . x in G " ({(F . x)} /\ {(F . y)})
by A49, FUNCT_1:137;
A51:
G . (f1 . x) in {(F . x)} /\ {(F . y)}
by A50, FUNCT_1:def 13;
A52:
G . (f1 . x) in {(F . x)}
by A51, 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;
A55:
G . (f1 . x) = F . y
by A53, TARSKI:def 1;
thus
x = y
by A34, A37, A38, A40, A45, A46, A54, A55, FUNCT_1:def 8;
verum end;
thus
IT is
one-to-one
by A31, FUNCT_1:def 8;
F = G * IT
A56:
dom (G * IT) = dom F
by A16, RELAT_1:46;
A57:
now let x be
set ;
( x in dom F implies F . x = (G * IT) . x )assume A58:
x in dom F
;
F . x = (G * IT) . xA59:
F . x in rng F
by A58, FUNCT_1:def 5;
reconsider f =
W . (F . x) as
Function by A7, A59;
A60:
(
dom f = F " {(F . x)} &
rng f = G " {(F . x)} )
by A7, A59;
A61:
F . x in {(F . x)}
by TARSKI:def 1;
A62:
x in F " {(F . x)}
by A58, A61, FUNCT_1:def 13;
A63:
f . x in G " {(F . x)}
by A60, A62, FUNCT_1:def 5;
A64:
G . (f . x) in {(F . x)}
by A63, FUNCT_1:def 13;
A65:
G . (f . x) = F . x
by A64, TARSKI:def 1;
A66:
IT . x = f . x
by A16, A58;
thus
F . x = (G * IT) . x
by A16, A58, A65, A66, FUNCT_1:23;
verum end;
thus
F = G * IT
by A56, A57, 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;
A73:
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 A74:
z in rng (H | (F " {x}))
;
z in G " {x}
consider y being
set such that A75:
y in dom (H | (F " {x}))
and A76:
(H | (F " {x})) . y = z
by A74, FUNCT_1:def 5;
A77:
F . y in {x}
by A72, A75, FUNCT_1:def 13;
A78:
F . y = x
by A77, TARSKI:def 1;
A79:
z = H . y
by A75, A76, FUNCT_1:70;
A80:
dom (H | (F " {x})) = (dom H) /\ (F " {x})
by RELAT_1:90;
A81:
y in dom H
by A75, A80, XBOOLE_0:def 4;
A82:
z in dom G
by A68, A79, A81, FUNCT_1:def 5;
A83:
x = G . z
by A70, A78, A79, A81, FUNCT_1:23;
A84:
G . z in {x}
by A83, TARSKI:def 1;
thus
z in G " {x}
by A82, A84, 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}))
A86:
z in dom G
by A85, FUNCT_1:def 13;
A87:
G . z in {x}
by A85, FUNCT_1:def 13;
A88:
G . z = x
by A87, 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;
A91:
F . y = x
by A70, A88, A89, A90, FUNCT_1:23;
A92:
F . y in {x}
by A91, TARSKI:def 1;
A93:
y in dom (H | (F " {x}))
by A67, A72, A89, A92, FUNCT_1:def 13;
A94:
(H | (F " {x})) . y in rng (H | (F " {x}))
by A93, FUNCT_1:def 5;
thus
z in rng (H | (F " {x}))
by A90, A93, A94, FUNCT_1:70;
verum
end;
A95:
F " {x},G " {x} are_equipotent
by A71, A72, A73, WELLORD2:def 4;
thus
card (Coim F,x) = card (Coim G,x)
by A95, CARD_1:21; verum