let l be limit_ordinal non empty Ordinal; 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; ( 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) )
; (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
reconsider u = union (rng h) as Ordinal ;
A7:
h <> {}
by A4;
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;
XBOOLE_0:def 10 l c= a
let x be
Ordinal;
ORDINAL1:def 5 ( not x in l or x in a )
assume A12:
x in l
;
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;
verum
end;
hence
(criticals f) . l = Union ((criticals f) | l)
by A11; verum