let A, B, C be Ordinal; ( C <> 0 & A in B implies A *^ C in B *^ C )
A1:
0 c= C
;
defpred S1[ Ordinal] means ( A in $1 implies A *^ C in $1 *^ C );
assume
C <> 0
; ( not A in B or A *^ C in B *^ C )
then A2:
0 c< C
by A1;
then A3:
0 in C
by ORDINAL1:11;
A4:
for B being Ordinal st ( for D being Ordinal st D in B holds
S1[D] ) holds
S1[B]
proof
let B be
Ordinal;
( ( for D being Ordinal st D in B holds
S1[D] ) implies S1[B] )
assume that A5:
for
D being
Ordinal st
D in B &
A in D holds
A *^ C in D *^ C
and A6:
A in B
;
A *^ C in B *^ C
now ( ( for D being Ordinal holds B <> succ D ) implies A *^ C in B *^ C )A14:
(
(A *^ C) +^ 0 = A *^ C &
(A *^ C) +^ 0 in (A *^ C) +^ C )
by A2, Th27, Th32, ORDINAL1:11;
A15:
(succ A) *^ C = (A *^ C) +^ C
by Th36;
deffunc H1(
Ordinal)
-> Ordinal = $1
*^ C;
consider fi being
Ordinal-Sequence such that A16:
(
dom fi = B & ( for
D being
Ordinal st
D in B holds
fi . D = H1(
D) ) )
from ORDINAL2:sch 3();
assume
for
D being
Ordinal holds
B <> succ D
;
A *^ C in B *^ Cthen A17:
B is
limit_ordinal
by ORDINAL1:29;
then A18:
succ A in B
by A6, ORDINAL1:28;
then
fi . (succ A) = (succ A) *^ C
by A16;
then
(succ A) *^ C in rng fi
by A16, A18, FUNCT_1:def 3;
then A19:
(succ A) *^ C c= union (sup (rng fi))
by Th19, ZFMISC_1:74;
B *^ C =
union (sup fi)
by A6, A17, A16, Th37
.=
union (sup (rng fi))
;
hence
A *^ C in B *^ C
by A19, A14, A15;
verum end;
hence
A *^ C in B *^ C
by A7;
verum
end;
for B being Ordinal holds S1[B]
from ORDINAL1:sch 2(A4);
hence
( not A in B or A *^ C in B *^ C )
; verum