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 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 for x being object st x in a holds
(Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . xlet x be
object ;
( 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:40;
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:8, ORDINAL1:12;
then
card x9 in dom (b -powerfunc_of a)
by Def2;
then A8:
(b -powerfunc_of a) . (card x9) in rng (b -powerfunc_of a)
by FUNCT_1:def 3;
x9,
card x9 are_equipotent
by CARD_1:def 2;
then A9:
card (Funcs (b,x9)) = card (Funcs (b,(card x9)))
by FUNCT_5:60;
(
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 x9) = exp (
(card x9),
b)
by A7, Def2;
then
card (exp ((card x9),b)) c= card (Union (b -powerfunc_of a))
by A8, CARD_1:11, ZFMISC_1:74;
then A11:
card (exp ((card x9),b)) c= Sum (b -powerfunc_of a)
by A5;
thus
(Card L) . x c= (a --> (Sum (b -powerfunc_of a))) . x
by A6, A10, A11, FUNCOP_1:7;
verum end;
( dom (a --> (Sum (b -powerfunc_of a))) = a & dom (Card L) = dom L )
by CARD_3:def 2;
then A12:
Sum (Card L) c= Sum (a --> (Sum (b -powerfunc_of a)))
by A3, A4, CARD_3:30;
a c= Sum (b -powerfunc_of a)
proof
let x be
Ordinal;
ORDINAL1:def 5 ( not x in a or x in Sum (b -powerfunc_of a) )
reconsider xx =
x as
set ;
assume A13:
x in a
;
x in Sum (b -powerfunc_of a)
reconsider x9 =
x as
Ordinal ;
set m =
card x9;
card x9 in a
by A13, CARD_1:8, ORDINAL1:12;
then A14:
nextcard (card x9) c= a
by CARD_3:90;
nextcard (card x9) <> a
by A1;
then A15:
nextcard (card x9) in a
by A14, CARD_1:3;
then
nextcard (card x9) in dom (b -powerfunc_of a)
by Def2;
then A16:
(b -powerfunc_of a) . (nextcard (card x9)) in rng (b -powerfunc_of a)
by FUNCT_1:def 3;
(b -powerfunc_of a) . (nextcard (card x9)) = exp (
(nextcard (card x9)),
b)
by A15, Def2;
then A17:
card (exp ((nextcard (card x9)),b)) c= card (Union (b -powerfunc_of a))
by A16, CARD_1:11, ZFMISC_1:74;
A18:
nextcard (card x9) c= exp (
(nextcard (card x9)),
b)
by Th19;
card xx = card (card xx)
;
then A19:
(
x9 in nextcard x9 &
nextcard (card xx) = nextcard xx )
by CARD_1:18, CARD_3:88;
(
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_3:40;
then
exp (
(nextcard (card x9)),
b)
c= Sum (b -powerfunc_of a)
by A17;
then
nextcard (card xx) c= Sum (b -powerfunc_of a)
by A18;
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 Th17;
Funcs (b,a) c= Union L
proof
let x be
object ;
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
Sequence by A22, ORDINAL1:def 7;
reconsider f =
f as
Ordinal-Sequence by A23, ORDINAL2:def 4;
rng f c= sup f
by ORDINAL2:49;
then A24:
x in Funcs (
b,
(sup f))
by A21, A22, FUNCT_2:def 2;
sup f in a
by A2, A22, A23, Th26;
then A25:
L . (sup f) in rng L
by A3, FUNCT_1:def 3;
L . (sup f) = Funcs (
b,
(sup f))
by A2, A3, A22, A23, Th26;
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:11;
card (Union L) c= Sum (Card L)
by CARD_3:39;
then
card (Funcs (b,a)) c= Sum (Card L)
by A26;
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 Th32;
Sum (a --> (Sum (b -powerfunc_of a))) = a *` (Sum (b -powerfunc_of a))
by CARD_2:65;
then
exp (a,b) c= a *` (Sum (b -powerfunc_of a))
by A27, A12;
hence
exp (a,b) = Sum (b -powerfunc_of a)
by A28, A20; verum