let A, B be Ordinal; :: thesis: ( A is_cofinal_with succ B implies ex C being Ordinal st A = succ C )

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

A2: rng psi c= A and

A3: psi is increasing and

A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ex C being Ordinal st A = succ C

reconsider C = psi . B as Ordinal ;

take C ; :: thesis: A = succ C

thus A c= succ C :: according to XBOOLE_0:def 10 :: thesis: succ C c= A

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

hence succ C c= A by A2, ORDINAL1:21; :: thesis: verum

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

A2: rng psi c= A and

A3: psi is increasing and

A4: A = sup psi ; :: according to ORDINAL2:def 17 :: thesis: ex C being Ordinal st A = succ C

reconsider C = psi . B as Ordinal ;

take C ; :: thesis: A = succ C

thus A c= succ C :: according to XBOOLE_0:def 10 :: thesis: succ C c= A

proof

B in succ B
by ORDINAL1:6;
let a be Ordinal; :: according to ORDINAL1:def 5 :: thesis: ( not a in A or a in succ C )

assume a in A ; :: thesis: a in succ C

then consider b being Ordinal such that

A5: b in rng psi and

A6: a c= b by A4, ORDINAL2:21;

consider e being object such that

A7: e in succ B and

A8: b = psi . e by A1, A5, FUNCT_1:def 3;

reconsider e = e as Ordinal by A7;

e c= B by A7, ORDINAL1:22;

then b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9;

then b in succ C by ORDINAL1:22;

hence a in succ C by A6, ORDINAL1:12; :: thesis: verum

end;assume a in A ; :: thesis: a in succ C

then consider b being Ordinal such that

A5: b in rng psi and

A6: a c= b by A4, ORDINAL2:21;

consider e being object such that

A7: e in succ B and

A8: b = psi . e by A1, A5, FUNCT_1:def 3;

reconsider e = e as Ordinal by A7;

e c= B by A7, ORDINAL1:22;

then b c= C by A1, A3, A8, ORDINAL1:6, ORDINAL4:9;

then b in succ C by ORDINAL1:22;

hence a in succ C by A6, ORDINAL1:12; :: thesis: verum

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

hence succ C c= A by A2, ORDINAL1:21; :: thesis: verum