let a, b be Aleph; ( a is limit_cardinal & b in cf a implies exp a,b = Sum (b -powerfunc_of a) )
assume that
A1:
a is limit_cardinal
and
A2:
b in cf a
; exp a,b = Sum (b -powerfunc_of a)
deffunc H1( Ordinal) -> set = Funcs b,$1;
consider L being T-Sequence such that
A3:
( dom L = a & ( for A being Ordinal st A in a holds
L . A = H1(A) ) )
from ORDINAL2:sch 2();
A4:
now let x be
set ;
( x in a implies (Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x )A5:
card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a)
by CARD_3:55;
assume A6:
x in a
;
(Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . xthen reconsider x9 =
x as
Ordinal ;
set m =
card x9;
A7:
card x9 in a
by A6, CARD_1:24, ORDINAL1:22;
then
card x9 in dom (b -powerfunc_of a)
by Def3;
then A8:
(b -powerfunc_of a) . (card x) in rng (b -powerfunc_of a)
by FUNCT_1:def 5;
x9,
card x9 are_equipotent
by CARD_1:def 5;
then A9:
card (Funcs b,x9) = card (Funcs b,(card x9))
by FUNCT_5:67;
(
L . x = Funcs b,
x9 &
(Card L) . x = card (L . x) )
by A3, A6, CARD_3:def 2;
then A10:
(Card L) . x = exp (card x9),
b
by A9, CARD_2:def 3;
(b -powerfunc_of a) . (card x) = exp (card x),
b
by A7, Def3;
then
card (exp (card x),b) c= card (Union (b -powerfunc_of a))
by A8, CARD_1:27, ZFMISC_1:92;
then A11:
card (exp (card x),b) c= Sum (b -powerfunc_of a)
by A5, XBOOLE_1:1;
card (exp (card x),b) = exp (card x),
b
by CARD_1:def 5;
hence
(Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x
by A6, A10, A11, FUNCOP_1:13;
verum end;
( dom (a --> (Sum (b -powerfunc_of a))) = a & dom (Card L) = dom L )
by CARD_3:def 2, FUNCOP_1:19;
then A12:
Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a)))
by A3, A4, CARD_3:43;
a c= Sum (b -powerfunc_of a)
proof
let x be
set ;
TARSKI:def 3 ( not x in a or x in Sum (b -powerfunc_of a) )
assume A13:
x in a
;
x in Sum (b -powerfunc_of a)
then reconsider x9 =
x as
Ordinal ;
set m =
card x9;
card x9 in a
by A13, CARD_1:24, ORDINAL1:22;
then A14:
nextcard (card x9) c= a
by CARD_3:107;
nextcard (card x9) <> a
by A1, CARD_1:def 7;
then A15:
nextcard (card x9) in a
by A14, CARD_1:13;
then
nextcard (card x9) in dom (b -powerfunc_of a)
by Def3;
then A16:
(b -powerfunc_of a) . (nextcard (card x9)) in rng (b -powerfunc_of a)
by FUNCT_1:def 5;
(b -powerfunc_of a) . (nextcard (card x9)) = exp (nextcard (card x9)),
b
by A15, Def3;
then A17:
card (exp (nextcard (card x9)),b) c= card (Union (b -powerfunc_of a))
by A16, CARD_1:27, ZFMISC_1:92;
A18:
nextcard (card x9) c= exp (nextcard (card x9)),
b
by Th31;
card x = card (card x)
;
then A19:
(
x9 in nextcard x9 &
nextcard (card x) = nextcard x )
by CARD_1:36, CARD_3:105;
(
card (exp (nextcard (card x9)),b) = exp (nextcard (card x9)),
b &
card (Union (b -powerfunc_of a)) c= Sum (b -powerfunc_of a) )
by CARD_1:def 5, CARD_3:55;
then
exp (nextcard (card x9)),
b c= Sum (b -powerfunc_of a)
by A17, XBOOLE_1:1;
then
nextcard (card x) c= Sum (b -powerfunc_of a)
by A18, XBOOLE_1:1;
hence
x in Sum (b -powerfunc_of a)
by A19;
verum
end;
then A20:
a *` (Sum (b -powerfunc_of a)) = Sum (b -powerfunc_of a)
by Th27;
Funcs b,a c= Union L
proof
let x be
set ;
TARSKI:def 3 ( not x in Funcs b,a or x in Union L )
assume
x in Funcs b,
a
;
x in Union L
then consider f being
Function such that A21:
x = f
and A22:
dom f = b
and A23:
rng f c= a
by FUNCT_2:def 2;
reconsider f =
f as
T-Sequence by A22, ORDINAL1:def 7;
reconsider f =
f as
Ordinal-Sequence by A23, ORDINAL2:def 8;
rng f c= sup f
by ORDINAL2:67;
then A24:
x in Funcs b,
(sup f)
by A21, A22, FUNCT_2:def 2;
sup f in a
by A2, A22, A23, Th39;
then A25:
L . (sup f) in rng L
by A3, FUNCT_1:def 5;
L . (sup f) = Funcs b,
(sup f)
by A2, A3, A22, A23, Th39;
hence
x in Union L
by A24, A25, TARSKI:def 4;
verum
end;
then A26:
card (Funcs b,a) c= card (Union L)
by CARD_1:27;
card (Union L) c= Sum (Card L)
by CARD_3:54;
then
card (Funcs b,a) c= Sum (Card L)
by A26, XBOOLE_1:1;
then A27:
exp a,b c= Sum (Card L)
by CARD_2:def 3;
A28:
Sum (b -powerfunc_of a) c= exp a,b
by Th45;
Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a))
by CARD_3:52;
then
exp a,b c= a *` (Sum (b -powerfunc_of a))
by A27, A12, XBOOLE_1:1;
hence
exp a,b = Sum (b -powerfunc_of a)
by A28, A20, XBOOLE_0:def 10; verum