let X be set ; for R being Relation
for C being Cardinal st ( for x being object st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
let R be Relation; for C being Cardinal st ( for x being object st x in X holds
card (Im (R,x)) = C ) holds
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
let C be Cardinal; ( ( for x being object st x in X holds
card (Im (R,x)) = C ) implies card R = (card (R | ((dom R) \ X))) +` (C *` (card X)) )
assume A1:
for x being object st x in X holds
card (Im (R,x)) = C
; card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
set DA = (dom R) \ X;
per cases
( X c= dom R or not X c= dom R )
;
suppose A2:
X c= dom R
;
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))deffunc H1(
object )
-> set =
Im (
R,$1);
consider f being
Function such that A3:
(
dom f = X & ( for
x being
object st
x in X holds
f . x = H1(
x) ) )
from FUNCT_1:sch 3();
defpred S1[
object ,
object ]
means ex
g being
Function st
(
g = $2 &
dom g = f . $1 &
rng g = C &
g is
one-to-one );
A4:
for
x being
object st
x in X holds
ex
y being
object st
S1[
x,
y]
consider ff being
Function such that A6:
(
dom ff = X & ( for
x being
object st
x in X holds
S1[
x,
ff . x] ) )
from CLASSES1:sch 1(A4);
then reconsider ff =
ff as
Function-yielding Function by FUNCOP_1:def 6;
deffunc H2(
object )
-> object =
[($1 `1),((ff . ($1 `1)) . ($1 `2))];
consider p being
Function such that A7:
(
dom p = R | X & ( for
x being
object st
x in R | X holds
p . x = H2(
x) ) )
from FUNCT_1:sch 3();
A8:
rng p = [:X,C:]
proof
hereby TARSKI:def 3,
XBOOLE_0:def 10 [:X,C:] c= rng p
let y be
object ;
( y in rng p implies y in [:X,C:] )assume
y in rng p
;
y in [:X,C:]then consider x being
object such that A9:
x in dom p
and A10:
p . x = y
by FUNCT_1:def 3;
A11:
p . x = [(x `1),((ff . (x `1)) . (x `2))]
by A7, A9;
A12:
x = [(x `1),(x `2)]
by A7, A9, MCART_1:21;
then
(
x `1 in {(x `1)} &
x in R )
by A7, A9, RELAT_1:def 11, TARSKI:def 1;
then A13:
x `2 in R .: {(x `1)}
by A12, RELAT_1:def 13;
A14:
x `1 in X
by A7, A9, A12, RELAT_1:def 11;
then consider g being
Function such that A15:
g = ff . (x `1)
and A16:
dom g = f . (x `1)
and A17:
rng g = C
and
g is
one-to-one
by A6;
f . (x `1) = Im (
R,
(x `1))
by A3, A14;
then
x `2 in dom g
by A13, A16, RELAT_1:def 16;
then
g . (x `2) in C
by A17, FUNCT_1:def 3;
hence
y in [:X,C:]
by A10, A11, A14, A15, ZFMISC_1:87;
verum
end;
let y be
object ;
TARSKI:def 3 ( not y in [:X,C:] or y in rng p )
assume
y in [:X,C:]
;
y in rng p
then consider y1,
y2 being
object such that A18:
y1 in X
and A19:
y2 in C
and A20:
y = [y1,y2]
by ZFMISC_1:def 2;
consider g being
Function such that A21:
g = ff . y1
and A22:
dom g = f . y1
and A23:
rng g = C
and
g is
one-to-one
by A6, A18;
consider x2 being
object such that A24:
x2 in dom g
and A25:
g . x2 = y2
by A19, A23, FUNCT_1:def 3;
A26:
H2(
[y1,x2])
= y
by A20, A21, A25;
f . y1 = Im (
R,
y1)
by A3, A18;
then
[y1,x2] in R
by A22, A24, RELSET_2:9;
then A27:
[y1,x2] in R | X
by A18, RELAT_1:def 11;
then
p . [y1,x2] = H2(
[y1,x2])
by A7;
hence
y in rng p
by A7, A26, A27, FUNCT_1:def 3;
verum
end; now for x1, x2 being object st x1 in dom p & x2 in dom p & p . x1 = p . x2 holds
x1 = x2let x1,
x2 be
object ;
( x1 in dom p & x2 in dom p & p . x1 = p . x2 implies x1 = x2 )assume that A28:
x1 in dom p
and A29:
x2 in dom p
and A30:
p . x1 = p . x2
;
x1 = x2A31:
(
p . x1 = H2(
x1) &
p . x2 = H2(
x2) )
by A7, A28, A29;
then A32:
x1 `1 = x2 `1
by A30, XTUPLE_0:1;
A33:
x1 = [(x1 `1),(x1 `2)]
by A7, A28, MCART_1:21;
then
x1 in R
by A7, A28, RELAT_1:def 11;
then A34:
x1 `2 in Im (
R,
(x1 `1))
by A33, RELSET_2:9;
A35:
x2 = [(x2 `1),(x2 `2)]
by A7, A29, MCART_1:21;
then
x2 in R
by A7, A29, RELAT_1:def 11;
then A36:
x2 `2 in Im (
R,
(x2 `1))
by A35, RELSET_2:9;
x2 `1 in X
by A7, A29, A35, RELAT_1:def 11;
then consider g2 being
Function such that A37:
g2 = ff . (x2 `1)
and
dom g2 = f . (x2 `1)
and
rng g2 = C
and
g2 is
one-to-one
by A6;
A38:
x1 `1 in X
by A7, A28, A33, RELAT_1:def 11;
then consider g1 being
Function such that A39:
g1 = ff . (x1 `1)
and A40:
dom g1 = f . (x1 `1)
and
rng g1 = C
and A41:
g1 is
one-to-one
by A6;
A42:
f . (x1 `1) = Im (
R,
(x1 `1))
by A3, A38;
g1 . (x1 `2) = g2 . (x2 `2)
by A30, A31, A37, A39, XTUPLE_0:1;
hence
x1 = x2
by A32, A35, A36, A33, A34, A37, A39, A40, A41, A42, FUNCT_1:def 4;
verum end; then
p is
one-to-one
by FUNCT_1:def 4;
then
R | X,
[:X,C:] are_equipotent
by A7, A8, WELLORD2:def 4;
then A43:
card (R | X) =
card [:X,C:]
by CARD_1:5
.=
card [:(card X),C:]
by CARD_2:7
.=
C *` (card X)
by CARD_2:def 2
;
A44:
R | X misses R | ((dom R) \ X)
((dom R) \ X) \/ X =
(dom R) \/ X
by XBOOLE_1:39
.=
dom R
by A2, XBOOLE_1:12
;
then (R | X) \/ (R | ((dom R) \ X)) =
R | (dom R)
by RELAT_1:78
.=
R
;
hence
card R = (card (R | ((dom R) \ X))) +` (C *` (card X))
by A43, A44, CARD_2:35;
verum end; end;