let phi be Ordinal-Sequence; :: thesis: for A being Ordinal st phi is increasing holds
phi " A is Ordinal
let A be Ordinal; :: thesis: ( phi is increasing implies phi " A is Ordinal )
assume A1: for A, B being Ordinal st A in B & B in dom phi holds
phi . A in phi . B ; :: according to ORDINAL2:def 16 :: thesis: phi " A is Ordinal

now

let X be set ; :: thesis: ( X in phi " A implies ( X is Ordinal & X c= phi " A ) )
assume X in phi " A ; :: thesis: ( X is Ordinal & X c= phi " A )
then A2: ( X in dom phi & phi . X in A ) by FUNCT_1:def 13;
hence X is Ordinal ; :: thesis: X c= phi " A
reconsider B = X as Ordinal by A2;
thus X c= phi " A :: thesis: verum

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in phi " A )
assume A3: x in X ; :: thesis: x in phi " A
then x in B ;
then reconsider C = x, D = phi . B as Ordinal ;
A5: C in dom phi by A2, A3, ORDINAL1:19;
reconsider E = phi . C as Ordinal ;
E in D by A1, A2, A3;
then phi . x in A by A2, ORDINAL1:19;
hence x in phi " A by A5, FUNCT_1:def 13; :: thesis: verum

end;

end;

hence phi " A is Ordinal by ORDINAL1:31; :: thesis: verum