let A, B be Ordinal; ( A is limit_ordinal implies A *^ B is limit_ordinal )
A1:
now ( A <> {} & A is limit_ordinal & A is limit_ordinal implies A *^ B is limit_ordinal )deffunc H1(
Ordinal)
-> set = $1
*^ B;
assume that A2:
A <> {}
and A3:
A is
limit_ordinal
;
( A is limit_ordinal implies A *^ B is limit_ordinal )consider fi being
Ordinal-Sequence such that A4:
(
dom fi = A & ( for
C being
Ordinal st
C in A holds
fi . C = H1(
C) ) )
from ORDINAL2:sch 3();
A5:
A *^ B =
union (sup fi)
by A2, A3, A4, ORDINAL2:37
.=
union (sup (rng fi))
;
for
C being
Ordinal st
C in A *^ B holds
succ C in A *^ B
proof
let C be
Ordinal;
( C in A *^ B implies succ C in A *^ B )
assume A6:
C in A *^ B
;
succ C in A *^ B
then consider X being
set such that A7:
C in X
and A8:
X in sup (rng fi)
by A5, TARSKI:def 4;
reconsider X =
X as
Ordinal by A8;
consider D being
Ordinal such that A9:
D in rng fi
and A10:
X c= D
by A8, ORDINAL2:21;
consider x being
object such that A11:
x in dom fi
and A12:
D = fi . x
by A9, FUNCT_1:def 3;
succ C c= D
by A7, A10, ORDINAL1:21;
then A13:
succ C in succ D
by ORDINAL1:22;
reconsider x =
x as
Ordinal by A11;
A14:
succ x in dom fi
by A3, A4, A11, ORDINAL1:28;
then fi . (succ x) =
(succ x) *^ B
by A4
.=
(x *^ B) +^ B
by ORDINAL2:36
;
then
(x *^ B) +^ B in rng fi
by A14, FUNCT_1:def 3;
then A15:
(x *^ B) +^ B in sup (rng fi)
by ORDINAL2:19;
A16:
(x *^ B) +^ (succ {}) = succ ((x *^ B) +^ {})
by ORDINAL2:28;
B <> {}
by A6, ORDINAL2:38;
then
{} in B
by Th8;
then A17:
succ {} c= B
by ORDINAL1:21;
A18:
(x *^ B) +^ {} = x *^ B
by ORDINAL2:27;
x *^ B = fi . x
by A4, A11;
then
succ D in sup (rng fi)
by A12, A17, A16, A18, A15, ORDINAL1:12, ORDINAL2:33;
hence
succ C in A *^ B
by A5, A13, TARSKI:def 4;
verum
end; hence
(
A is
limit_ordinal implies
A *^ B is
limit_ordinal )
by ORDINAL1:28;
verum end;
assume
A is limit_ordinal
; A *^ B is limit_ordinal
hence
A *^ B is limit_ordinal
by A1, ORDINAL2:35; verum