let a be Ordinal; :: thesis: for l being limit_ordinal non empty Ordinal
for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let l be limit_ordinal non empty Ordinal; :: thesis: for f being Ordinal-Sequence st l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) holds
l in dom (criticals f)
let f be Ordinal-Sequence; :: thesis: ( l c= dom (criticals f) & a is_a_fixpoint_of f & ( for x being set st x in l holds
(criticals f) . x in a ) implies l in dom (criticals f) )
set g = criticals f;
assume that
A1: l c= dom (criticals f) and
A2: a is_a_fixpoint_of f and
A3: for x being set st x in l holds
(criticals f) . x in a ; :: thesis: l in dom (criticals f)
consider b being Ordinal such that
A4: ( b in dom (criticals f) & a = (criticals f) . b ) by A2, Th33;
l c= b
proof
let x be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not x in l or x in b )
assume x in l ; :: thesis: x in b
then ( x in dom (criticals f) & (criticals f) . x in (criticals f) . b ) by A1, A3, A4;
hence x in b by A4, Th23; :: thesis: verum
end;
hence l in dom (criticals f) by A4, ORDINAL1:12; :: thesis: verum