let M be non countable Aleph; :: thesis: ( omega in cf M implies for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded ) )
assume A1:
omega in cf M
; :: thesis: for S being non empty Subset-Family of M st card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) holds
( meet S is closed & meet S is unbounded )
let S be non empty Subset-Family of M; :: thesis: ( card S in cf M & ( for X being Element of S holds
( X is closed & X is unbounded ) ) implies ( meet S is closed & meet S is unbounded ) )
assume that
A2:
card S in cf M
and
A3:
for X being Element of S holds
( X is closed & X is unbounded )
; :: thesis: ( meet S is closed & meet S is unbounded )
thus
meet S is closed
by A3, Th22; :: thesis: meet S is unbounded
for B1 being Ordinal st B1 in M holds
ex C being Ordinal st
( C in meet S & B1 c= C )
proof
let B1 be
Ordinal;
:: thesis: ( B1 in M implies ex C being Ordinal st
( C in meet S & B1 c= C ) )
assume A4:
B1 in M
;
:: thesis: ex C being Ordinal st
( C in meet S & B1 c= C )
reconsider B11 =
B1 as
Element of
M by A4;
deffunc H1(
Element of
M)
-> Element of
bool M =
{ (LBound $1,X) where X is Element of S : X in S } /\ ([#] M);
A5:
for
B being
Element of
M holds
H1(
B)
= { (LBound B,X) where X is Element of S : X in S }
A8:
for
B being
Element of
M holds
(
sup H1(
B)
in M &
B in sup H1(
B) )
defpred S1[
set ,
Element of
M,
set ]
means ( $3
= sup H1($2) & $2
in $3 );
A11:
for
n being
Element of
NAT for
x being
Element of
M ex
y being
Element of
M st
S1[
n,
x,
y]
consider L being
Function of
NAT ,
M such that A12:
L . 0 = B11
and A13:
for
n being
Element of
NAT holds
S1[
n,
L . n,
L . (n + 1)]
from RECDEF_1:sch 2(A11);
take
sup (rng L)
;
:: thesis: ( sup (rng L) in meet S & B1 c= sup (rng L) )
reconsider L1 =
L as
Function of
NAT ,
([#] M) ;
A14:
sup (rng L1) in M
by A1, Th23;
A15:
B1 in rng L
by A12, FUNCT_2:6;
then A16:
B1 in sup (rng L)
by ORDINAL2:27;
reconsider RNG =
rng L as
Subset of
M by RELAT_1:def 19;
for
C1 being
Ordinal st
C1 in RNG holds
ex
C2 being
Ordinal st
(
C2 in RNG &
C1 in C2 )
then reconsider SUPL =
sup RNG as
limit_ordinal infinite Element of
M by A14, A15, Th4;
for
X1 being
set st
X1 in S holds
SUPL in X1
proof
let X1 be
set ;
:: thesis: ( X1 in S implies SUPL in X1 )
assume A20:
X1 in S
;
:: thesis: SUPL in X1
reconsider X =
X1 as
Element of
S by A20;
A21:
(
X is
closed &
X is
unbounded &
X in S )
by A3;
then A22:
not
X is
empty
by Th8;
sup (X /\ SUPL) = SUPL
proof
sup (X /\ SUPL) c= sup SUPL
by ORDINAL2:30, XBOOLE_1:17;
then A23:
sup (X /\ SUPL) c= SUPL
by ORDINAL2:26;
assume
sup (X /\ SUPL) <> SUPL
;
:: thesis: contradiction
then
sup (X /\ SUPL) c< SUPL
by A23, XBOOLE_0:def 8;
then consider B3 being
Ordinal such that A24:
B3 in rng L
and A25:
sup (X /\ SUPL) c= B3
by ORDINAL1:21, ORDINAL2:29;
consider y1 being
set such that A26:
y1 in dom L
and A27:
B3 = L . y1
by A24, FUNCT_1:def 5;
reconsider y =
y1 as
Element of
NAT by A26, FUNCT_2:def 1;
LBound (L . y),
X in X
by A22;
then reconsider LBY =
LBound (L . y),
X as
Element of
M ;
LBound (L . y),
X in { (LBound (L . y),Y) where Y is Element of S : Y in S }
;
then
LBound (L . y),
X in H1(
L . y)
by A5;
then
LBY in sup H1(
L . y)
by ORDINAL2:27;
then A28:
LBound (L . y),
X in L . (y + 1)
by A13;
L . (y + 1) in rng L
by FUNCT_2:6;
then
L . (y + 1) in SUPL
by ORDINAL2:27;
then
LBY in SUPL
by A28, ORDINAL1:19;
then
LBound (L . y),
X in X /\ SUPL
by A22, XBOOLE_0:def 4;
then
LBY in sup (X /\ SUPL)
by ORDINAL2:27;
then
LBY in L . y
by A25, A27;
hence
contradiction
by A21, Th10;
:: thesis: verum
end;
hence
SUPL in X1
by A21, Def5;
:: thesis: verum
end;
hence
sup (rng L) in meet S
by SETFAM_1:def 1;
:: thesis: B1 c= sup (rng L)
thus
B1 c= sup (rng L)
by A16, ORDINAL1:def 2;
:: thesis: verum
end;
hence
meet S is unbounded
by Th7; :: thesis: verum