let g be Ordinal-Sequence-valued Sequence; :: thesis: { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } is ordinal-membered
now :: thesis: for x being set st x in { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } holds
x is ordinal
let x be set ; :: thesis: ( x in { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } implies x is ordinal )
assume x in { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } ; :: thesis: x is ordinal
then ex a being Element of dom (g . 0) st
( x = a & a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) ;
hence x is ordinal ; :: thesis: verum
end;
hence { a where a is Element of dom (g . 0) : ( a in dom (g . 0) & ( for f being Ordinal-Sequence st f in rng g holds
a is_a_fixpoint_of f ) ) } is ordinal-membered by Th1; :: thesis: verum