let l be limit_ordinal non empty Ordinal; :: thesis: for f being Ordinal-Sequence st f is normal & l in dom (criticals f) holds
(criticals f) . l = Union ((criticals f) | l)
let f be Ordinal-Sequence; :: thesis: ( f is normal & l in dom (criticals f) implies (criticals f) . l = Union ((criticals f) | l) )
set g = criticals f;
reconsider h = (criticals f) | l as increasing Ordinal-Sequence by ORDINAL4:15;
set X = rng h;
assume A1: ( f is normal & l in dom (criticals f) ) ; :: thesis: (criticals f) . l = Union ((criticals f) | l)
then (criticals f) . l is_a_fixpoint_of f by Th29;
then A2: ( (criticals f) . l in dom f & f . ((criticals f) . l) = (criticals f) . l ) ;
A3: l c= dom (criticals f) by A1, ORDINAL1:def 2;
then A4: dom h = l by RELAT_1:62;
A5: for x being set st x in rng h holds
x is_a_fixpoint_of f
proof
let x be set ; :: thesis: ( x in rng h implies x is_a_fixpoint_of f )
assume x in rng h ; :: thesis: x is_a_fixpoint_of f
then consider y being object such that
A6: ( y in dom h & x = h . y ) by FUNCT_1:def 3;
( x = (criticals f) . y & y in dom (criticals f) ) by A3, A4, A6, FUNCT_1:47;
hence x is_a_fixpoint_of f by Th29; :: thesis: verum
end;
reconsider u = union (rng h) as Ordinal ;
A7: h <> {} by A4;
now :: thesis: for x being set st x in rng h holds
x c= (criticals f) . l
let x be set ; :: thesis: ( x in rng h implies x c= (criticals f) . l )
assume x in rng h ; :: thesis: x c= (criticals f) . l
then consider y being object such that
A8: ( y in dom h & x = h . y ) by FUNCT_1:def 3;
( x = (criticals f) . y & y in dom (criticals f) ) by A3, A4, A8, FUNCT_1:47;
then x in (criticals f) . l by A1, A4, A8, ORDINAL2:def 12;
hence x c= (criticals f) . l by ORDINAL1:def 2; :: thesis: verum
end;
then A9: union (rng h) c= (criticals f) . l by ZFMISC_1:76;
then A10: u in dom f by A2, ORDINAL1:12;
u = f . u by A1, A5, A7, A9, Th37, A2, ORDINAL1:12;
then u is_a_fixpoint_of f by A10;
then consider a being Ordinal such that
A11: ( a in dom (criticals f) & u = (criticals f) . a ) by Th33;
a = l
proof
thus a c= l by A1, A11, A9, Th22; :: according to XBOOLE_0:def 10 :: thesis: l c= a
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in l or x in a )
assume A12: x in l ; :: thesis: x in a
then A13: succ x in l by ORDINAL1:28;
then A14: ( (criticals f) . x = h . x & (criticals f) . (succ x) = h . (succ x) & h . (succ x) in rng h ) by A4, A12, FUNCT_1:47, FUNCT_1:def 3;
x in succ x by ORDINAL1:6;
then h . x in h . (succ x) by A4, A13, ORDINAL2:def 12;
then (criticals f) . x in u by A14, TARSKI:def 4;
then ( (criticals f) . a c/= (criticals f) . x & x in dom (criticals f) ) by A3, A11, A12, Th4;
then a c/= x by A11, Th22;
hence x in a by Th4; :: thesis: verum
end;
hence (criticals f) . l = Union ((criticals f) | l) by A11; :: thesis: verum