let C be Ordinal; for A being Ordinal st A <> {} & A is limit_ordinal holds
ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) & ex D being Ordinal st D is_limes_of fi )
defpred S1[ Ordinal] means ( $1 <> {} & $1 is limit_ordinal & ( for fi being Ordinal-Sequence st dom fi = $1 & ( for B being Ordinal st B in $1 holds
fi . B = exp (C,B) ) holds
for D being Ordinal holds not D is_limes_of fi ) );
let A be Ordinal; ( A <> {} & A is limit_ordinal implies ex fi being Ordinal-Sequence st
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) & ex D being Ordinal st D is_limes_of fi ) )
assume that
A1:
A <> {}
and
A2:
A is limit_ordinal
and
A3:
for fi being Ordinal-Sequence st dom fi = A & ( for B being Ordinal st B in A holds
fi . B = exp (C,B) ) holds
for D being Ordinal holds not D is_limes_of fi
; contradiction
deffunc H1( Ordinal) -> set = exp (C,$1);
A4:
ex A being Ordinal st S1[A]
by A1, A2, A3;
consider A being Ordinal such that
A5:
S1[A]
and
A6:
for A1 being Ordinal st S1[A1] holds
A c= A1
from ORDINAL1:sch 1(A4);
consider fi being Ordinal-Sequence such that
A7:
( dom fi = A & ( for B being Ordinal st B in A holds
fi . B = H1(B) ) )
from ORDINAL2:sch 3();
A8:
( C <> {} & C <> 1 )
by A5, A7, Lm6, Lm7;
then
{} in C
by ORDINAL3:8;
then
1 c= C
by Lm3, ORDINAL1:21;
then A9:
1 c< C
by A8;
A10:
for B2, B1 being Ordinal st B1 in B2 & B2 in A holds
exp (C,B1) in exp (C,B2)
proof
defpred S2[
Ordinal]
means for
B1 being
Ordinal st
B1 in $1 & $1
in A holds
exp (
C,
B1)
in exp (
C,$1);
A11:
for
B being
Ordinal st
S2[
B] holds
S2[
succ B]
proof
let B be
Ordinal;
( S2[B] implies S2[ succ B] )
assume A12:
for
B1 being
Ordinal st
B1 in B &
B in A holds
exp (
C,
B1)
in exp (
C,
B)
;
S2[ succ B]
let B1 be
Ordinal;
( B1 in succ B & succ B in A implies exp (C,B1) in exp (C,(succ B)) )
assume that A13:
B1 in succ B
and A14:
succ B in A
;
exp (C,B1) in exp (C,(succ B))
A15:
B1 c= B
by A13, ORDINAL1:22;
B in succ B
by ORDINAL1:6;
then A16:
B in A
by A14, ORDINAL1:10;
A17:
1
*^ (exp (C,B)) = exp (
C,
B)
by ORDINAL2:39;
A18:
exp (
C,
B)
<> {}
A20:
exp (
C,
(succ B))
= C *^ (exp (C,B))
by ORDINAL2:44;
then A21:
exp (
C,
B)
in exp (
C,
(succ B))
by A9, A18, A17, ORDINAL1:11, ORDINAL2:40;
hence
exp (
C,
B1)
in exp (
C,
(succ B))
by A9, A18, A20, A17, ORDINAL1:11, ORDINAL2:40;
verum
end;
A22:
for
B being
Ordinal st
B <> 0 &
B is
limit_ordinal & ( for
D being
Ordinal st
D in B holds
S2[
D] ) holds
S2[
B]
proof
let B be
Ordinal;
( B <> 0 & B is limit_ordinal & ( for D being Ordinal st D in B holds
S2[D] ) implies S2[B] )
assume that A23:
B <> 0
and A24:
B is
limit_ordinal
and A25:
for
D being
Ordinal st
D in B holds
S2[
D]
;
S2[B]
let B1 be
Ordinal;
( B1 in B & B in A implies exp (C,B1) in exp (C,B) )
assume that A26:
B1 in B
and A27:
B in A
;
exp (C,B1) in exp (C,B)
consider psi being
Ordinal-Sequence such that A28:
dom psi = B
and A29:
for
D being
Ordinal st
D in B holds
psi . D = exp (
C,
D)
and
ex
D being
Ordinal st
D is_limes_of psi
by A6, A24, A26, A27, ORDINAL1:5;
psi . B1 = exp (
C,
B1)
by A26, A29;
then A30:
exp (
C,
B1)
in rng psi
by A26, A28, FUNCT_1:def 3;
psi is
increasing
proof
let B1,
B2 be
Ordinal;
ORDINAL2:def 12 ( not B1 in B2 or not B2 in dom psi or psi . B1 in psi . B2 )
assume that A31:
B1 in B2
and A32:
B2 in dom psi
;
psi . B1 in psi . B2
B2 in A
by A27, A28, A32, ORDINAL1:10;
then A33:
exp (
C,
B1)
in exp (
C,
B2)
by A25, A28, A31, A32;
psi . B1 = exp (
C,
B1)
by A28, A29, A31, A32, ORDINAL1:10;
hence
psi . B1 in psi . B2
by A28, A29, A32, A33;
verum
end;
then A34:
lim psi = sup psi
by A23, A24, A28, Th8;
exp (
C,
B)
= lim psi
by A23, A24, A28, A29, ORDINAL2:45;
hence
exp (
C,
B1)
in exp (
C,
B)
by A34, A30, ORDINAL2:19;
verum
end;
A35:
S2[
0 ]
;
thus
for
B being
Ordinal holds
S2[
B]
from ORDINAL2:sch 1(A35, A11, A22); verum
end;
fi is increasing
proof
let B1,
B2 be
Ordinal;
ORDINAL2:def 12 ( not B1 in B2 or not B2 in dom fi or fi . B1 in fi . B2 )
assume that A36:
B1 in B2
and A37:
B2 in dom fi
;
fi . B1 in fi . B2
A38:
fi . B1 = exp (
C,
B1)
by A7, A36, A37, ORDINAL1:10;
exp (
C,
B1)
in exp (
C,
B2)
by A7, A10, A36, A37;
hence
fi . B1 in fi . B2
by A7, A37, A38;
verum
end;
then
sup fi is_limes_of fi
by A5, A7, Th8;
hence
contradiction
by A5, A7; verum