let A, B be Ordinal; :: thesis: ( A is_cofinal_with B implies ( A is limit_ordinal iff B is limit_ordinal ) )

given psi being Ordinal-Sequence such that A1: dom psi = B and

A2: rng psi c= A and

A3: psi is increasing and

A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ( A is limit_ordinal iff B is limit_ordinal )

thus ( A is limit_ordinal implies B is limit_ordinal ) :: thesis: ( B is limit_ordinal implies A is limit_ordinal )

given psi being Ordinal-Sequence such that A1: dom psi = B and

A2: rng psi c= A and

A3: psi is increasing and

A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ( A is limit_ordinal iff B is limit_ordinal )

thus ( A is limit_ordinal implies B is limit_ordinal ) :: thesis: ( B is limit_ordinal implies A is limit_ordinal )

proof

thus
( B is limit_ordinal implies A is limit_ordinal )
by A1, A3, A4, Th16; :: thesis: verum
assume A5:
A is limit_ordinal
; :: thesis: B is limit_ordinal

end;now :: thesis: for C being Ordinal st C in B holds

succ C in B

hence
B is limit_ordinal
by ORDINAL1:28; :: thesis: verumsucc C in B

let C be Ordinal; :: thesis: ( C in B implies succ C in B )

reconsider c = psi . C as Ordinal ;

assume A6: C in B ; :: thesis: succ C in B

then psi . C in rng psi by A1, FUNCT_1:def 3;

then succ c in A by A2, A5, ORDINAL1:28;

then consider b being Ordinal such that

A7: b in rng psi and

A8: succ c c= b by A4, ORDINAL2:21;

consider e being object such that

A9: e in B and

A10: b = psi . e by A1, A7, FUNCT_1:def 3;

reconsider e = e as Ordinal by A9;

c in succ c by ORDINAL1:6;

then not e c= C by A1, A3, A6, A8, A10, Th9, ORDINAL1:5;

then C in e by ORDINAL1:16;

then succ C c= e by ORDINAL1:21;

hence succ C in B by A9, ORDINAL1:12; :: thesis: verum

end;reconsider c = psi . C as Ordinal ;

assume A6: C in B ; :: thesis: succ C in B

then psi . C in rng psi by A1, FUNCT_1:def 3;

then succ c in A by A2, A5, ORDINAL1:28;

then consider b being Ordinal such that

A7: b in rng psi and

A8: succ c c= b by A4, ORDINAL2:21;

consider e being object such that

A9: e in B and

A10: b = psi . e by A1, A7, FUNCT_1:def 3;

reconsider e = e as Ordinal by A9;

c in succ c by ORDINAL1:6;

then not e c= C by A1, A3, A6, A8, A10, Th9, ORDINAL1:5;

then C in e by ORDINAL1:16;

then succ C c= e by ORDINAL1:21;

hence succ C in B by A9, ORDINAL1:12; :: thesis: verum