let A, B be Ordinal; ( 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
; ORDINAL2:def 17 ( A is limit_ordinal iff B is limit_ordinal )
thus
( A is limit_ordinal implies B is limit_ordinal )
( B is limit_ordinal implies A is limit_ordinal )proof
assume A5:
A is
limit_ordinal
;
B is limit_ordinal
now for C being Ordinal st C in B holds
succ C in Blet C be
Ordinal;
( C in B implies succ C in B )reconsider c =
psi . C as
Ordinal ;
assume A6:
C in B
;
succ C in Bthen
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;
verum end;
hence
B is
limit_ordinal
by ORDINAL1:28;
verum
end;
thus
( B is limit_ordinal implies A is limit_ordinal )
by A1, A3, A4, Th16; verum