A7:
dom F3() = omega
by FUNCT_2:def 1;
A8:
F2() in rng F3()
by A5, A7, FUNCT_1:def 3;
hence
F2() c= Union F3()
by ZFMISC_1:74; ( F4((Union F3())) = Union F3() & ( for b being Ordinal st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )
set phi = F3();
then
F2() c= F4(F2())
;
then A13:
( F2() c< F4(F2()) or F2() = F4(F2()) )
;
per cases
( F4(F2()) = F2() or F2() in F4(F2()) )
by A13, ORDINAL1:11;
suppose A21:
F2()
in F4(
F2())
;
( F4((Union F3())) = Union F3() & ( for b being Ordinal st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )deffunc H1(
Ordinal,
Ordinal)
-> Ordinal =
F4($2);
deffunc H2(
Ordinal,
Sequence)
-> set =
{} ;
A24:
for
a being
Ordinal st
a in omega holds
(
F2()
c= F3()
. a &
F3()
. a in F3()
. (succ a) )
deffunc H3(
Ordinal)
-> Ordinal =
F4($1);
consider fi being
Ordinal-Sequence such that A29:
(
dom fi = Union F3() & ( for
a being
Ordinal st
a in Union F3() holds
fi . a = H3(
a) ) )
from ORDINAL2:sch 3();
1
= succ 0
;
then
F3()
. 1
= H3(
F2())
by A5, A6;
then
H3(
F2())
in rng F3()
by A7, FUNCT_1:def 3;
then A30:
H3(
F2())
c= Union F3()
by ZFMISC_1:74;
A31:
Union F3()
in F1()
by A1, Th41;
then A33:
Union F3() is
limit_ordinal
by ORDINAL1:28;
then A34:
H3(
Union F3())
is_limes_of fi
by A4, A21, A29, A30, A31;
fi is
increasing
then A36:
sup fi =
lim fi
by A21, A29, A30, A33, ORDINAL4:8
.=
H3(
Union F3())
by A34, ORDINAL2:def 10
;
thus
H3(
Union F3())
c= Union F3()
XBOOLE_0:def 10 ( Union F3() c= F4((Union F3())) & ( for b being Ordinal st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= b ) )proof
let x be
Ordinal;
ORDINAL1:def 5 ( not x in H3( Union F3()) or x in Union F3() )
assume A37:
x in H3(
Union F3())
;
x in Union F3()
reconsider A =
x as
Ordinal ;
consider b being
Ordinal such that A38:
(
b in rng fi &
A c= b )
by A36, A37, ORDINAL2:21;
consider y being
object such that A39:
(
y in dom fi &
b = fi . y )
by A38, FUNCT_1:def 3;
reconsider y =
y as
Ordinal by A39;
consider z being
object such that A40:
(
z in dom F3() &
y in F3()
. z )
by A29, A39, CARD_5:2;
reconsider z =
z as
Ordinal by A40;
set c =
F3()
. z;
succ z in omega
by A7, A40, ORDINAL1:28;
then A41:
(
F3()
. (succ z) = H3(
F3()
. z) &
F3()
. (succ z) in rng F3() &
b = H3(
y) )
by A7, A22, A29, A39, FUNCT_1:def 3;
(
b in H3(
F3()
. z) &
H3(
F3()
. z)
c= Union F3() )
by A41, A3, A40, ZFMISC_1:74;
hence
x in Union F3()
by A38, ORDINAL1:12;
verum
end; thus
Union F3()
c= H3(
Union F3())
by A9, A1, Th41;
for b being Ordinal st F2() c= b & b in F1() & F4(b) = b holds
Union F3() c= blet b be
Ordinal;
( F2() c= b & b in F1() & F4(b) = b implies Union F3() c= b )assume A42:
(
F2()
c= b &
b in F1() &
H3(
b)
= b )
;
Union F3() c= b
rng F3()
c= b
then
(
Union F3()
c= union b &
union b c= b )
by ORDINAL2:5, ZFMISC_1:77;
hence
Union F3()
c= b
;
verum end; end;