let phi be Ordinal-Sequence; :: thesis: ( phi is increasing & dom phi is limit_ordinal implies sup phi is limit_ordinal )

assume that

A1: phi is increasing and

A2: dom phi is limit_ordinal ; :: thesis: sup phi is limit_ordinal

assume that

A1: phi is increasing and

A2: dom phi is limit_ordinal ; :: thesis: sup phi is limit_ordinal

now :: thesis: for A being Ordinal st A in sup phi holds

succ A in sup phi

hence
sup phi is limit_ordinal
by ORDINAL1:28; :: thesis: verumsucc A in sup phi

let A be Ordinal; :: thesis: ( A in sup phi implies succ A in sup phi )

assume A in sup phi ; :: thesis: succ A in sup phi

then consider B being Ordinal such that

A3: B in rng phi and

A4: A c= B by ORDINAL2:21;

consider x being object such that

A5: x in dom phi and

A6: B = phi . x by A3, FUNCT_1:def 3;

reconsider x = x as Ordinal by A5;

A7: succ x in dom phi by A2, A5, ORDINAL1:28;

reconsider C = phi . (succ x) as Ordinal ;

x in succ x by ORDINAL1:6;

then B in C by A1, A6, A7;

then A8: succ B c= C by ORDINAL1:21;

A9: succ A c= succ B by A4, ORDINAL2:1;

C in rng phi by A7, FUNCT_1:def 3;

then C in sup phi by ORDINAL2:19;

then succ B in sup phi by A8, ORDINAL1:12;

hence succ A in sup phi by A9, ORDINAL1:12; :: thesis: verum

end;assume A in sup phi ; :: thesis: succ A in sup phi

then consider B being Ordinal such that

A3: B in rng phi and

A4: A c= B by ORDINAL2:21;

consider x being object such that

A5: x in dom phi and

A6: B = phi . x by A3, FUNCT_1:def 3;

reconsider x = x as Ordinal by A5;

A7: succ x in dom phi by A2, A5, ORDINAL1:28;

reconsider C = phi . (succ x) as Ordinal ;

x in succ x by ORDINAL1:6;

then B in C by A1, A6, A7;

then A8: succ B c= C by ORDINAL1:21;

A9: succ A c= succ B by A4, ORDINAL2:1;

C in rng phi by A7, FUNCT_1:def 3;

then C in sup phi by ORDINAL2:19;

then succ B in sup phi by A8, ORDINAL1:12;

hence succ A in sup phi by A9, ORDINAL1:12; :: thesis: verum