let fi be Ordinal-Sequence; :: thesis: ( dom fi <> {} & dom fi is limit_ordinal & fi is increasing implies ( sup fi is_limes_of fi & lim fi = sup fi ) )
assume that
A1: ( dom fi <> {} & dom fi is limit_ordinal ) and
A2: for A, B being Ordinal st A in B & B in dom fi holds
fi . A in fi . B ; :: according to ORDINAL2:def 12 :: thesis: ( sup fi is_limes_of fi & lim fi = sup fi )
reconsider x = fi . {} as Ordinal ;
{} in dom fi by A1, ORDINAL3:8;
then A3: x in rng fi by FUNCT_1:def 3;
thus sup fi is_limes_of fi :: thesis: lim fi = sup fi
proof
per cases ( sup fi = 0 or sup fi <> 0 ) ;
:: according to ORDINAL2:def 9
case sup fi = 0 ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = 0 ) ) )
hence ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or fi . b2 = 0 ) ) ) by A3, ORDINAL2:19; :: thesis: verum
end;
case sup fi <> 0 ; :: thesis: for b1, b2 being set holds
( not b1 in sup fi or not sup fi in b2 or ex b3 being set st
( b3 in dom fi & ( for b4 being set holds
( not b3 c= b4 or not b4 in dom fi or ( b1 in fi . b4 & fi . b4 in b2 ) ) ) ) )
let A, B be Ordinal; :: thesis: ( not A in sup fi or not sup fi in B or ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A in fi . b2 & fi . b2 in B ) ) ) ) )
assume that
A4: A in sup fi and
A5: sup fi in B ; :: thesis: ex b1 being set st
( b1 in dom fi & ( for b2 being set holds
( not b1 c= b2 or not b2 in dom fi or ( A in fi . b2 & fi . b2 in B ) ) ) )
consider C being Ordinal such that
A6: C in rng fi and
A7: A c= C by A4, ORDINAL2:21;
consider x being object such that
A8: x in dom fi and
A9: C = fi . x by A6, FUNCT_1:def 3;
reconsider x = x as Ordinal by A8;
take M = succ x; :: thesis: ( M in dom fi & ( for b1 being set holds
( not M c= b1 or not b1 in dom fi or ( A in fi . b1 & fi . b1 in B ) ) ) )
thus M in dom fi by A1, A8, ORDINAL1:28; :: thesis: for b1 being set holds
( not M c= b1 or not b1 in dom fi or ( A in fi . b1 & fi . b1 in B ) )
let D be Ordinal; :: thesis: ( not M c= D or not D in dom fi or ( A in fi . D & fi . D in B ) )
assume that
A10: M c= D and
A11: D in dom fi ; :: thesis: ( A in fi . D & fi . D in B )
reconsider E = fi . D as Ordinal ;
x in M by ORDINAL1:6;
then C in E by A2, A9, A10, A11;
hence A in fi . D by A7, ORDINAL1:12; :: thesis: fi . D in B
fi . D in rng fi by A11, FUNCT_1:def 3;
then E in sup fi by ORDINAL2:19;
hence fi . D in B by A5, ORDINAL1:10; :: thesis: verum
end;
end;
end;
hence lim fi = sup fi by ORDINAL2:def 10; :: thesis: verum