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

{} c= M ;
then {} c< M by XBOOLE_0:def 8;
hence card (union X) in M by A3, ORDINAL1:11, 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 } ;
card { H₁(Y) where Y is Element of X1 : Y in X1 } c= card X1 from TREES_2:sch 2();
then A4: card { H₁(Y) where Y is Element of X1 : Y in X1 } in cf M by A1, ORDINAL1:12;
A5: 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 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 ) )
then consider Y being Element of X1 such that
A6: card Y = x and
Y in X1 ;
thus x in M by A2, A6; :: 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 A6; :: thesis: verum

end;

then 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 reconsider UN = union { H₁(Y) where Y is Element of X1 : Y in X1 } as Cardinal by Th32;
for x being object st x in { H₁(Y) where Y is Element of X1 : Y in X1 } holds
x in M by A5;
then { H₁(Y) where Y is Element of X1 : Y in X1 } c= M ;
then UN in M by A4, CARD_5:26;
then A7: (card X1) *` UN in (cf M) *` M by A1, CARD_4:20;
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 Y in X1 ; :: thesis: card Y c= UN
then card Y in { H₁(Y) where Y is Element of X1 : Y in X1 } ;
hence card Y c= UN by ZFMISC_1:74; :: thesis: verum

end;

then A8: card (union X1) c= (card X1) *` UN by CARD_2:87;
cf M c= M by CARD_5:def 1;
then (cf M) *` M c= M *` M by CARD_2:90;
then (cf M) *` M c= M by CARD_4:15;
hence card (union X) in M by A8, A7, ORDINAL1:12; :: thesis: verum

end;

end;