let X be set ; :: thesis: for M being Cardinal st X c= M & card X in cf M holds
( sup X in M & union X in M )
let M be Cardinal; :: thesis: ( X c= M & card X in cf M implies ( sup X in M & union X in M ) )
assume that
A1: X c= M and
A2: card X in cf M ; :: thesis: ( sup X in M & union X in M )
set A = order_type_of (RelIncl X);
A3: card (order_type_of (RelIncl X)) = card X by A1, Th7;
consider N being Cardinal such that
A4: N c= card (order_type_of (RelIncl X)) and
A5: order_type_of (RelIncl X) is_cofinal_with N and
for C being Ordinal st order_type_of (RelIncl X) is_cofinal_with C holds
N c= C by Th9;
sup X is_cofinal_with order_type_of (RelIncl X) by A1, Th6;
then A6: sup X is_cofinal_with N by A5, ORDINAL4:37;
A7: now :: thesis: not sup X = M
assume sup X = M ; :: thesis: contradiction
then cf M c= N by A6, Def1;
hence contradiction by A2, A3, A4, CARD_1:4; :: thesis: verum
end;
for x being object st x in X holds
x is Ordinal by A1;
then reconsider A = union X as epsilon-transitive epsilon-connected set by ORDINAL1:23;
A8: sup M = M by ORDINAL2:18;
sup X c= sup M by A1, ORDINAL2:22;
then A9: sup X c< M by A8, A7;
hence sup X in M by ORDINAL1:11; :: thesis: union X in M
A c= sup X
proof
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in A or x in sup X )
assume x in A ; :: thesis: x in sup X
then consider Y being set such that
A10: x in Y and
A11: Y in X by TARSKI:def 4;
reconsider Y = Y as Ordinal by A1, A11;
Y in sup X by A11, ORDINAL2:19;
then Y c= sup X by ORDINAL1:def 2;
hence x in sup X by A10; :: thesis: verum
end;
hence union X in M by A9, ORDINAL1:11, ORDINAL1:12; :: thesis: verum