let l be limit_ordinal non empty Ordinal; :: thesis: for g being Ordinal-Sequence-valued Sequence st dom g <> {} & ( for a being Ordinal st a in dom g holds
g . a is normal ) & l in dom (criticals g) holds
(criticals g) . l = Union ((criticals g) | l)
let F be Ordinal-Sequence-valued Sequence; :: thesis: ( dom F <> {} & ( for a being Ordinal st a in dom F holds
F . a is normal ) & l in dom (criticals F) implies (criticals F) . l = Union ((criticals F) | l) )
assume A1: dom F <> {} ; :: thesis: ( ex a being Ordinal st
( a in dom F & not F . a is normal ) or not l in dom (criticals F) or (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 A2: ( ( for a being Ordinal st a in dom F holds
F . a is normal ) & l in dom (criticals F) ) ; :: thesis: (criticals F) . l = Union ((criticals F) | l)
A3: now :: thesis: for a being Ordinal st a in dom F holds
( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l )
let a be Ordinal; :: thesis: ( a in dom F implies ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) )
set f = F . a;
assume a in dom F ; :: thesis: ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l )
then (criticals F) . l is_a_fixpoint_of F . a by A2, Th47;
hence ( (criticals F) . l in dom (F . a) & (F . a) . ((criticals F) . l) = (criticals F) . l ) ; :: thesis: verum
end;
A4: l c= dom (criticals F) by A2, ORDINAL1:def 2;
then A5: dom h = l by RELAT_1:62;
A6: for a being Ordinal
for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a
proof
let a be Ordinal; :: thesis: for x being set st a in dom F & x in rng h holds
x is_a_fixpoint_of F . a
let x be set ; :: thesis: ( a in dom F & x in rng h implies x is_a_fixpoint_of F . a )
assume A7: ( a in dom F & x in rng h ) ; :: thesis: x is_a_fixpoint_of F . a
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 A4, A5, A8, FUNCT_1:47;
hence x is_a_fixpoint_of F . a by A7, Th47; :: thesis: verum
end;
reconsider u = union (rng h) as Ordinal ;
A9: h <> {} by A5;
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
A10: ( y in dom h & x = h . y ) by FUNCT_1:def 3;
( x = (criticals F) . y & y in dom (criticals F) ) by A4, A5, A10, FUNCT_1:47;
then x in (criticals F) . l by A2, A5, A10, ORDINAL2:def 12;
hence x c= (criticals F) . l by ORDINAL1:def 2; :: thesis: verum
end;
then A11: u c= (criticals F) . l by ZFMISC_1:76;
now :: thesis: for c being Ordinal st c in dom F holds
u is_a_fixpoint_of F . c
let c be Ordinal; :: thesis: ( c in dom F implies u is_a_fixpoint_of F . c )
set f = F . c;
assume A12: c in dom F ; :: thesis: u is_a_fixpoint_of F . c
then A13: (criticals F) . l in dom (F . c) by A3;
then A14: u in dom (F . c) by A11, ORDINAL1:12;
A15: F . c is normal by A2, A12;
for x being set st x in rng h holds
x is_a_fixpoint_of F . c by A6, A12;
then u = (F . c) . u by A9, A13, A15, Th37, A11, ORDINAL1:12;
hence u is_a_fixpoint_of F . c by A14; :: thesis: verum
end;
then consider a being Ordinal such that
A16: ( a in dom (criticals F) & u = (criticals F) . a ) by A1, Th50;
a = l
proof
thus a c= l by A2, A16, A11, 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 A17: x in l ; :: thesis: x in a
then A18: succ x in l by ORDINAL1:28;
then A19: ( (criticals F) . x = h . x & (criticals F) . (succ x) = h . (succ x) & h . (succ x) in rng h ) by A5, A17, FUNCT_1:47, FUNCT_1:def 3;
x in succ x by ORDINAL1:6;
then h . x in h . (succ x) by A5, A18, ORDINAL2:def 12;
then (criticals F) . x in u by A19, TARSKI:def 4;
then ( (criticals F) . a c/= (criticals F) . x & x in dom (criticals F) ) by A4, A16, A17, Th4;
then a c/= x by A16, Th22;
hence x in a by Th4; :: thesis: verum
end;
hence (criticals F) . l = Union ((criticals F) | l) by A16; :: thesis: verum