let n be Nat; :: thesis: for TM being metrizable TopSpace

for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )

let TM be metrizable TopSpace; :: thesis: for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )

set cTM = [#] TM;

set TOP = the topology of TM;

let M be Subset of TM; :: thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ) )

assume A1: TM | M is second-countable ; :: thesis: ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) )

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ; :: thesis: ( M is finite-ind & ind M <= n )

for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )

let TM be metrizable TopSpace; :: thesis: for H being Subset of TM st TM | H is second-countable holds

( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) )

set cTM = [#] TM;

set TOP = the topology of TM;

let M be Subset of TM; :: thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ) )

assume A1: TM | M is second-countable ; :: thesis: ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) )

hereby :: thesis: ( ex Bas being Basis of TM st

for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) implies ( M is finite-ind & ind M <= n ) )

given B being Basis of TM such that A28:
for A being Subset of TM st A in B holds for A being Subset of TM st A in Bas holds

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) implies ( M is finite-ind & ind M <= n ) )

defpred S_{1}[ object , object ] means for p being Point of TM

for A being Subset of TM st $1 = [p,A] holds

( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = $2 & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) );

assume A2: ( M is finite-ind & ind M <= n ) ; :: thesis: ex RNG being Basis of TM st

for B being Subset of TM st B in RNG holds

( M /\ (Fr b_{4}) is finite-ind & ind (M /\ (Fr b_{4})) <= n - 1 )

A3: for x being object st x in [:([#] TM), the topology of TM:] holds

ex y being object st S_{1}[x,y]

A12: dom f = [:([#] TM), the topology of TM:] and

A13: for x being object st x in [:([#] TM), the topology of TM:] holds

S_{1}[x,f . x]
from CLASSES1:sch 1(A3);

A14: rng f c= the topology of TM

take RNG = RNG; :: thesis: for B being Subset of TM st B in RNG holds

( M /\ (Fr b_{3}) is finite-ind & ind (M /\ (Fr b_{3})) <= n - 1 )

let B be Subset of TM; :: thesis: ( B in RNG implies ( M /\ (Fr b_{2}) is finite-ind & ind (M /\ (Fr b_{2})) <= n - 1 ) )

assume B in RNG ; :: thesis: ( M /\ (Fr b_{2}) is finite-ind & ind (M /\ (Fr b_{2})) <= n - 1 )

then consider x being object such that

A22: x in dom f and

A23: f . x = B by FUNCT_1:def 3;

consider p, A being object such that

A24: p in [#] TM and

A25: A in the topology of TM and

A26: x = [p,A] by A12, A22, ZFMISC_1:def 2;

reconsider A = A as open Subset of TM by A25, PRE_TOPC:def 2;

end;for A being Subset of TM st $1 = [p,A] holds

( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = $2 & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) );

assume A2: ( M is finite-ind & ind M <= n ) ; :: thesis: ex RNG being Basis of TM st

for B being Subset of TM st B in RNG holds

( M /\ (Fr b

A3: for x being object st x in [:([#] TM), the topology of TM:] holds

ex y being object st S

proof

consider f being Function such that
let x be object ; :: thesis: ( x in [:([#] TM), the topology of TM:] implies ex y being object st S_{1}[x,y] )

assume A4: x in [:([#] TM), the topology of TM:] ; :: thesis: ex y being object st S_{1}[x,y]

consider p9, A9 being object such that

A5: p9 in [#] TM and

A6: A9 in the topology of TM and

A7: x = [p9,A9] by A4, ZFMISC_1:def 2;

reconsider A9 = A9 as open Subset of TM by A6, PRE_TOPC:def 2;

reconsider p9 = p9 as Point of TM by A5;

end;assume A4: x in [:([#] TM), the topology of TM:] ; :: thesis: ex y being object st S

consider p9, A9 being object such that

A5: p9 in [#] TM and

A6: A9 in the topology of TM and

A7: x = [p9,A9] by A4, ZFMISC_1:def 2;

reconsider A9 = A9 as open Subset of TM by A6, PRE_TOPC:def 2;

reconsider p9 = p9 as Point of TM by A5;

per cases
( not p9 in A9 or p9 in A9 )
;

end;

suppose A8:
not p9 in A9
; :: thesis: ex y being object st S_{1}[x,y]

take
{} TM
; :: thesis: S_{1}[x, {} TM]

let p be Point of TM; :: thesis: for A being Subset of TM st x = [p,A] holds

( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

let A be Subset of TM; :: thesis: ( x = [p,A] implies ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )

assume A9: x = [p,A] ; :: thesis: ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

p = p9 by A7, A9, XTUPLE_0:1;

hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A7, A8, A9, PRE_TOPC:def 2, XTUPLE_0:1; :: thesis: verum

end;let p be Point of TM; :: thesis: for A being Subset of TM st x = [p,A] holds

( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

let A be Subset of TM; :: thesis: ( x = [p,A] implies ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )

assume A9: x = [p,A] ; :: thesis: ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

p = p9 by A7, A9, XTUPLE_0:1;

hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A7, A8, A9, PRE_TOPC:def 2, XTUPLE_0:1; :: thesis: verum

suppose
p9 in A9
; :: thesis: ex y being object st S_{1}[x,y]

then consider W being open Subset of TM such that

A10: ( p9 in W & W c= A9 & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A1, A2, Th13;

take W ; :: thesis: S_{1}[x,W]

let p be Point of TM; :: thesis: for A being Subset of TM st x = [p,A] holds

( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

let A be Subset of TM; :: thesis: ( x = [p,A] implies ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )

assume A11: x = [p,A] ; :: thesis: ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

( p = p9 & A = A9 ) by A7, A11, XTUPLE_0:1;

hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A10, PRE_TOPC:def 2; :: thesis: verum

end;A10: ( p9 in W & W c= A9 & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A1, A2, Th13;

take W ; :: thesis: S

let p be Point of TM; :: thesis: for A being Subset of TM st x = [p,A] holds

( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

let A be Subset of TM; :: thesis: ( x = [p,A] implies ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) )

assume A11: x = [p,A] ; :: thesis: ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) )

( p = p9 & A = A9 ) by A7, A11, XTUPLE_0:1;

hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st

( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A10, PRE_TOPC:def 2; :: thesis: verum

A12: dom f = [:([#] TM), the topology of TM:] and

A13: for x being object st x in [:([#] TM), the topology of TM:] holds

S

A14: rng f c= the topology of TM

proof

then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng f or y in the topology of TM )

assume y in rng f ; :: thesis: y in the topology of TM

then consider x being object such that

A15: x in dom f and

A16: f . x = y by FUNCT_1:def 3;

ex p, A being object st

( p in [#] TM & A in the topology of TM & x = [p,A] ) by A12, A15, ZFMISC_1:def 2;

hence y in the topology of TM by A12, A13, A15, A16; :: thesis: verum

end;assume y in rng f ; :: thesis: y in the topology of TM

then consider x being object such that

A15: x in dom f and

A16: f . x = y by FUNCT_1:def 3;

ex p, A being object st

( p in [#] TM & A in the topology of TM & x = [p,A] ) by A12, A15, ZFMISC_1:def 2;

hence y in the topology of TM by A12, A13, A15, A16; :: thesis: verum

now :: thesis: for A being Subset of TM st A is open holds

for p being Point of TM st p in A holds

ex W being Subset of TM st

( W in RNG & p in W & W c= A )

then reconsider RNG = RNG as Basis of TM by A14, YELLOW_9:32;for p being Point of TM st p in A holds

ex W being Subset of TM st

( W in RNG & p in W & W c= A )

let A be Subset of TM; :: thesis: ( A is open implies for p being Point of TM st p in A holds

ex W being Subset of TM st

( W in RNG & p in W & W c= A ) )

assume A17: A is open ; :: thesis: for p being Point of TM st p in A holds

ex W being Subset of TM st

( W in RNG & p in W & W c= A )

A18: A in the topology of TM by A17, PRE_TOPC:def 2;

let p be Point of TM; :: thesis: ( p in A implies ex W being Subset of TM st

( W in RNG & p in W & W c= A ) )

assume A19: p in A ; :: thesis: ex W being Subset of TM st

( W in RNG & p in W & W c= A )

A20: [p,A] in [:([#] TM), the topology of TM:] by A18, A19, ZFMISC_1:87;

then consider W being open Subset of TM such that

A21: ( W = f . [p,A] & p in W & W c= A ) and

M /\ (Fr W) is finite-ind and

ind (M /\ (Fr W)) <= n - 1 by A13, A19;

reconsider W = W as Subset of TM ;

take W = W; :: thesis: ( W in RNG & p in W & W c= A )

thus ( W in RNG & p in W & W c= A ) by A12, A20, A21, FUNCT_1:def 3; :: thesis: verum

end;ex W being Subset of TM st

( W in RNG & p in W & W c= A ) )

assume A17: A is open ; :: thesis: for p being Point of TM st p in A holds

ex W being Subset of TM st

( W in RNG & p in W & W c= A )

A18: A in the topology of TM by A17, PRE_TOPC:def 2;

let p be Point of TM; :: thesis: ( p in A implies ex W being Subset of TM st

( W in RNG & p in W & W c= A ) )

assume A19: p in A ; :: thesis: ex W being Subset of TM st

( W in RNG & p in W & W c= A )

A20: [p,A] in [:([#] TM), the topology of TM:] by A18, A19, ZFMISC_1:87;

then consider W being open Subset of TM such that

A21: ( W = f . [p,A] & p in W & W c= A ) and

M /\ (Fr W) is finite-ind and

ind (M /\ (Fr W)) <= n - 1 by A13, A19;

reconsider W = W as Subset of TM ;

take W = W; :: thesis: ( W in RNG & p in W & W c= A )

thus ( W in RNG & p in W & W c= A ) by A12, A20, A21, FUNCT_1:def 3; :: thesis: verum

take RNG = RNG; :: thesis: for B being Subset of TM st B in RNG holds

( M /\ (Fr b

let B be Subset of TM; :: thesis: ( B in RNG implies ( M /\ (Fr b

assume B in RNG ; :: thesis: ( M /\ (Fr b

then consider x being object such that

A22: x in dom f and

A23: f . x = B by FUNCT_1:def 3;

consider p, A being object such that

A24: p in [#] TM and

A25: A in the topology of TM and

A26: x = [p,A] by A12, A22, ZFMISC_1:def 2;

reconsider A = A as open Subset of TM by A25, PRE_TOPC:def 2;

per cases
( p in A or not p in A )
;

end;

suppose
p in A
; :: thesis: ( M /\ (Fr b_{2}) is finite-ind & ind (M /\ (Fr b_{2})) <= n - 1 )

then
ex W being open Subset of TM st

( W = f . [p,A] & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A12, A13, A22, A26;

hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A23, A26; :: thesis: verum

end;( W = f . [p,A] & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A12, A13, A22, A26;

hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A23, A26; :: thesis: verum

suppose
not p in A
; :: thesis: ( M /\ (Fr b_{2}) is finite-ind & ind (M /\ (Fr b_{2})) <= n - 1 )

then
B = {} TM
by A12, A13, A22, A23, A24, A26;

then A27: Fr B = {} by TOPGEN_1:14;

0 - 1 <= n - 1 by XREAL_1:9;

hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A27, TOPDIM_1:6; :: thesis: verum

end;then A27: Fr B = {} by TOPGEN_1:14;

0 - 1 <= n - 1 by XREAL_1:9;

hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A27, TOPDIM_1:6; :: thesis: verum

( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ; :: thesis: ( M is finite-ind & ind M <= n )

for p being Point of TM

for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

proof

hence
( M is finite-ind & ind M <= n )
by A1, Th13; :: thesis: verum
let p be Point of TM; :: thesis: for U being open Subset of TM st p in U holds

ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let U be open Subset of TM; :: thesis: ( p in U implies ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

assume A29: p in U ; :: thesis: ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

consider a being Subset of TM such that

A30: a in B and

A31: ( p in a & a c= U ) by A29, YELLOW_9:31;

B c= the topology of TM by TOPS_2:64;

then reconsider a = a as open Subset of TM by A30, PRE_TOPC:def 2;

take a ; :: thesis: ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 )

thus ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) by A28, A30, A31; :: thesis: verum

end;ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

let U be open Subset of TM; :: thesis: ( p in U implies ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) )

assume A29: p in U ; :: thesis: ex W being open Subset of TM st

( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 )

consider a being Subset of TM such that

A30: a in B and

A31: ( p in a & a c= U ) by A29, YELLOW_9:31;

B c= the topology of TM by TOPS_2:64;

then reconsider a = a as open Subset of TM by A30, PRE_TOPC:def 2;

take a ; :: thesis: ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 )

thus ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) by A28, A30, A31; :: thesis: verum