let X be non empty set ; :: thesis: ( ( for x being object st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ) implies union X is epsilon Ordinal )
assume A1: for x being object st x in X holds
( x is epsilon Ordinal & ex e being epsilon Ordinal st
( x in e & e in X ) ) ; :: thesis: union X is epsilon Ordinal
then for x being object st x in X holds
x is Ordinal ;
then reconsider a = union X as epsilon-transitive epsilon-connected set by ORDINAL1:23;
now :: thesis: for b being Ordinal st b in a holds
succ b in a
let b be Ordinal; :: thesis: ( b in a implies succ b in a )
assume b in a ; :: thesis: succ b in a
then consider x being set such that
A2: ( b in x & x in X ) by TARSKI:def 4;
reconsider x = x as epsilon Ordinal by A2, A1;
succ b in x by A2, ORDINAL1:28;
hence succ b in a by A2, TARSKI:def 4; :: thesis: verum
end;
then A3: a is limit_ordinal by ORDINAL1:28;
set z = the Element of X;
ex e being epsilon Ordinal st
( the Element of X in e & e in X ) by A1;
then A4: a <> {} by TARSKI:def 4;
a is epsilon
proof
thus exp (omega,a) c= a :: according to XBOOLE_0:def 10,ORDINAL5:def 5 :: thesis: not a c/= exp (omega,a)
proof
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in exp (omega,a) or x in a )
assume x in exp (omega,a) ; :: thesis: x in a
then consider b being Ordinal such that
A5: ( b in a & x in exp (omega,b) ) by A3, A4, Th11;
consider y being set such that
A6: ( b in y & y in X ) by A5, TARSKI:def 4;
reconsider y = y as epsilon Ordinal by A1, A6;
exp (omega,b) in exp (omega,y) by A6, ORDINAL4:24;
then exp (omega,b) in y by Def5;
then x in y by A5, ORDINAL1:10;
hence x in a by A6, TARSKI:def 4; :: thesis: verum
end;
thus not a c/= exp (omega,a) by ORDINAL4:32; :: thesis: verum
end;
hence union X is epsilon Ordinal ; :: thesis: verum