assume A5:
for a being Ordinal of F1() holds
( not F2() in a or not F3(a) = a )
; contradiction
deffunc H1( Ordinal, Ordinal) -> Ordinal = F3($2);
deffunc H2( Ordinal, Sequence) -> set = {} ;
consider phi being Ordinal-Sequence such that
A6:
dom phi = omega
and
A7:
( 0 in omega implies phi . 0 = succ F2() )
and
A8:
for a being Ordinal st succ a in omega holds
phi . (succ a) = H1(a,phi . a)
and
for a being Ordinal st a in omega & a <> 0 & a is limit_ordinal holds
phi . a = H2(a,phi | a)
from ORDINAL2:sch 11();
A9:
rng phi c= On F1()
then reconsider phi = phi as Ordinal-Sequence of omega,F1() by A6, FUNCT_2:2;
A20:
for a being Ordinal st a in omega holds
F2() in phi . a
A24:
phi is increasing
proof
let a be
Ordinal;
ORDINAL2:def 12 for b1 being set holds
( not a in b1 or not b1 in dom phi or phi . a in phi . b1 )let b be
Ordinal;
( not a in b or not b in dom phi or phi . a in phi . b )
assume A25:
(
a in b &
b in dom phi )
;
phi . a in phi . b
then A26:
ex
c being
Ordinal st
(
b = a +^ c &
c <> {} )
by ORDINAL3:28;
defpred S1[
Ordinal]
means (
a +^ $1
in omega & $1
<> {} implies
phi . a in phi . (a +^ $1) );
A27:
S1[
0 ]
;
A28:
for
c being
Ordinal st
S1[
c] holds
S1[
succ c]
proof
let c be
Ordinal;
( S1[c] implies S1[ succ c] )
assume that A29:
(
a +^ c in omega &
c <> {} implies
phi . a in phi . (a +^ c) )
and A30:
(
a +^ (succ c) in omega &
succ c <> {} )
;
phi . a in phi . (a +^ (succ c))
A31:
(
a +^ c in succ (a +^ c) &
a +^ (succ c) = succ (a +^ c) )
by ORDINAL1:6, ORDINAL2:28;
reconsider d =
phi . (a +^ c) as
Ordinal ;
a +^ c in omega
by A30, A31, ORDINAL1:10;
then
(
phi . (a +^ (succ c)) = F3(
d) &
d in F3(
d) &
a +^ {} = a )
by A8, A19, A30, A31, A20, ORDINAL2:27;
hence
phi . a in phi . (a +^ (succ c))
by A29, A30, A31, ORDINAL1:10;
verum
end;
A32:
for
b being
Ordinal st
b <> 0 &
b is
limit_ordinal & ( for
c being
Ordinal st
c in b holds
S1[
c] ) holds
S1[
b]
for
c being
Ordinal holds
S1[
c]
from ORDINAL2:sch 1(A27, A28, A32);
hence
phi . a in phi . b
by A6, A25, A26;
verum
end;
A35:
sup phi in F1()
by A1, Th42;
deffunc H3( Ordinal) -> Ordinal = F3($1);
consider fi being Ordinal-Sequence such that
A36:
( dom fi = sup phi & ( for a being Ordinal st a in sup phi holds
fi . a = H3(a) ) )
from ORDINAL2:sch 3();
( succ F2() in rng phi & sup (rng phi) = sup phi )
by A6, A7, FUNCT_1:def 3;
then A37:
( sup phi <> {} & sup phi is limit_ordinal )
by A6, A24, ORDINAL2:19, ORDINAL4:16;
then A38:
H3( sup phi) is_limes_of fi
by A35, A4, A36;
fi is increasing
then A40: sup fi =
lim fi
by A36, A37, ORDINAL4:8
.=
H3( sup phi)
by A38, ORDINAL2:def 10
;
A41:
sup fi c= sup phi
proof
let x be
Ordinal;
ORDINAL1:def 5 ( not x in sup fi or x in sup phi )
assume A42:
x in sup fi
;
x in sup phi
reconsider A =
x as
Ordinal ;
consider b being
Ordinal such that A43:
(
b in rng fi &
A c= b )
by A42, ORDINAL2:21;
consider y being
object such that A44:
(
y in dom fi &
b = fi . y )
by A43, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A44;
consider c being
Ordinal such that A45:
(
c in rng phi &
y c= c )
by A36, A44, ORDINAL2:21;
A46:
c in F1()
by A9, A45, ORDINAL1:def 9;
consider z being
object such that A47:
(
z in dom phi &
c = phi . z )
by A45, FUNCT_1:def 3;
reconsider z =
z as
Ordinal by A47;
succ z in omega
by A6, A47, ORDINAL1:28;
then A48:
(
phi . (succ z) = H3(
c) &
phi . (succ z) in rng phi &
b = H3(
y) )
by A6, A8, A36, A44, A47, FUNCT_1:def 3;
(
y c< c iff (
y <> c &
y c= c ) )
;
then
(
H3(
y)
in H3(
c) or
y = c )
by A46, A3, A45, ORDINAL1:11;
then
(
b c= H3(
c) &
H3(
c)
in sup phi )
by A48, ORDINAL1:def 2, ORDINAL2:19;
then
b in sup phi
by ORDINAL1:12;
hence
x in sup phi
by A43, ORDINAL1:12;
verum
end;
phi . 0 in rng phi
by A6, FUNCT_1:def 3;
then
( F2() in phi . 0 & phi . 0 in sup phi )
by A20, ORDINAL2:19;
then
F2() in sup phi
by ORDINAL1:10;
hence
contradiction
by A35, A19, A40, A41, ORDINAL1:5; verum