let W be Universe; for b being Ordinal of W
for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
let b be Ordinal of W; for phi being Ordinal-Sequence of W st omega in W & phi is increasing & phi is continuous holds
ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
let phi be Ordinal-Sequence of W; ( omega in W & phi is increasing & phi is continuous implies ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega ) )
assume that
A1:
omega in W
and
A2:
phi is increasing
and
A3:
phi is continuous
; ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
A4:
omega in On W
by A1, ORDINAL1:def 9;
deffunc H1( Ordinal, set ) -> Element of W = 0-element_of W;
deffunc H2( Ordinal, Ordinal of W) -> Element of W = succ (phi . $2);
consider nu being Ordinal-Sequence of W such that
A5:
nu . (0-element_of W) = b
and
A6:
for a being Ordinal of W holds nu . (succ a) = H2(a,nu . a)
and
for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
nu . a = H1(a,nu | a)
from ZF_REFLE:sch 3();
set xi = nu | omega;
set a = sup (nu | omega);
A7:
On W c= W
by ORDINAL2:7;
dom nu = On W
by FUNCT_2:def 1;
then A8:
omega c= dom nu
by A4;
then A9:
dom (nu | omega) = omega
by RELAT_1:62;
( rng (nu | omega) c= rng nu & rng nu c= On W )
by RELAT_1:def 19;
then
rng (nu | omega) c= On W
;
then
rng (nu | omega) c= W
by A7;
then reconsider a = sup (nu | omega) as Ordinal of W by A1, A9, Th11, ZF_REFLE:19;
A10:
a in dom phi
by ORDINAL4:34;
then A11:
a c= dom phi
by ORDINAL1:def 2;
then A12:
dom (phi | a) = a
by RELAT_1:62;
A13:
nu | omega is increasing
proof
let A be
Ordinal;
ORDINAL2:def 12 for b1 being set holds
( not A in b1 or not b1 in dom (nu | omega) or (nu | omega) . A in (nu | omega) . b1 )let B be
Ordinal;
( not A in B or not B in dom (nu | omega) or (nu | omega) . A in (nu | omega) . B )
assume that A14:
A in B
and A15:
B in dom (nu | omega)
;
(nu | omega) . A in (nu | omega) . B
defpred S2[
Ordinal]
means (
A +^ $1
in dom (nu | omega) & $1
<> {} implies
(nu | omega) . A in (nu | omega) . (A +^ $1) );
A16:
for
B being
Ordinal st
B <> 0 &
B is
limit_ordinal & ( for
C being
Ordinal st
C in B holds
S2[
C] ) holds
S2[
B]
A20:
for
C being
Ordinal st
S2[
C] holds
S2[
succ C]
proof
let C be
Ordinal;
( S2[C] implies S2[ succ C] )
assume that A21:
(
A +^ C in dom (nu | omega) &
C <> {} implies
(nu | omega) . A in (nu | omega) . (A +^ C) )
and A22:
A +^ (succ C) in dom (nu | omega)
and
succ C <> {}
;
(nu | omega) . A in (nu | omega) . (A +^ (succ C))
A23:
A +^ (succ C) in On W
by A4, A9, A22, ORDINAL1:10;
then reconsider asc =
A +^ (succ C) as
Ordinal of
W by ZF_REFLE:7;
A24:
A +^ C in asc
by ORDINAL1:6, ORDINAL2:32;
then
A +^ C in On W
by A23, ORDINAL1:10;
then reconsider ac =
A +^ C as
Ordinal of
W by ZF_REFLE:7;
A29:
(
succ ac = asc &
nu . ac in dom phi )
by ORDINAL2:28, ORDINAL4:34;
A +^ C in dom (nu | omega)
by A22, A24, ORDINAL1:10;
then
( (
(nu | omega) . A in (nu | omega) . ac &
nu . asc = succ (phi . (nu . ac)) &
nu . ac = (nu | omega) . ac &
phi . (nu . ac) in succ (phi . (nu . ac)) &
nu . ac c= phi . (nu . ac) ) or
C = {} )
by A2, A6, A21, A29, FUNCT_1:47, ORDINAL1:6, ORDINAL4:10;
then
( (
(nu | omega) . A in nu . ac &
nu . ac in nu . asc &
nu . asc = (nu | omega) . asc ) or
C = {} )
by A22, FUNCT_1:47, ORDINAL1:12;
then
( (
(nu | omega) . A in nu . ac &
nu . ac c= (nu | omega) . asc ) or
C = {} )
by ORDINAL1:def 2;
hence
(nu | omega) . A in (nu | omega) . (A +^ (succ C))
by A25;
verum
end;
A30:
S2[
0 ]
;
A31:
for
C being
Ordinal holds
S2[
C]
from ORDINAL2:sch 1(A30, A20, A16);
ex
C being
Ordinal st
(
B = A +^ C &
C <> {} )
by A14, ORDINAL3:28;
hence
(nu | omega) . A in (nu | omega) . B
by A15, A31;
verum
end;
then A32:
a is limit_ordinal
by A9, Lm2, ORDINAL4:16;
take
a
; ( b in a & phi . a = a & a is_cofinal_with omega )
0-element_of W in dom nu
by ORDINAL4:34;
then A33:
b in rng (nu | omega)
by A5, Lm1, FUNCT_1:50;
hence
b in a
by ORDINAL2:19; ( phi . a = a & a is_cofinal_with omega )
A34:
a <> {}
by A33, ORDINAL2:19;
a in dom phi
by ORDINAL4:34;
then A35:
phi . a is_limes_of phi | a
by A3, A32, A34;
phi | a is increasing
by A2, ORDINAL4:15;
then
sup (phi | a) = lim (phi | a)
by A32, A34, A12, ORDINAL4:8;
then A36:
phi . a = sup (rng (phi | a))
by A35, ORDINAL2:def 10;
thus
phi . a c= a
XBOOLE_0:def 10 ( a c= phi . a & a is_cofinal_with omega )proof
let A be
Ordinal;
ORDINAL1:def 5 ( not A in phi . a or A in a )
assume
A in phi . a
;
A in a
then consider B being
Ordinal such that A37:
B in rng (phi | a)
and A38:
A c= B
by A36, ORDINAL2:21;
consider e being
object such that A39:
e in a
and A40:
B = (phi | a) . e
by A12, A37, FUNCT_1:def 3;
reconsider e =
e as
Ordinal by A39;
consider C being
Ordinal such that A41:
C in rng (nu | omega)
and A42:
e c= C
by A39, ORDINAL2:21;
A43:
(
e c< C iff (
e c= C &
e <> C ) )
;
consider u being
object such that A44:
u in omega
and A45:
C = (nu | omega) . u
by A9, A41, FUNCT_1:def 3;
reconsider u =
u as
Ordinal by A44;
u c= omega
by A44, ORDINAL1:def 2;
then reconsider u =
u as
Ordinal of
W by A1, CLASSES1:def 1;
A46:
succ u in dom nu
by ORDINAL4:34;
C in a
by A41, ORDINAL2:19;
then
(
e = C or (
e in C &
C in dom phi ) )
by A11, A42, A43, ORDINAL1:11;
then A47:
(
phi . e = phi . C or
phi . e in phi . C )
by A2;
A48:
nu . (succ u) = succ (phi . (nu . u))
by A6;
succ u in omega
by A44, Lm2, ORDINAL1:28;
then
nu . (succ u) in rng (nu | omega)
by A46, FUNCT_1:50;
then A49:
nu . (succ u) in a
by ORDINAL2:19;
C = nu . u
by A9, A44, A45, FUNCT_1:47;
then A50:
phi . e c= phi . (nu . u)
by A47, ORDINAL1:def 2;
phi . e = B
by A12, A39, A40, FUNCT_1:47;
then
B in nu . (succ u)
by A48, A50, ORDINAL1:6, ORDINAL1:12;
then
B in a
by A49, ORDINAL1:10;
hence
A in a
by A38, ORDINAL1:12;
verum
end;
thus
a c= phi . a
by A2, A10, ORDINAL4:10; a is_cofinal_with omega
take
nu | omega
; ORDINAL2:def 17 ( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) )
rng (nu | omega) c= a
hence
( dom (nu | omega) = omega & rng (nu | omega) c= a & nu | omega is increasing & a = sup (nu | omega) )
by A8, A13, RELAT_1:62; verum