let f be Function; card (Union f) c= Sum (Card f)
now assume A2:
dom f <> {}
;
card (Union f) c= Sum (Card f)defpred S2[
set ,
set ]
means for
x being
set holds
(
x in $2 iff (
x in Funcs (
(card $1),$1) & ex
g being
Function st
(
x = g &
rng g = $1 ) ) );
defpred S3[
set ,
set ]
means S2[
f . $1,$2];
A3:
for
x being
set st
x in dom f holds
ex
y being
set st
S3[
x,
y]
consider k being
Function such that A5:
(
dom k = dom f & ( for
x being
set st
x in dom f holds
S3[
x,
k . x] ) )
from CLASSES1:sch 1(A3);
reconsider M =
rng k as non
empty set by A2, A5, RELAT_1:42;
then consider FF being
Function such that
dom FF = M
and A10:
for
X being
set st
X in M holds
FF . X in X
by FUNCT_1:111;
set DD =
union (rng (disjoin (Card f)));
defpred S4[
set ,
set ]
means ex
g being
Function st
(
g = FF . (k . ($1 `2)) & $2
= g . ($1 `1) );
A11:
for
x being
set st
x in union (rng (disjoin (Card f))) holds
ex
y being
set st
S4[
x,
y]
proof
let x be
set ;
( x in union (rng (disjoin (Card f))) implies ex y being set st S4[x,y] )
assume
x in union (rng (disjoin (Card f)))
;
ex y being set st S4[x,y]
then consider X being
set such that A12:
x in X
and A13:
X in rng (disjoin (Card f))
by TARSKI:def 4;
consider y being
set such that A14:
y in dom (disjoin (Card f))
and A15:
X = (disjoin (Card f)) . y
by A13, FUNCT_1:def 3;
A16:
dom (disjoin (Card f)) = dom (Card f)
by Def3;
A17:
dom (Card f) = dom f
by Def2;
X = [:((Card f) . y),{y}:]
by A14, A15, A16, Def3;
then
x `2 in {y}
by A12, MCART_1:10;
then A18:
x `2 in dom f
by A14, A16, A17, TARSKI:def 1;
then
k . (x `2) in M
by A5, FUNCT_1:def 3;
then
FF . (k . (x `2)) in k . (x `2)
by A10;
then
FF . (k . (x `2)) in Funcs (
(card (f . (x `2))),
(f . (x `2)))
by A5, A18;
then consider g being
Function such that A19:
FF . (k . (x `2)) = g
and
dom g = card (f . (x `2))
and
rng g c= f . (x `2)
by FUNCT_2:def 2;
take
g . (x `1)
;
S4[x,g . (x `1)]
take
g
;
( g = FF . (k . (x `2)) & g . (x `1) = g . (x `1) )
thus
(
g = FF . (k . (x `2)) &
g . (x `1) = g . (x `1) )
by A19;
verum
end; consider t being
Function such that A20:
(
dom t = union (rng (disjoin (Card f))) & ( for
x being
set st
x in union (rng (disjoin (Card f))) holds
S4[
x,
t . x] ) )
from CLASSES1:sch 1(A11);
union (rng f) c= rng t
proof
let x be
set ;
TARSKI:def 3 ( not x in union (rng f) or x in rng t )
assume
x in union (rng f)
;
x in rng t
then consider X being
set such that A21:
x in X
and A22:
X in rng f
by TARSKI:def 4;
consider y being
set such that A23:
y in dom f
and A24:
X = f . y
by A22, FUNCT_1:def 3;
k . y in M
by A5, A23, FUNCT_1:def 3;
then A25:
FF . (k . y) in k . y
by A10;
then
FF . (k . y) in Funcs (
(card (f . y)),
(f . y))
by A5, A23;
then consider g being
Function such that A26:
FF . (k . y) = g
and A27:
dom g = card (f . y)
and
rng g c= f . y
by FUNCT_2:def 2;
ex
g being
Function st
(
FF . (k . y) = g &
rng g = f . y )
by A5, A23, A25;
then consider z being
set such that A28:
z in dom g
and A29:
x = g . z
by A21, A24, A26, FUNCT_1:def 3;
A30:
(Card f) . y = card (f . y)
by A23, Def2;
A31:
dom (Card f) = dom f
by Def2;
then A32:
(disjoin (Card f)) . y = [:(dom g),{y}:]
by A23, A27, A30, Def3;
A33:
y in {y}
by TARSKI:def 1;
A34:
dom (disjoin (Card f)) = dom f
by A31, Def3;
A35:
[z,y] in [:(dom g),{y}:]
by A28, A33, ZFMISC_1:87;
[:(dom g),{y}:] in rng (disjoin (Card f))
by A23, A32, A34, FUNCT_1:def 3;
then A36:
[z,y] in union (rng (disjoin (Card f)))
by A35, TARSKI:def 4;
A37:
[z,y] `1 = z
by MCART_1:7;
[z,y] `2 = y
by MCART_1:7;
then
ex
g being
Function st
(
g = FF . (k . y) &
t . [z,y] = g . z )
by A20, A36, A37;
hence
x in rng t
by A20, A26, A29, A36, FUNCT_1:def 3;
verum
end; hence
card (Union f) c= Sum (Card f)
by A20, CARD_1:12;
verum end;
hence
card (Union f) c= Sum (Card f)
by A1; verum