let X be set ; :: thesis: ( X is mutually-disjoint implies Sum (Card (id X)) = card (union X) )
set D = disjoin (Card (id X));
assume A1: X is mutually-disjoint ; :: thesis: Sum (Card (id X)) = card (union X)
per cases ( ( X <> {} & X <> {{}} ) or X = {} or X = {{}} ) ;
suppose A2: ( X <> {} & X <> {{}} ) ; :: thesis: Sum (Card (id X)) = card (union X)
reconsider P = X \ {{}} as a_partition of union X by A1, Th11;
reconsider U = union X as non empty set by A2, SCMYCIEL:18;
reconsider P = P as non empty a_partition of U ;
deffunc H1( object ) -> Enumeration of ((proj P) . $1) = the Enumeration of ((proj P) . $1);
deffunc H2( object ) -> object = [(H1($1) . $1),((proj P) . $1)];
consider f being Function such that
A3: ( dom f = union X & ( for z being object st z in union X holds
f . z = H2(z) ) ) from FUNCT_1:sch 3();
A4: dom (disjoin (Card (id X))) = dom (Card (id X)) by CARD_3:def 3
.= dom (id X) by CARD_3:def 2
.= X ;
now :: thesis: for y being object holds
( ( y in rng f implies y in Union (disjoin (Card (id X))) ) & ( y in Union (disjoin (Card (id X))) implies y in rng f ) )
let y be object ; :: thesis: ( ( y in rng f implies y in Union (disjoin (Card (id X))) ) & ( y in Union (disjoin (Card (id X))) implies y in rng f ) )
hereby :: thesis: ( y in Union (disjoin (Card (id X))) implies y in rng f )
assume y in rng f ; :: thesis: y in Union (disjoin (Card (id X)))
then consider z being object such that
A5: ( z in dom f & f . z = y ) by FUNCT_1:def 3;
set x = (proj P) . z;
A6: y = [(H1(z) . z),((proj P) . z)] by A3, A5;
A7: (proj P) . z in P by A3, A5, FUNCT_2:5;
then A8: (disjoin (Card (id X))) . ((proj P) . z) = [:(card ((proj P) . z)),{((proj P) . z)}:] by Th13;
A9: (disjoin (Card (id X))) . ((proj P) . z) in rng (disjoin (Card (id X))) by A4, A7, FUNCT_1:3;
y in (disjoin (Card (id X))) . ((proj P) . z)
proof
z in (proj P) . z by A3, A5, EQREL_1:def 9;
then z in dom H1(z) by AOFA_I00:6;
then A10: H1(z) . z in rng H1(z) by FUNCT_1:3;
(proj P) . z in {((proj P) . z)} by TARSKI:def 1;
hence y in (disjoin (Card (id X))) . ((proj P) . z) by A6, A8, A10, ZFMISC_1:def 2; :: thesis: verum
end;
then y in union (rng (disjoin (Card (id X)))) by A9, TARSKI:def 4;
hence y in Union (disjoin (Card (id X))) by CARD_3:def 4; :: thesis: verum
end;
assume y in Union (disjoin (Card (id X))) ; :: thesis: y in rng f
then y in union (rng (disjoin (Card (id X)))) by CARD_3:def 4;
then consider Y being set such that
A11: ( y in Y & Y in rng (disjoin (Card (id X))) ) by TARSKI:def 4;
consider x being object such that
A12: ( x in dom (disjoin (Card (id X))) & (disjoin (Card (id X))) . x = Y ) by A11, FUNCT_1:def 3;
reconsider x = x as set by TARSKI:1;
y in [:(card x),{x}:] by A4, A11, A12, Th13;
then consider a, b being object such that
A13: ( a in card x & b in {x} & y = [a,b] ) by ZFMISC_1:def 2;
a in rng the Enumeration of x by A13, AOFA_I00:6;
then consider z being object such that
A14: z in dom the Enumeration of x and
A15: the Enumeration of x . z = a by FUNCT_1:def 3;
A16: z in x by A14;
then A17: z in U by A4, A12, TARSKI:def 4;
not x in {{}} by A16, TARSKI:def 1;
then x in P by A4, A12, XBOOLE_0:def 5;
then (proj P) . z = x by A16, EQREL_1:65;
then ( a = H1(z) . z & b = (proj P) . z ) by A13, A15, TARSKI:def 1;
then y = f . z by A3, A13, A17;
hence y in rng f by A3, A17, FUNCT_1:3; :: thesis: verum
end;
then A18: rng f = Union (disjoin (Card (id X))) by TARSKI:2;
now :: thesis: for z1, z2 being object st z1 in dom f & z2 in dom f & f . z1 = f . z2 holds
z1 = z2
let z1, z2 be object ; :: thesis: ( z1 in dom f & z2 in dom f & f . z1 = f . z2 implies z1 = z2 )
assume A19: ( z1 in dom f & z2 in dom f & f . z1 = f . z2 ) ; :: thesis: z1 = z2
then ( f . z1 = [(H1(z1) . z1),((proj P) . z1)] & f . z2 = [(H1(z2) . z2),((proj P) . z2)] ) by A3;
then A20: ( H1(z1) . z1 = H1(z2) . z2 & (proj P) . z1 = (proj P) . z2 ) by A19, XTUPLE_0:1;
then ( z1 in (proj P) . z1 & z2 in (proj P) . z1 ) by A3, A19, EQREL_1:def 9;
then ( z1 in dom H1(z1) & z2 in dom H1(z1) ) by AOFA_I00:6;
hence z1 = z2 by A20, FUNCT_1:def 4; :: thesis: verum
end;
then card (Union (disjoin (Card (id X)))) = card (union X) by A3, A18, CARD_1:70, FUNCT_1:def 4;
hence Sum (Card (id X)) = card (union X) by CARD_3:def 7; :: thesis: verum
end;
suppose A21: X = {} ; :: thesis: Sum (Card (id X)) = card (union X)
set f = the empty Function;
thus Sum (Card (id X)) = card (Union (disjoin (Card (id X)))) by CARD_3:def 7
.= card (union (rng (disjoin (Card (id X))))) by CARD_3:def 4
.= card (union (rng (disjoin the empty Function))) by A21
.= card (union X) by A21, CARD_3:3 ; :: thesis: verum
end;
suppose A22: X = {{}} ; :: thesis: Sum (Card (id X)) = card (union X)
thus Sum (Card (id X)) = card (Union (disjoin (Card (id X)))) by CARD_3:def 7
.= card (union (rng (disjoin (Card (id X))))) by CARD_3:def 4
.= card (union (rng (disjoin (Card ({} .--> {}))))) by A22, FUNCT_4:96
.= card (union (rng (disjoin (Card (X --> {}))))) by A22, FUNCOP_1:def 9
.= card (union (rng (disjoin (X --> (card {}))))) by CARD_3:2
.= card (union (rng (disjoin ({} .--> {})))) by A22, FUNCOP_1:def 9
.= card (union (rng ({} .--> [:{},{{}}:]))) by CARD_3:4
.= card (union X) by A22, FUNCOP_1:88 ; :: thesis: verum
end;
end;