let X be set ; :: thesis: for M being Aleph st card X in cf M & ( for Y being set st Y in X holds
card Y in M ) holds
card (union X) in M
let M be Aleph; :: thesis: ( card X in cf M & ( for Y being set st Y in X holds
card Y in M ) implies card (union X) in M )
assume A1: card X in cf M ; :: thesis: ( ex Y being set st
( Y in X & not card Y in M ) or card (union X) in M )
assume A2: for Y being set st Y in X holds
card Y in M ; :: thesis: card (union X) in M

per cases ( X = {} or not X is empty ) ;

suppose A3: X = {} ; :: thesis: card (union X) in M

( M <> {} & {} c= M ) by XBOOLE_1:2;
then {} c< M by XBOOLE_0:def 8;
hence card (union X) in M by A3, CARD_1:47, ORDINAL1:21, ZFMISC_1:2; :: thesis: verum

end;

suppose not X is empty ; :: thesis: card (union X) in M

then reconsider X1 = X as non empty set ;
deffunc H₁( set ) -> set = card $1;
set CARDS = { H₁(Y) where Y is Element of X1 : Y in X1 } ;
for x being set st x in { H₁(Y) where Y is Element of X1 : Y in X1 } holds
( x in M & ex y being set st
( y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) )

proof

let x be set ; :: thesis: ( x in { H₁(Y) where Y is Element of X1 : Y in X1 } implies ( x in M & ex y being set st
( y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) ) )
assume A4: x in { H₁(Y) where Y is Element of X1 : Y in X1 } ; :: thesis: ( x in M & ex y being set st
( y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) )
consider Y being Element of X1 such that
A5: card Y = x and
Y in X1 by A4;
thus x in M by A2, A5; :: thesis: ex y being set st
( y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal )
take card Y ; :: thesis: ( card Y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal )
thus ( card Y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal ) by A5; :: thesis: verum

end;

then A6: ( ( for x being set st x in { H₁(Y) where Y is Element of X1 : Y in X1 } holds
x in M ) & ( for x being set st x in { H₁(Y) where Y is Element of X1 : Y in X1 } holds
ex y being set st
( y in { H₁(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) ) ) ;
then A7: { H₁(Y) where Y is Element of X1 : Y in X1 } c= M by TARSKI:def 3;
reconsider UN = union { H₁(Y) where Y is Element of X1 : Y in X1 } as Cardinal by A6, Th33;
card { H₁(Y) where Y is Element of X1 : Y in X1 } c= card X1 from TREES_2:sch 2();
then card { H₁(Y) where Y is Element of X1 : Y in X1 } in cf M by A1, ORDINAL1:22;
then A8: UN in M by A7, CARD_5:38;
for Y being set st Y in X1 holds
card Y c= UN

proof

let Y be set ; :: thesis: ( Y in X1 implies card Y c= UN )
assume A9: Y in X1 ; :: thesis: card Y c= UN
card Y in { H₁(Y) where Y is Element of X1 : Y in X1 } by A9;
hence card Y c= UN by ZFMISC_1:92; :: thesis: verum

end;

then A10: card (union X1) c= (card X1) *` UN by CARD_3:133;
A11: (card X1) *` UN in (cf M) *` M by A1, A8, CARD_4:82;
( cf M c= M & M c= M ) by CARD_5:def 2;
then (cf M) *` M c= M *` M by CARD_3:136;
then (cf M) *` M c= M by CARD_4:77;
hence card (union X) in M by A10, A11, ORDINAL1:22; :: thesis: verum

end;

end;