let A be Ordinal; ( A <> 0 & A is limit_ordinal & ( for B being Ordinal st B in A holds
S1[B] ) implies S1[A] )
deffunc H1( Ordinal) -> set = Rank $1;
assume that
A1:
A <> 0
and
A2:
A is limit_ordinal
and
A3:
for B being Ordinal st B in A holds
S1[B]
; S1[A]
let W be set ; ( W is Tarski & A in On W implies ( card (Rank A) in card W & Rank A in W ) )
assume that
A4:
W is Tarski
and
A5:
A in On W
; ( card (Rank A) in card W & Rank A in W )
consider L being Sequence such that
A6:
( dom L = A & ( for B being Ordinal st B in A holds
L . B = H1(B) ) )
from ORDINAL2:sch 2();
deffunc H2( object ) -> set = card (bool (L . $1));
consider F being Cardinal-Function such that
A7:
( dom F = A & ( for x being set st x in A holds
F . x = H2(x) ) )
from CARD_3:sch 1();
A8:
product F c= Funcs (A,W)
proof
let x be
object ;
TARSKI:def 3 ( not x in product F or x in Funcs (A,W) )
assume
x in product F
;
x in Funcs (A,W)
then consider f being
Function such that A9:
x = f
and A10:
dom f = dom F
and A11:
for
x being
object st
x in dom F holds
f . x in F . x
by CARD_3:def 5;
rng f c= W
proof
A12:
A in W
by A5, ORDINAL1:def 9;
let z be
object ;
TARSKI:def 3 ( not z in rng f or z in W )
assume
z in rng f
;
z in W
then consider y being
object such that A13:
y in dom f
and A14:
z = f . y
by FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A7, A10, A13;
A15:
f . y in F . y
by A10, A11, A13;
y c= A
by A7, A10, A13, ORDINAL1:def 2;
then
y in W
by A4, A12, CLASSES1:def 1;
then A16:
y in On W
by ORDINAL1:def 9;
L . y = Rank y
by A6, A7, A10, A13;
then
L . y in W
by A3, A4, A7, A10, A13, A16;
then
bool (L . y) in W
by A4;
then A17:
card (bool (L . y)) in W
by A4, Th11;
F . y = card (bool (L . y))
by A7, A10, A13;
then
F . y c= W
by A4, A17, Th5;
hence
z in W
by A14, A15;
verum
end;
hence
x in Funcs (
A,
W)
by A7, A9, A10, FUNCT_2:def 2;
verum
end;
A18:
Product F = card (product F)
by CARD_3:def 8;
A19:
A in W
by A5, ORDINAL1:def 9;
then
A c= W
by A4, Th5;
then
Funcs (A,W) c= W
by A4, A19, Th22;
then
product F c= W
by A8;
then A20:
Product F c= card W
by A18, CARD_1:11;
A21:
for x being object st x in dom (Card L) holds
(Card L) . x in F . x
dom (Card L) = dom L
by CARD_3:def 2;
then A24:
Sum (Card L) in Product F
by A6, A7, A21, CARD_3:41;
A25:
Rank A c= W
A28:
Rank A = Union L
by A2, A6, Th24;
hence
card (Rank A) in card W
by A24, A20, CARD_3:39, ORDINAL1:12; Rank A in W
card (Rank A) in Product F
by A28, A24, CARD_3:39, ORDINAL1:12;
hence
Rank A in W
by A4, A20, A25, CLASSES1:1; verum