let T be non empty TopSpace; :: thesis: for F being Subset-Family of T
for S being SetSequence of T st rng S c= F & S is non-empty holds
ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
let F be Subset-Family of T; :: thesis: for S being SetSequence of T st rng S c= F & S is non-empty holds
ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
let S be SetSequence of T; :: thesis: ( rng S c= F & S is non-empty implies ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) ) )
assume A1:
( rng S c= F & S is non-empty )
; :: thesis: ex R being non-empty closed SetSequence of T st
( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
defpred S1[ set , set ] means for i being natural number st i = $1 holds
ex SS being Subset-Family of T st
( SS c= F & SS = { (S . j) where j is Element of NAT : j >= i } & $2 = Cl (union SS) );
A2:
for x being set st x in NAT holds
ex y being set st
( y in bool the carrier of T & S1[x,y] )
consider R being SetSequence of T such that
A7:
for x being set st x in NAT holds
S1[x,R . x]
from FUNCT_2:sch 1(A2);
then reconsider R = R as non-empty closed SetSequence of T by A8, Def6, FUNCT_1:def 15;
take
R
; :: thesis: ( R is non-ascending & ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
hence
R is non-ascending
by KURATO_2:def 5; :: thesis: ( ( F is locally_finite & S is one-to-one implies meet R = {} ) & ( for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } ) ) )
thus
( F is locally_finite & S is one-to-one implies meet R = {} )
:: thesis: for i being natural number ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } )proof
assume A18:
(
F is
locally_finite &
S is
one-to-one )
;
:: thesis: meet R = {}
assume
meet R <> {}
;
:: thesis: contradiction
then consider x being
set such that A19:
x in meet R
by XBOOLE_0:def 1;
reconsider x =
x as
Point of
T by A19;
A20:
dom S = NAT
by FUNCT_2:def 1;
then reconsider rngS =
rng S as non
empty Subset-Family of
T by RELAT_1:65;
rng S is
locally_finite
by A1, A18, PCOMPS_1:12;
then consider W being
Subset of
T such that A21:
(
x in W &
W is
open )
and A22:
{ V where V is Subset of T : ( V in rngS & V meets W ) } is
finite
by PCOMPS_1:def 2;
reconsider Sp =
S as
Function of
NAT ,
rngS by A20, FUNCT_2:3;
reconsider S' =
Sp " as
Function ;
reconsider S' =
S' as
Function of
rngS,
NAT by A18, FUNCT_2:31;
deffunc H1(
Element of
rngS)
-> Element of
NAT =
S' . $1;
set X =
{ V where V is Subset of T : ( V in rngS & V meets W ) } ;
set Y =
{ H1(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } ;
A23:
{ H1(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } is
finite
from FRAENKEL:sch 21(A22);
{ H1(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } c= NAT
then reconsider Y =
{ H1(z) where z is Element of rngS : z in { V where V is Subset of T : ( V in rngS & V meets W ) } } as
Subset of
NAT ;
consider n being
Element of
NAT such that A25:
for
k being
Element of
NAT st
k in Y holds
k <= n
by A23, STIRL2_1:66;
set n1 =
n + 1;
consider Sn being
Subset-Family of
T such that A26:
Sn c= F
and A27:
Sn = { (S . j) where j is Element of NAT : j >= n + 1 }
and A28:
R . (n + 1) = Cl (union Sn)
by A7;
Sn is
locally_finite
by A18, A26, PCOMPS_1:12;
then
(
Cl (union Sn) = union (clf Sn) &
x in R . (n + 1) )
by A19, KURATO_2:6, PCOMPS_1:23;
then consider CLF being
set such that A29:
(
x in CLF &
CLF in clf Sn )
by A28, TARSKI:def 4;
reconsider CLF =
CLF as
Subset of
T by A29;
consider U being
Subset of
T such that A30:
(
CLF = Cl U &
U in Sn )
by A29, PCOMPS_1:def 3;
consider j being
Element of
NAT such that A31:
(
U = S . j &
j >= n + 1 )
by A27, A30;
(
Sp . j in rngS &
Sp . j meets W )
by A21, A29, A30, A31, TOPS_1:39;
then X:
Sp . j in { V where V is Subset of T : ( V in rngS & V meets W ) }
;
(S " ) . (S . j) = j
by A18, FUNCT_2:32;
then
j in Y
by X;
then
j <= n
by A25;
hence
contradiction
by A31, NAT_1:13;
:: thesis: verum
end;
let i be natural number ; :: thesis: ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } )
i in NAT
by ORDINAL1:def 13;
then
ex SS being Subset-Family of T st
( SS c= F & SS = { (S . j) where j is Element of NAT : j >= i } & R . i = Cl (union SS) )
by A7;
hence
ex Si being Subset-Family of T st
( R . i = Cl (union Si) & Si = { (S . j) where j is Element of NAT : j >= i } )
; :: thesis: verum