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

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 )
;

end;

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;then {} c< M by XBOOLE_0:def 8;

hence card (union X) in M by A3, ORDINAL1:11, ZFMISC_1:2; :: thesis: verum

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

then reconsider X1 = X as non empty set ;

deffunc H_{1}( set ) -> set = card $1;

set CARDS = { H_{1}(Y) where Y is Element of X1 : Y in X1 } ;

card { H_{1}(Y) where Y is Element of X1 : Y in X1 } c= card X1
from TREES_2:sch 2();

then A4: card { H_{1}(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_{1}(Y) where Y is Element of X1 : Y in X1 } holds

( x in M & ex y being set st

( y in { H_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) )
_{1}(Y) where Y is Element of X1 : Y in X1 } holds

ex y being set st

( y in { H_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal )
;

then reconsider UN = union { H_{1}(Y) where Y is Element of X1 : Y in X1 } as Cardinal by Th32;

for x being object st x in { H_{1}(Y) where Y is Element of X1 : Y in X1 } holds

x in M by A5;

then { H_{1}(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

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;deffunc H

set CARDS = { H

card { H

then A4: card { H

A5: for x being set st x in { H

( x in M & ex y being set st

( y in { H

proof

then
for x being set st x in { H
let x be set ; :: thesis: ( x in { H_{1}(Y) where Y is Element of X1 : Y in X1 } implies ( x in M & ex y being set st

( y in { H_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal ) ) )

assume x in { H_{1}(Y) where Y is Element of X1 : Y in X1 }
; :: thesis: ( x in M & ex y being set st

( y in { H_{1}(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_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= y & y is Cardinal )

take card Y ; :: thesis: ( card Y in { H_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal )

thus ( card Y in { H_{1}(Y) where Y is Element of X1 : Y in X1 } & x c= card Y & card Y is Cardinal )
by A6; :: thesis: verum

end;( y in { H

assume x in { H

( y in { H

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

take card Y ; :: thesis: ( card Y in { H

thus ( card Y in { H

ex y being set st

( y in { H

then reconsider UN = union { H

for x being object st x in { H

x in M by A5;

then { H

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

then A8:
card (union X1) c= (card X1) *` UN
by CARD_2:87;
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_{1}(Y) where Y is Element of X1 : Y in X1 }
;

hence card Y c= UN by ZFMISC_1:74; :: thesis: verum

end;assume Y in X1 ; :: thesis: card Y c= UN

then card Y in { H

hence card Y c= UN by ZFMISC_1:74; :: thesis: verum

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