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