let A be Ordinal; :: thesis: ( A is limit_ordinal iff for C being Ordinal st C in A holds
succ C in A )
thus ( A is limit_ordinal implies for C being Ordinal st C in A holds
succ C in A ) :: thesis: ( ( for C being Ordinal st C in A holds
succ C in A ) implies A is limit_ordinal )
proof
assume A is limit_ordinal ; :: thesis: for C being Ordinal st C in A holds
succ C in A
then A1: A = union A ;
let C be Ordinal; :: thesis: ( C in A implies succ C in A )
assume C in A ; :: thesis: succ C in A
then consider z being set such that
A2: C in z and
A3: z in A by A1, TARSKI:def 4;
for b being object st b in {C} holds
b in z by A2, TARSKI:def 1;
then A4: {C} c= z ;
A5: z is Ordinal by A3, Th9;
then C c= z by A2, Def2;
then succ C c= z by A4, XBOOLE_1:8;
then ( succ C = z or succ C c< z ) ;
then A6: ( succ C = z or succ C in z ) by A5, Th7;
z c= A by A3, Def2;
hence succ C in A by A3, A6; :: thesis: verum
end;
assume A7: for C being Ordinal st C in A holds
succ C in A ; :: thesis: A is limit_ordinal
now :: thesis: for a being object st a in A holds
a in union A
let a be object ; :: thesis: ( a in A implies a in union A )
reconsider aa = a as set by TARSKI:1;
assume A8: a in A ; :: thesis: a in union A
then a is Ordinal by Th9;
then A9: succ aa in A by A7, A8;
a in succ aa by Th2;
hence a in union A by A9, TARSKI:def 4; :: thesis: verum
end;
then A10: A c= union A ;
now :: thesis: for a being object st a in union A holds
a in A
let a be object ; :: thesis: ( a in union A implies a in A )
assume a in union A ; :: thesis: a in A
then consider z being set such that
A11: a in z and
A12: z in A by TARSKI:def 4;
z c= A by A12, Def2;
hence a in A by A11; :: thesis: verum
end;
then union A c= A ;
then A = union A by A10;
hence A is limit_ordinal ; :: thesis: verum