let W be Universe; :: thesis: 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; :: thesis: 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; :: thesis: ( 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 A1:
( omega in W & phi is increasing & phi is continuous )
; :: thesis: ex a being Ordinal of W st
( b in a & phi . a = a & a is_cofinal_with omega )
deffunc H1( Ordinal, Ordinal of W) -> Element of W = succ (phi . $2);
deffunc H2( Ordinal, set ) -> Element of W = 0-element_of W;
consider nu being Ordinal-Sequence of W such that
A2:
nu . (0-element_of W) = b
and
A3:
for a being Ordinal of W holds nu . (succ a) = H1(a,nu . a)
and
for a being Ordinal of W st a <> 0-element_of W & a is limit_ordinal holds
nu . a = H2(a,nu | a)
from ZF_REFLE:sch 3();
set xi = nu | omega ;
set a = sup (nu | omega );
A4:
( omega in On W & dom nu = On W )
by A1, FUNCT_2:def 1, ORDINAL1:def 10;
then A5:
omega c= dom nu
;
then A6:
( dom (nu | omega ) = omega & sup (nu | omega ) = sup (rng (nu | omega )) )
by RELAT_1:91;
( rng (nu | omega ) c= rng nu & rng nu c= On W )
by RELAT_1:def 19;
then
( rng (nu | omega ) c= On W & On W c= W )
by ORDINAL2:9, XBOOLE_1:1;
then
rng (nu | omega ) c= W
by XBOOLE_1:1;
then
sup (nu | omega ) in W
by A1, A6, Th12, ZF_REFLE:28;
then reconsider a = sup (nu | omega ) as Ordinal of W ;
take
a
; :: thesis: ( b in a & phi . a = a & a is_cofinal_with omega )
( 0-element_of W = {} & 0-element_of W in dom nu )
by ORDINAL4:36;
then A7:
b in rng (nu | omega )
by A2, Lm1, FUNCT_1:73;
hence
b in a
by ORDINAL2:27; :: thesis: ( phi . a = a & a is_cofinal_with omega )
A8:
rng (nu | omega ) c= a
A11:
nu | omega is increasing
proof
let A be
Ordinal;
:: according to ORDINAL2:def 16 :: thesis: for b1 being set holds
( not A in b1 or not b1 in proj1 (nu | omega ) or (nu | omega ) . A in (nu | omega ) . b1 )let B be
Ordinal;
:: thesis: ( not A in B or not B in proj1 (nu | omega ) or (nu | omega ) . A in (nu | omega ) . B )
assume A12:
(
A in B &
B in dom (nu | omega ) )
;
:: thesis: (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) );
A13:
S2[
{} ]
;
A14:
for
C being
Ordinal st
S2[
C] holds
S2[
succ C]
proof
let C be
Ordinal;
:: thesis: ( S2[C] implies S2[ succ C] )
assume that A15:
(
A +^ C in dom (nu | omega ) &
C <> {} implies
(nu | omega ) . A in (nu | omega ) . (A +^ C) )
and A16:
(
A +^ (succ C) in dom (nu | omega ) &
succ C <> {} )
;
:: thesis: (nu | omega ) . A in (nu | omega ) . (A +^ (succ C))
A17:
A +^ (succ C) in On W
by A4, A6, A16, ORDINAL1:19;
then reconsider asc =
A +^ (succ C) as
Ordinal of
W by ZF_REFLE:8;
A +^ C in asc
by ORDINAL1:10, ORDINAL2:49;
then A18:
(
A +^ C in On W &
A +^ C in dom (nu | omega ) )
by A16, A17, ORDINAL1:19;
then reconsider ac =
A +^ C as
Ordinal of
W by ZF_REFLE:8;
(
succ ac = asc &
nu . ac in dom phi & (
C = {} or
C <> {} ) )
by ORDINAL2:45, ORDINAL4:36;
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 A1, A3, A15, A18, FUNCT_1:70, ORDINAL1:10, ORDINAL4:10;
then
( (
(nu | omega ) . A in nu . ac &
nu . ac in nu . asc &
nu . asc = (nu | omega ) . asc ) or
C = {} )
by A16, FUNCT_1:70, ORDINAL1:22;
then A19:
( (
(nu | omega ) . A in nu . ac &
nu . ac c= (nu | omega ) . asc ) or
C = {} )
by ORDINAL1:def 2;
now assume
C = {}
;
:: thesis: (nu | omega ) . A in (nu | omega ) . (A +^ (succ C))then A20:
(
ac = A &
asc = succ ac &
A in succ A &
nu . ac in dom phi )
by ORDINAL1:10, ORDINAL2:44, ORDINAL2:45, ORDINAL4:36;
then
(
nu . asc = succ (phi . (nu . ac)) &
nu . ac c= phi . (nu . ac) &
phi . (nu . ac) in succ (phi . (nu . ac)) &
(nu | omega ) . ac = nu . ac &
(nu | omega ) . asc = nu . asc )
by A1, A3, A16, A18, FUNCT_1:70, ORDINAL1:10, ORDINAL4:10;
hence
(nu | omega ) . A in (nu | omega ) . (A +^ (succ C))
by A20, ORDINAL1:22;
:: thesis: verum end;
hence
(nu | omega ) . A in (nu | omega ) . (A +^ (succ C))
by A19;
:: thesis: verum
end;
A21:
for
B being
Ordinal st
B <> {} &
B is
limit_ordinal & ( for
C being
Ordinal st
C in B holds
S2[
C] ) holds
S2[
B]
A23:
for
C being
Ordinal holds
S2[
C]
from ORDINAL2:sch 1(A13, A14, A21);
ex
C being
Ordinal st
(
B = A +^ C &
C <> {} )
by A12, ORDINAL3:31;
hence
(nu | omega ) . A in (nu | omega ) . B
by A12, A23;
:: thesis: verum
end;
A24:
a in dom phi
by ORDINAL4:36;
then A25:
a c= dom phi
by ORDINAL1:def 2;
then A26:
( a is limit_ordinal & a <> {} & phi | a is increasing & dom (phi | a) = a & a in dom phi )
by A1, A6, A7, A11, Lm2, ORDINAL2:27, ORDINAL4:15, ORDINAL4:16, ORDINAL4:36, RELAT_1:91;
then
( phi . a is_limes_of phi | a & sup (phi | a) = lim (phi | a) & sup (phi | a) = sup (rng (phi | a)) )
by A1, ORDINAL2:def 17, ORDINAL4:8;
then A27:
phi . a = sup (rng (phi | a))
by ORDINAL2:def 14;
thus
phi . a c= a
:: according to XBOOLE_0:def 10 :: thesis: ( a c= phi . a & a is_cofinal_with omega )proof
let A be
Ordinal;
:: according to ORDINAL1:def 5 :: thesis: ( not A in phi . a or A in a )
assume
A in phi . a
;
:: thesis: A in a
then consider B being
Ordinal such that A28:
(
B in rng (phi | a) &
A c= B )
by A27, ORDINAL2:29;
consider e being
set such that A29:
(
e in a &
B = (phi | a) . e )
by A26, A28, FUNCT_1:def 5;
reconsider e =
e as
Ordinal by A29;
consider C being
Ordinal such that A30:
(
C in rng (nu | omega ) &
e c= C )
by A29, ORDINAL2:29;
consider u being
set such that A31:
(
u in omega &
C = (nu | omega ) . u )
by A6, A30, FUNCT_1:def 5;
reconsider u =
u as
Ordinal by A31;
u c= omega
by A31, ORDINAL1:def 2;
then
u in W
by A1, CLASSES1:def 1;
then reconsider u =
u as
Ordinal of
W ;
A32:
C in a
by A30, ORDINAL2:27;
(
e c< C iff (
e c= C &
e <> C ) )
by XBOOLE_0:def 8;
then
(
e = C or (
e in C &
C in dom phi ) )
by A25, A30, A32, ORDINAL1:21;
then A33:
(
phi . e = phi . C or
phi . e in phi . C )
by A1, ORDINAL2:def 16;
(
succ u in omega &
succ u in dom nu )
by A31, Lm2, ORDINAL1:41, ORDINAL4:36;
then A34:
(
(nu | omega ) . (succ u) = nu . (succ u) &
C = nu . u &
nu . u in dom phi &
nu . (succ u) in rng (nu | omega ) &
phi . e = B )
by A6, A26, A29, A31, FUNCT_1:70, FUNCT_1:73, ORDINAL4:36;
then
(
nu . (succ u) = succ (phi . (nu . u)) &
phi . e c= phi . (nu . u) &
phi . C in succ (phi . (nu . u)) )
by A3, A33, ORDINAL1:10, ORDINAL1:def 2;
then
(
B in nu . (succ u) &
nu . (succ u) in a )
by A34, ORDINAL1:22, ORDINAL2:27;
then
B in a
by ORDINAL1:19;
hence
A in a
by A28, ORDINAL1:22;
:: thesis: verum
end;
thus
a c= phi . a
by A1, A24, ORDINAL4:10; :: thesis: a is_cofinal_with omega
take
nu | omega
; :: according to ORDINAL2:def 21 :: thesis: ( proj1 (nu | omega ) = omega & proj2 (nu | omega ) c= a & nu | omega is increasing & a = sup (nu | omega ) )
thus
( proj1 (nu | omega ) = omega & proj2 (nu | omega ) c= a & nu | omega is increasing & a = sup (nu | omega ) )
by A5, A8, A11, RELAT_1:91; :: thesis: verum