let A, B, C be Ordinal; :: thesis: ( A in B *^ C & B is limit_ordinal implies ex D being Ordinal st
( D in B & A in D *^ C ) )
assume that
A1: A in B *^ C and
A2: B is limit_ordinal ; :: thesis: ex D being Ordinal st
( D in B & A in D *^ C )
deffunc H₁( Ordinal) -> set = $1 *^ C;
consider fi being Ordinal-Sequence such that
A3: ( dom fi = B & ( for D being Ordinal st D in B holds
fi . D = H₁(D) ) ) from ORDINAL2:sch 3();
B <> {} by A1, ORDINAL2:35;
then B *^ C = union (sup fi) by A2, A3, ORDINAL2:37
.= union (sup (rng fi)) ;
then consider X being set such that
A4: A in X and
A5: X in sup (rng fi) by A1, TARSKI:def 4;
reconsider X = X as Ordinal by A5;
consider D being Ordinal such that
A6: D in rng fi and
A7: X c= D by A5, ORDINAL2:21;
consider x being object such that
A8: x in dom fi and
A9: D = fi . x by A6, FUNCT_1:def 3;
reconsider x = x as Ordinal by A8;
take E = succ x; :: thesis: ( E in B & A in E *^ C )
thus E in B by A2, A3, A8, ORDINAL1:28; :: thesis: A in E *^ C
A10: D +^ {} = D by ORDINAL2:27;
A11: C <> {} by A1, ORDINAL2:38;
E *^ C = (x *^ C) +^ C by ORDINAL2:36
.= D +^ C by A3, A8, A9 ;
then D in E *^ C by A11, A10, Th8, ORDINAL2:32;
hence A in E *^ C by A4, A7, ORDINAL1:10; :: thesis: verum