let X be set ; :: thesis: ( ( for x being set st x in X holds

ex y being set st

( y in X & x c= y & y is Cardinal ) ) implies union X is Cardinal )

assume A1: for x being set st x in X holds

ex y being set st

( y in X & x c= y & y is Cardinal ) ; :: thesis: union X is Cardinal

for x being set st x in union X holds

( x is Ordinal & x c= union X )

A8: UNX c= card UNX

hence union X is Cardinal by A8, XBOOLE_0:def 10; :: thesis: verum

ex y being set st

( y in X & x c= y & y is Cardinal ) ) implies union X is Cardinal )

assume A1: for x being set st x in X holds

ex y being set st

( y in X & x c= y & y is Cardinal ) ; :: thesis: union X is Cardinal

for x being set st x in union X holds

( x is Ordinal & x c= union X )

proof

then reconsider UNX = union X as epsilon-transitive epsilon-connected set by ORDINAL1:19;
let x be set ; :: thesis: ( x in union X implies ( x is Ordinal & x c= union X ) )

assume x in union X ; :: thesis: ( x is Ordinal & x c= union X )

then consider Y being set such that

A2: x in Y and

A3: Y in X by TARSKI:def 4;

consider y being set such that

A4: y in X and

A5: Y c= y and

A6: y is Cardinal by A1, A3;

reconsider y1 = y as Cardinal by A6;

A7: y1 c= union X by A4, ZFMISC_1:74;

x in y1 by A2, A5;

hence x is Ordinal ; :: thesis: x c= union X

x c= y1 by A2, A5, ORDINAL1:def 2;

hence x c= union X by A7; :: thesis: verum

end;assume x in union X ; :: thesis: ( x is Ordinal & x c= union X )

then consider Y being set such that

A2: x in Y and

A3: Y in X by TARSKI:def 4;

consider y being set such that

A4: y in X and

A5: Y c= y and

A6: y is Cardinal by A1, A3;

reconsider y1 = y as Cardinal by A6;

A7: y1 c= union X by A4, ZFMISC_1:74;

x in y1 by A2, A5;

hence x is Ordinal ; :: thesis: x c= union X

x c= y1 by A2, A5, ORDINAL1:def 2;

hence x c= union X by A7; :: thesis: verum

A8: UNX c= card UNX

proof

card UNX c= UNX
by CARD_1:8;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in UNX or x in card UNX )

assume A9: x in UNX ; :: thesis: x in card UNX

reconsider x1 = x as Ordinal by A9;

assume not x in card UNX ; :: thesis: contradiction

then card UNX c= x1 by ORDINAL1:16;

then card UNX in UNX by A9, ORDINAL1:12;

then consider Y being set such that

A10: card UNX in Y and

A11: Y in X by TARSKI:def 4;

consider y being set such that

A12: y in X and

A13: Y c= y and

A14: y is Cardinal by A1, A11;

reconsider y1 = y as Cardinal by A14;

card y1 c= card UNX by A12, CARD_1:11, ZFMISC_1:74;

then A15: y1 c= card UNX ;

card UNX in y1 by A10, A13;

then card UNX in card UNX by A15;

hence contradiction ; :: thesis: verum

end;assume A9: x in UNX ; :: thesis: x in card UNX

reconsider x1 = x as Ordinal by A9;

assume not x in card UNX ; :: thesis: contradiction

then card UNX c= x1 by ORDINAL1:16;

then card UNX in UNX by A9, ORDINAL1:12;

then consider Y being set such that

A10: card UNX in Y and

A11: Y in X by TARSKI:def 4;

consider y being set such that

A12: y in X and

A13: Y c= y and

A14: y is Cardinal by A1, A11;

reconsider y1 = y as Cardinal by A14;

card y1 c= card UNX by A12, CARD_1:11, ZFMISC_1:74;

then A15: y1 c= card UNX ;

card UNX in y1 by A10, A13;

then card UNX in card UNX by A15;

hence contradiction ; :: thesis: verum

hence union X is Cardinal by A8, XBOOLE_0:def 10; :: thesis: verum