let X be set ; :: thesis: for f being Ordinal-Sequence st f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) holds
union X = f . (union X)
let f be Ordinal-Sequence; :: thesis: ( f is normal & union X in dom f & not X is empty & ( for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ) implies union X = f . (union X) )
assume that
A1: f is normal and
A2: ( union X in dom f & not X is empty ) and
A3: for x being set st x in X holds
ex y being set st
( x c= y & y in X & y is_a_fixpoint_of f ) ; :: thesis: union X = f . (union X)
reconsider l = union X as Ordinal by A2;
per cases ( ex a being Ordinal st
( a in X & ( for b being Ordinal st b in X holds
b c= a ) ) or for a being Ordinal holds
( not a in X or ex b being Ordinal st
( b in X & not b c= a ) ) ) ;
suppose ex a being Ordinal st
( a in X & ( for b being Ordinal st b in X holds
b c= a ) ) ; :: thesis: union X = f . (union X)
then consider a being Ordinal such that
A4: ( a in X & ( for b being Ordinal st b in X holds
b c= a ) ) ;
now :: thesis: for x being set st x in X holds
x c= a
let x be set ; :: thesis: ( x in X implies x c= a )
assume x in X ; :: thesis: x c= a
then consider y being set such that
A5: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3;
y c= a by A4, A5;
hence x c= a by A5; :: thesis: verum
end;
then ( union X c= a & a c= union X ) by A4, ZFMISC_1:74, ZFMISC_1:76;
then A6: union X = a ;
then consider y being set such that
A7: ( union X c= y & y in X & y is_a_fixpoint_of f ) by A3, A4;
y c= union X by A6, A7, A4;
then y = union X by A7;
hence union X = f . (union X) by A7; :: thesis: verum
end;
suppose A8: for a being Ordinal holds
( not a in X or ex b being Ordinal st
( b in X & not b c= a ) ) ; :: thesis: union X = f . (union X)
set y0 = the Element of X;
consider x0 being set such that
A9: ( the Element of X c= x0 & x0 in X & x0 is_a_fixpoint_of f ) by A2, A3;
consider b being Ordinal such that
A10: ( b in X & b c/= x0 ) by A9, A8;
now :: thesis: for a being Ordinal st a in l holds
succ a in l
let a be Ordinal; :: thesis: ( a in l implies succ a in l )
assume a in l ; :: thesis: succ a in l
then consider x being set such that
A11: ( a in x & x in X ) by TARSKI:def 4;
consider y being set such that
A12: ( x c= y & y in X & y is_a_fixpoint_of f ) by A3, A11;
consider b being Ordinal such that
A13: ( b in X & b c/= y ) by A8, A12;
( succ a c= y & y in b ) by A11, A12, A13, Th4, ORDINAL1:21;
then succ a in b by ORDINAL1:12;
hence succ a in l by A13, TARSKI:def 4; :: thesis: verum
end;
then reconsider l = l as limit_ordinal non empty Ordinal by A10, ORDINAL1:28, TARSKI:def 4;
thus union X c= f . (union X) by A2, A1, ORDINAL4:10; :: according to XBOOLE_0:def 10 :: thesis: f . (union X) c= union X
reconsider g = f | l as increasing Ordinal-Sequence by A1, ORDINAL4:15;
l c= dom f by A2, ORDINAL1:def 2;
then A14: dom g = l by RELAT_1:62;
then A15: Union g is_limes_of g by ORDINAL5:6;
f . l is_limes_of g by A1, A2, ORDINAL2:def 13;
then A16: ( f . l = lim g & Union g = lim g ) by A15, ORDINAL2:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . (union X) or x in union X )
assume x in f . (union X) ; :: thesis: x in union X
then consider z being object such that
A17: ( z in dom g & x in g . z ) by A16, CARD_5:2;
consider y being set such that
A18: ( z in y & y in X ) by A14, A17, TARSKI:def 4;
consider t being set such that
A19: ( y c= t & t in X & t is_a_fixpoint_of f ) by A18, A3;
A20: ( t in dom f & t = f . t ) by A19;
then reconsider z = z, t = t as Ordinal by A17;
( f . z = g . z & z in t ) by A17, A18, A19, FUNCT_1:47;
then g . z in t by A1, A20, ORDINAL2:def 12;
then x in t by A17, ORDINAL1:10;
hence x in union X by A19, TARSKI:def 4; :: thesis: verum
end;
end;