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 A0: omega in W ; :: thesis: criticals F is Ordinal-Sequence of W
set G = criticals F;
A1: ( dom F = On W & rng F c= On W ) by FUNCT_2:def 1, RELAT_1:def 19;
D2: rng (criticals F) c= rng F by Th03;
then A2: rng (criticals F) c= On W by A1, XBOOLE_1:1;
dom (criticals F) = On W

proof

thus dom (criticals F) c= On W by A1, Th05; :: according to XBOOLE_0:def 10 :: thesis: On W c= dom (criticals F)
let a be ordinal number ; :: 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 A3: 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
A4: ( 0-element_of W in a0 & a0 is_a_fixpoint_of F ) by A0, Th38;
consider a1 being Ordinal such that
A5: ( a1 in dom (criticals F) & a0 = (criticals F) . a1 ) by A4, Th06;
00: S₁[ {} ] by A5, ORDINAL1:12, XBOOLE_1:2;
01: for a being ordinal number st S₁[a] holds
S₁[ succ a]

proof

let a be ordinal number ; :: thesis: ( S₁[a] implies S₁[ succ a] )
assume B1: ( S₁[a] & succ a in W ) ; :: thesis: succ a in dom (criticals F)
B4: a c= succ a by ORDINAL3:1;
then (criticals F) . a in rng (criticals F) by B1, CLASSES1:def 1, FUNCT_1:def 3;
then (criticals F) . a in W by A2, ORDINAL1:def 9;
then consider b being ordinal number such that
B2: ( (criticals F) . a in b & b is_a_fixpoint_of F ) by A0, Th38;
consider c being ordinal number such that
B3: ( c in dom (criticals F) & b = (criticals F) . c ) by B2, Th06;
a in c by B1, B4, B2, B3, ThN5, CLASSES1:def 1;
then succ a c= c by ORDINAL1:21;
hence succ a in dom (criticals F) by B3, ORDINAL1:12; :: thesis: verum

end;

02: for a being ordinal number st a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₁[b] ) holds
S₁[a]

proof

let a be ordinal number ; :: thesis: ( a <> {} & a is limit_ordinal & ( for b being ordinal number st b in a holds
S₁[b] ) implies S₁[a] )
assume that
C1: ( a <> {} & a is limit_ordinal ) and
C2: for b being ordinal number st b in a holds
S₁[b] and
C3: 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 by XBOOLE_1:1;
then card ((criticals F) .: a) in W by C3, CLASSES1:def 1;
then card ((criticals F) .: a) in On W by ORDINAL1:def 9;
then C4: card ((criticals F) .: a) in card W by CLASSES2:9;
D5: (criticals F) .: a c= rng (criticals F) by RELAT_1:111;
then C5: (criticals F) .: a c= On W by A2, XBOOLE_1:1;
reconsider u = union ((criticals F) .: a) as Ordinal by D5, A2, ORDINAL3:4, XBOOLE_1:1;
On W c= W by ORDINAL2:7;
then (criticals F) .: a c= W by C5, XBOOLE_1:1;
then (criticals F) .: a in W by C4, CLASSES1:1;
then u in W by CLASSES2:59;
then consider b being ordinal number such that
B2: ( u in b & b is_a_fixpoint_of F ) by A0, Th38;
C6: a c= dom (criticals F)

proof

let c be ordinal number ; :: according to ORDINAL1:def 5 :: thesis: ( not c in a or c in dom (criticals F) )
assume C7: c in a ; :: thesis: c in dom (criticals F)
then c in W by C3, ORDINAL1:10;
hence c in dom (criticals F) by C2, C7; :: thesis: verum

end;

now

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

end;

hence a in dom (criticals F) by C1, C6, B2, Th19; :: thesis: verum

end;

for b being ordinal number holds S₁[b] from ORDINAL2:sch 1(00, 01, 02);
hence a in dom (criticals F) by A3; :: thesis: verum

end;

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