let fi be Ordinal-Sequence; :: thesis: for A being Ordinal
for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
let A be Ordinal; :: thesis: for f1, f2 being Ordinal-Sequence st f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 holds
A is_limes_of fi
let f1, f2 be Ordinal-Sequence; :: thesis: ( f1 is increasing & A is_limes_of f2 & sup (rng f1) = dom f2 & fi = f2 * f1 implies A is_limes_of fi )
assume that
A1: f1 is increasing and
A2: ( ( A = {} & ex B being Ordinal st
( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) ) or ( A <> {} & ( for B, C being Ordinal st B in A & A in C holds
ex D being Ordinal st
( D in dom f2 & ( for E being Ordinal st D c= E & E in dom f2 holds
( B in f2 . E & f2 . E in C ) ) ) ) ) ) and
A3: ( sup (rng f1) = dom f2 & fi = f2 * f1 ) ; :: according to ORDINAL2:def 13 :: thesis: A is_limes_of fi
per cases ( A = {} or A <> {} ) ;
:: according to ORDINAL2:def 13
case A = {} ; :: 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 = {} ) ) )
then consider B being Ordinal such that
A4: ( B in dom f2 & ( for C being Ordinal st B c= C & C in dom f2 holds
f2 . C = {} ) ) by A2;
consider B1 being Ordinal such that
A5: ( B1 in rng f1 & B c= B1 ) by A3, A4, ORDINAL2:29;
consider x being set such that
A6: ( x in dom f1 & B1 = f1 . x ) by A5, FUNCT_1:def 5;
reconsider x = x as Ordinal by A6;
take x ; :: thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = {} ) ) )
B1 in dom f2 by A3, A5, ORDINAL2:27;
hence x in dom fi by A3, A6, FUNCT_1:21; :: thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or fi . b1 = {} )
let C be Ordinal; :: thesis: ( not x c= C or not C in dom fi or fi . C = {} )
assume A7: ( x c= C & C in dom fi ) ; :: thesis: fi . C = {}
A8: dom fi c= dom f1 by A3, RELAT_1:44;
reconsider C1 = f1 . C as Ordinal ;
B1 c= C1 by A1, A6, A7, A8, Th9;
then A9: B c= C1 by A5, XBOOLE_1:1;
C1 in rng f1 by A7, A8, FUNCT_1:def 5;
then f2 . C1 = {} by A3, A4, A9, ORDINAL2:27;
hence fi . C = {} by A3, A7, FUNCT_1:22; :: thesis: verum
end;
case A <> {} ; :: thesis: for b1, b2 being set holds
( not b1 in A or not A 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 B, C be Ordinal; :: thesis: ( not B in A or not A in C 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 ( B in fi . b2 & fi . b2 in C ) ) ) ) )
assume ( B in A & A in C ) ; :: 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 ( B in fi . b2 & fi . b2 in C ) ) ) )
then consider D being Ordinal such that
A10: ( D in dom f2 & ( for A1 being Ordinal st D c= A1 & A1 in dom f2 holds
( B in f2 . A1 & f2 . A1 in C ) ) ) by A2;
consider B1 being Ordinal such that
A11: ( B1 in rng f1 & D c= B1 ) by A3, A10, ORDINAL2:29;
consider x being set such that
A12: ( x in dom f1 & B1 = f1 . x ) by A11, FUNCT_1:def 5;
reconsider x = x as Ordinal by A12;
take x ; :: thesis: ( x in dom fi & ( for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) ) ) )
B1 in dom f2 by A3, A11, ORDINAL2:27;
hence x in dom fi by A3, A12, FUNCT_1:21; :: thesis: for b1 being set holds
( not x c= b1 or not b1 in dom fi or ( B in fi . b1 & fi . b1 in C ) )
let E be Ordinal; :: thesis: ( not x c= E or not E in dom fi or ( B in fi . E & fi . E in C ) )
assume A13: ( x c= E & E in dom fi ) ; :: thesis: ( B in fi . E & fi . E in C )
A14: dom fi c= dom f1 by A3, RELAT_1:44;
reconsider E1 = f1 . E as Ordinal ;
B1 c= E1 by A1, A12, A13, A14, Th9;
then A15: D c= E1 by A11, XBOOLE_1:1;
E1 in rng f1 by A13, A14, FUNCT_1:def 5;
then E1 in dom f2 by A3, ORDINAL2:27;
then ( B in f2 . E1 & f2 . E1 in C ) by A10, A15;
hence ( B in fi . E & fi . E in C ) by A3, A13, FUNCT_1:22; :: thesis: verum
end;
end;