let T be infinite-weight TopSpace; for B being Basis of T ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
let B be Basis of T; ex B1 being Basis of T st
( B1 c= B & card B1 = weight T )
consider B0 being Basis of T such that
A1:
card B0 = weight T
by WAYBEL23:74;
defpred S1[ object , object ] means ex A being set st
( A = $2 & union A = $1 & card A c= weight T );
A2:
now for a being object st a in B0 holds
ex b being object st
( b in bool B & S1[a,b] )let a be
object ;
( a in B0 implies ex b being object st
( b in bool B & S1[a,b] ) )reconsider aa =
a as
set by TARSKI:1;
set Sa =
{ U where U is Subset of T : ( U in B & U c= aa ) } ;
A3:
{ U where U is Subset of T : ( U in B & U c= aa ) } c= B
assume
a in B0
;
ex b being object st
( b in bool B & S1[a,b] )then reconsider W =
a as
open Subset of
T by YELLOW_8:10;
A4:
union { U where U is Subset of T : ( U in B & U c= aa ) } = W
by YELLOW_8:9;
reconsider Sa =
{ U where U is Subset of T : ( U in B & U c= aa ) } as
open Subset-Family of
T by A3, TOPS_2:11, XBOOLE_1:1;
consider G being
open Subset-Family of
T such that A5:
G c= Sa
and A6:
union G = union Sa
and A7:
card G c= weight T
by Th11;
reconsider b =
G as
object ;
take b =
b;
( b in bool B & S1[a,b] )
G c= B
by A3, A5;
hence
b in bool B
;
S1[a,b]thus
S1[
a,
b]
by A4, A6, A7;
verum end;
consider f being Function such that
A8:
( dom f = B0 & rng f c= bool B )
and
A9:
for a being object st a in B0 holds
S1[a,f . a]
from FUNCT_1:sch 6(A2);
A10:
Union f c= union (bool B)
by A8, ZFMISC_1:77;
then A11:
Union f c= B
by ZFMISC_1:81;
then reconsider B1 = Union f as Subset-Family of T by XBOOLE_1:1;
now ( B1 c= the topology of T & ( for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A ) ) )
B c= the
topology of
T
by TOPS_2:64;
hence
B1 c= the
topology of
T
by A11;
for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A )let A be
Subset of
T;
( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A ) )assume A12:
A is
open
;
for p being Point of T st p in A holds
ex a being Subset of T st
( a in B1 & p in a & a c= A )let p be
Point of
T;
( p in A implies ex a being Subset of T st
( a in B1 & p in a & a c= A ) )assume
p in A
;
ex a being Subset of T st
( a in B1 & p in a & a c= A )then consider U being
Subset of
T such that A13:
U in B0
and A14:
p in U
and A15:
U c= A
by A12, YELLOW_9:31;
A16:
S1[
U,
f . U]
by A9, A13;
then consider a being
set such that A17:
p in a
and A18:
a in f . U
by A14, TARSKI:def 4;
A19:
a c= U
by A16, A18, ZFMISC_1:74;
a in B1
by A8, A13, A18, CARD_5:2;
hence
ex
a being
Subset of
T st
(
a in B1 &
p in a &
a c= A )
by A15, A17, A19, XBOOLE_1:1;
verum end;
then reconsider B1 = B1 as Basis of T by YELLOW_9:32;
then A21:
card B1 c= (weight T) *` (weight T)
by CARD_2:87;
take
B1
; ( B1 c= B & card B1 = weight T )
thus
B1 c= B
by A10, ZFMISC_1:81; card B1 = weight T
weight T is infinite
by Def4;
hence
card B1 c= weight T
by A21, CARD_4:15; XBOOLE_0:def 10 weight T c= card B1
thus
weight T c= card B1
by WAYBEL23:73; verum