let W be Universe; :: thesis: for F being normal Ordinal-Sequence of W st omega in W holds
criticals F is Ordinal-Sequence of W
let F be normal Ordinal-Sequence of W; :: thesis: ( omega in W implies criticals F is Ordinal-Sequence of W )
assume A1: omega in W ; :: thesis: criticals F is Ordinal-Sequence of W
set G = criticals F;
A2: ( dom F = On W & rng F c= On W ) by FUNCT_2:def 1, RELAT_1:def 19;
A3: rng (criticals F) c= rng F by Th30;
then A4: rng (criticals F) c= On W by A2;
dom (criticals F) = On W

proof

thus dom (criticals F) c= On W by A2, Th32; :: according to XBOOLE_0:def 10 :: thesis: On W c= dom (criticals F)
let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in On W or a in dom (criticals F) )
assume a in On W ; :: thesis: a in dom (criticals F)
then A5: a in W by ORDINAL1:def 9;
defpred S₁[ Ordinal] means ( $1 in W implies $1 in dom (criticals F) );
consider a0 being Ordinal such that
A6: ( 0-element_of W in a0 & a0 is_a_fixpoint_of F ) by A1, Th43;
consider a1 being Ordinal such that
A7: ( a1 in dom (criticals F) & a0 = (criticals F) . a1 ) by A6, Th33;
A8: S₁[ 0 ] by A7, ORDINAL1:12, XBOOLE_1:2;
A9: for a being Ordinal st S₁[a] holds
S₁[ succ a]

proof

let a be Ordinal; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume A10: ( S₁[a] & succ a in W ) ; :: thesis: succ a in dom (criticals F)
A11: a c= succ a by ORDINAL3:1;
then (criticals F) . a in rng (criticals F) by A10, CLASSES1:def 1, FUNCT_1:def 3;
then (criticals F) . a in W by A4, ORDINAL1:def 9;
then consider b being Ordinal such that
A12: ( (criticals F) . a in b & b is_a_fixpoint_of F ) by A1, Th43;
consider c being Ordinal such that
A13: ( c in dom (criticals F) & b = (criticals F) . c ) by A12, Th33;
a in c by A10, A11, A12, A13, Th23, CLASSES1:def 1;
then succ a c= c by ORDINAL1:21;
hence succ a in dom (criticals F) by A13, ORDINAL1:12; :: thesis: verum

end;

A14: for a being Ordinal st a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S₁[b] ) holds
S₁[a]

proof

let a be Ordinal; :: thesis: ( a <> 0 & a is limit_ordinal & ( for b being Ordinal st b in a holds
S₁[b] ) implies S₁[a] )
assume that
A15: ( a <> 0 & a is limit_ordinal ) and
A16: for b being Ordinal st b in a holds
S₁[b] and
A17: a in W ; :: thesis: a in dom (criticals F)
set X = (criticals F) .: a;
( card ((criticals F) .: a) c= card a & card a c= a ) by CARD_1:8, CARD_1:67;
then card ((criticals F) .: a) c= a ;
then card ((criticals F) .: a) in W by A17, CLASSES1:def 1;
then card ((criticals F) .: a) in On W by ORDINAL1:def 9;
then A18: card ((criticals F) .: a) in card W by CLASSES2:9;
A19: (criticals F) .: a c= rng (criticals F) by RELAT_1:111;
then A20: (criticals F) .: a c= On W by A4;
reconsider u = union ((criticals F) .: a) as Ordinal by A19, A4, ORDINAL3:4, XBOOLE_1:1;
On W c= W by ORDINAL2:7;
then (criticals F) .: a c= W by A20;
then (criticals F) .: a in W by A18, CLASSES1:1;
then u in W by CLASSES2:59;
then consider b being Ordinal such that
A21: ( u in b & b is_a_fixpoint_of F ) by A1, Th43;
A22: a c= dom (criticals F)

proof

let c be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not c in a or c in dom (criticals F) )
assume A23: c in a ; :: thesis: c in dom (criticals F)
then c in W by A17, ORDINAL1:10;
hence c in dom (criticals F) by A16, A23; :: thesis: verum

end;

now :: thesis: for x being set st x in a holds
(criticals F) . x in b

let x be set ; :: thesis: ( x in a implies (criticals F) . x in b )
assume x in a ; :: thesis: (criticals F) . x in b
then (criticals F) . x in (criticals F) .: a by A22, FUNCT_1:def 6;
then ( (criticals F) . x is Ordinal & (criticals F) . x c= u ) by ZFMISC_1:74;
hence (criticals F) . x in b by A21, ORDINAL1:12; :: thesis: verum

end;

hence a in dom (criticals F) by A15, A22, A21, Th38; :: thesis: verum

end;

for b being Ordinal holds S₁[b] from ORDINAL2:sch 1(A8, A9, A14);
hence a in dom (criticals F) by A5; :: thesis: verum

end;

hence criticals F is Ordinal-Sequence of W by A3, A2, FUNCT_2:2, XBOOLE_1:1; :: thesis: verum