let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds

for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= n implies for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )

assume that

A1: ( TM is second-countable & TM is finite-ind ) and

A2: ind TM <= n ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

reconsider I = n as Integer ;

consider G being finite Subset-Family of TM such that

A3: G is Cover of TM and

A4: ( G is finite-ind & ind G <= 0 ) and

A5: card G <= I + 1 and

for a, b being Subset of TM st a in G & b in G & a meets b holds

a = b by A1, A2, Th7;

set cTM = the carrier of TM;

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of TM implies ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )

assume that

A6: F is open and

A7: F is Cover of TM ; :: thesis: ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

A8: card ((n + 1) * (card F)) = (n + 1) * (card F) ;

defpred S_{1}[ object , object ] means for A being Subset of TM st A = $1 holds

ex g being Function of F,(bool the carrier of TM) st

( $2 = rng g & rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) );

A9: for x being object st x in G holds

ex y being object st

( y in bool (bool the carrier of TM) & S_{1}[x,y] )

A14: for x being object st x in G holds

S_{1}[x,GG . x]
from FUNCT_2:sch 1(A9);

union (rng GG) c= union (bool (bool the carrier of TM)) by ZFMISC_1:77;

then reconsider Ugg = Union GG as Subset-Family of TM ;

A15: dom GG = G by FUNCT_2:def 1;

A16: for x being object st x in dom GG holds

card (GG . x) c= card F

then A19: card Ugg c= (n + 1) *` (card F) by A16, CARD_2:86;

( card (card F) = card F & card (n + 1) = n + 1 ) ;

then A20: (n + 1) *` (card F) = (n + 1) * (card F) by A8, CARD_2:39;

then reconsider Ugg = Ugg as finite Subset-Family of TM by A19;

take Ugg ; :: thesis: ( Ugg is open & Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )

thus Ugg is open :: thesis: ( Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )

thus Ugg is_finer_than F :: thesis: ( card Ugg <= (card F) * (n + 1) & order Ugg <= n )

hence card Ugg <= (card F) * (n + 1) by NAT_1:39; :: thesis: order Ugg <= n

defpred S_{2}[ object , object ] means $1 in GG . $2;

for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= n implies for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )

assume that

A1: ( TM is second-countable & TM is finite-ind ) and

A2: ind TM <= n ; :: thesis: for F being finite Subset-Family of TM st F is open & F is Cover of TM holds

ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

reconsider I = n as Integer ;

consider G being finite Subset-Family of TM such that

A3: G is Cover of TM and

A4: ( G is finite-ind & ind G <= 0 ) and

A5: card G <= I + 1 and

for a, b being Subset of TM st a in G & b in G & a meets b holds

a = b by A1, A2, Th7;

set cTM = the carrier of TM;

let F be finite Subset-Family of TM; :: thesis: ( F is open & F is Cover of TM implies ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) )

assume that

A6: F is open and

A7: F is Cover of TM ; :: thesis: ex G being finite Subset-Family of TM st

( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n )

A8: card ((n + 1) * (card F)) = (n + 1) * (card F) ;

defpred S

ex g being Function of F,(bool the carrier of TM) st

( $2 = rng g & rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) );

A9: for x being object st x in G holds

ex y being object st

( y in bool (bool the carrier of TM) & S

proof

consider GG being Function of G,(bool (bool the carrier of TM)) such that
let x be object ; :: thesis: ( x in G implies ex y being object st

( y in bool (bool the carrier of TM) & S_{1}[x,y] ) )

assume A10: x in G ; :: thesis: ex y being object st

( y in bool (bool the carrier of TM) & S_{1}[x,y] )

then reconsider A = x as Subset of TM ;

A11: TM | A is second-countable by A1;

[#] TM c= union F by A7, SETFAM_1:def 11;

then A c= union F ;

then A12: F is Cover of A by SETFAM_1:def 11;

( A is finite-ind & ind A <= 0 ) by A4, A10, TOPDIM_1:11;

then consider g being Function of F,(bool the carrier of TM) such that

A13: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A6, A11, A12, Th22;

take rng g ; :: thesis: ( rng g in bool (bool the carrier of TM) & S_{1}[x, rng g] )

thus ( rng g in bool (bool the carrier of TM) & S_{1}[x, rng g] )
by A13; :: thesis: verum

end;( y in bool (bool the carrier of TM) & S

assume A10: x in G ; :: thesis: ex y being object st

( y in bool (bool the carrier of TM) & S

then reconsider A = x as Subset of TM ;

A11: TM | A is second-countable by A1;

[#] TM c= union F by A7, SETFAM_1:def 11;

then A c= union F ;

then A12: F is Cover of A by SETFAM_1:def 11;

( A is finite-ind & ind A <= 0 ) by A4, A10, TOPDIM_1:11;

then consider g being Function of F,(bool the carrier of TM) such that

A13: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A6, A11, A12, Th22;

take rng g ; :: thesis: ( rng g in bool (bool the carrier of TM) & S

thus ( rng g in bool (bool the carrier of TM) & S

A14: for x being object st x in G holds

S

union (rng GG) c= union (bool (bool the carrier of TM)) by ZFMISC_1:77;

then reconsider Ugg = Union GG as Subset-Family of TM ;

A15: dom GG = G by FUNCT_2:def 1;

A16: for x being object st x in dom GG holds

card (GG . x) c= card F

proof

Segm (card (dom GG)) c= Segm (n + 1)
by A5, A15, NAT_1:39;
let x be object ; :: thesis: ( x in dom GG implies card (GG . x) c= card F )

assume A17: x in dom GG ; :: thesis: card (GG . x) c= card F

then reconsider A = x as Subset of TM by A15;

consider g being Function of F,(bool the carrier of TM) such that

A18: GG . x = rng g and

rng g is open and

rng g is Cover of A and

for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A17;

dom g = F by FUNCT_2:def 1;

hence card (GG . x) c= card F by A18, CARD_1:12; :: thesis: verum

end;assume A17: x in dom GG ; :: thesis: card (GG . x) c= card F

then reconsider A = x as Subset of TM by A15;

consider g being Function of F,(bool the carrier of TM) such that

A18: GG . x = rng g and

rng g is open and

rng g is Cover of A and

for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A17;

dom g = F by FUNCT_2:def 1;

hence card (GG . x) c= card F by A18, CARD_1:12; :: thesis: verum

then A19: card Ugg c= (n + 1) *` (card F) by A16, CARD_2:86;

( card (card F) = card F & card (n + 1) = n + 1 ) ;

then A20: (n + 1) *` (card F) = (n + 1) * (card F) by A8, CARD_2:39;

then reconsider Ugg = Ugg as finite Subset-Family of TM by A19;

take Ugg ; :: thesis: ( Ugg is open & Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )

thus Ugg is open :: thesis: ( Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )

proof

[#] TM c= union Ugg
let A be Subset of TM; :: according to TOPS_2:def 1 :: thesis: ( not A in Ugg or A is open )

assume A in Ugg ; :: thesis: A is open

then consider Y being set such that

A21: A in Y and

A22: Y in rng GG by TARSKI:def 4;

consider x being object such that

A23: ( x in dom GG & Y = GG . x ) by A22, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

ex g being Function of F,(bool the carrier of TM) st

( Y = rng g & rng g is open & rng g is Cover of x & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A14, A15, A23;

hence A is open by A21; :: thesis: verum

end;assume A in Ugg ; :: thesis: A is open

then consider Y being set such that

A21: A in Y and

A22: Y in rng GG by TARSKI:def 4;

consider x being object such that

A23: ( x in dom GG & Y = GG . x ) by A22, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

ex g being Function of F,(bool the carrier of TM) st

( Y = rng g & rng g is open & rng g is Cover of x & ( for a being set st a in F holds

g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b ) ) by A14, A15, A23;

hence A is open by A21; :: thesis: verum

proof

hence
Ugg is Cover of TM
by SETFAM_1:def 11; :: thesis: ( Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n )
A24:
[#] TM c= union G
by A3, SETFAM_1:def 11;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] TM or x in union Ugg )

assume A25: x in [#] TM ; :: thesis: x in union Ugg

consider A being set such that

A26: x in A and

A27: A in G by A24, A25, TARSKI:def 4;

consider g being Function of F,(bool the carrier of TM) such that

A28: GG . A = rng g and

rng g is open and

A29: rng g is Cover of A and

for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A27;

A c= union (rng g) by A29, SETFAM_1:def 11;

then consider y being set such that

A30: x in y and

A31: y in rng g by A26, TARSKI:def 4;

GG . A in rng GG by A15, A27, FUNCT_1:def 3;

then y in Ugg by A28, A31, TARSKI:def 4;

hence x in union Ugg by A30, TARSKI:def 4; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] TM or x in union Ugg )

assume A25: x in [#] TM ; :: thesis: x in union Ugg

consider A being set such that

A26: x in A and

A27: A in G by A24, A25, TARSKI:def 4;

consider g being Function of F,(bool the carrier of TM) such that

A28: GG . A = rng g and

rng g is open and

A29: rng g is Cover of A and

for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A27;

A c= union (rng g) by A29, SETFAM_1:def 11;

then consider y being set such that

A30: x in y and

A31: y in rng g by A26, TARSKI:def 4;

GG . A in rng GG by A15, A27, FUNCT_1:def 3;

then y in Ugg by A28, A31, TARSKI:def 4;

hence x in union Ugg by A30, TARSKI:def 4; :: thesis: verum

thus Ugg is_finer_than F :: thesis: ( card Ugg <= (card F) * (n + 1) & order Ugg <= n )

proof

Segm (card Ugg) c= Segm ((card F) * (n + 1))
by A19, A20;
let A be set ; :: according to SETFAM_1:def 2 :: thesis: ( not A in Ugg or ex b_{1} being set st

( b_{1} in F & A c= b_{1} ) )

assume A in Ugg ; :: thesis: ex b_{1} being set st

( b_{1} in F & A c= b_{1} )

then consider Y being set such that

A32: A in Y and

A33: Y in rng GG by TARSKI:def 4;

consider x being object such that

A34: ( x in dom GG & Y = GG . x ) by A33, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

consider g being Function of F,(bool the carrier of TM) such that

A35: Y = rng g and

rng g is open and

rng g is Cover of x and

A36: for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A15, A34;

dom g = F by FUNCT_2:def 1;

then ex z being object st

( z in F & g . z = A ) by A32, A35, FUNCT_1:def 3;

hence ex b_{1} being set st

( b_{1} in F & A c= b_{1} )
by A36; :: thesis: verum

end;( b

assume A in Ugg ; :: thesis: ex b

( b

then consider Y being set such that

A32: A in Y and

A33: Y in rng GG by TARSKI:def 4;

consider x being object such that

A34: ( x in dom GG & Y = GG . x ) by A33, FUNCT_1:def 3;

reconsider x = x as set by TARSKI:1;

consider g being Function of F,(bool the carrier of TM) such that

A35: Y = rng g and

rng g is open and

rng g is Cover of x and

A36: for a being set st a in F holds

g . a c= a and

for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14, A15, A34;

dom g = F by FUNCT_2:def 1;

then ex z being object st

( z in F & g . z = A ) by A32, A35, FUNCT_1:def 3;

hence ex b

( b

hence card Ugg <= (card F) * (n + 1) by NAT_1:39; :: thesis: order Ugg <= n

defpred S

now :: thesis: for H being finite Subset-Family of TM st H c= Ugg & card H > n + 1 holds

meet H is empty

hence
order Ugg <= n
by Th3; :: thesis: verummeet H is empty

let H be finite Subset-Family of TM; :: thesis: ( H c= Ugg & card H > n + 1 implies meet H is empty )

assume that

A37: H c= Ugg and

A38: card H > n + 1 ; :: thesis: meet H is empty

not H is empty by A38;

then consider XX being object such that

A39: XX in H ;

A40: for x being object st x in H holds

ex y being object st

( y in G & S_{2}[x,y] )

A43: for x being object st x in H holds

S_{2}[x,q . x]
from FUNCT_2:sch 1(A40);

ex y being object st

( y in G & S_{2}[XX,y] )
by A40, A39;

then A44: dom q = H by FUNCT_2:def 1;

assume not meet H is empty ; :: thesis: contradiction

then consider x being object such that

A45: x in meet H ;

for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds

x1 = x2

rng q c= G ;

then Segm (card H) c= Segm (card G) by A54, A44, CARD_1:10;

then card H <= card G by NAT_1:39;

hence contradiction by A5, A38, XXREAL_0:2; :: thesis: verum

end;assume that

A37: H c= Ugg and

A38: card H > n + 1 ; :: thesis: meet H is empty

not H is empty by A38;

then consider XX being object such that

A39: XX in H ;

A40: for x being object st x in H holds

ex y being object st

( y in G & S

proof

consider q being Function of H,G such that
let A be object ; :: thesis: ( A in H implies ex y being object st

( y in G & S_{2}[A,y] ) )

assume A in H ; :: thesis: ex y being object st

( y in G & S_{2}[A,y] )

then consider Y being set such that

A41: A in Y and

A42: Y in rng GG by A37, TARSKI:def 4;

ex x being object st

( x in dom GG & Y = GG . x ) by A42, FUNCT_1:def 3;

hence ex y being object st

( y in G & S_{2}[A,y] )
by A41; :: thesis: verum

end;( y in G & S

assume A in H ; :: thesis: ex y being object st

( y in G & S

then consider Y being set such that

A41: A in Y and

A42: Y in rng GG by A37, TARSKI:def 4;

ex x being object st

( x in dom GG & Y = GG . x ) by A42, FUNCT_1:def 3;

hence ex y being object st

( y in G & S

A43: for x being object st x in H holds

S

ex y being object st

( y in G & S

then A44: dom q = H by FUNCT_2:def 1;

assume not meet H is empty ; :: thesis: contradiction

then consider x being object such that

A45: x in meet H ;

for x1, x2 being object st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds

x1 = x2

proof

then A54:
q is one-to-one
by FUNCT_1:def 4;
let x1, x2 be object ; :: thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 )

assume that

A46: x1 in dom q and

A47: x2 in dom q and

A48: q . x1 = q . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as set by TARSKI:1;

( x in x1 & x in x2 ) by A45, A46, A47, SETFAM_1:def 1;

then A49: x1 meets x2 by XBOOLE_0:3;

q . x1 in rng q by A46, FUNCT_1:def 3;

then q . x1 in G ;

then consider g being Function of F,(bool the carrier of TM) such that

A50: GG . (q . x1) = rng g and

rng g is open and

rng g is Cover of q . x1 and

for a being set st a in F holds

g . a c= a and

A51: for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14;

A52: dom g = F by FUNCT_2:def 1;

x2 in GG . (q . x1) by A43, A47, A48;

then A53: ex y2 being object st

( y2 in F & x2 = g . y2 ) by A50, A52, FUNCT_1:def 3;

x1 in GG . (q . x1) by A43, A46;

then ex y1 being object st

( y1 in F & x1 = g . y1 ) by A50, A52, FUNCT_1:def 3;

hence x1 = x2 by A49, A51, A53; :: thesis: verum

end;assume that

A46: x1 in dom q and

A47: x2 in dom q and

A48: q . x1 = q . x2 ; :: thesis: x1 = x2

reconsider x1 = x1, x2 = x2 as set by TARSKI:1;

( x in x1 & x in x2 ) by A45, A46, A47, SETFAM_1:def 1;

then A49: x1 meets x2 by XBOOLE_0:3;

q . x1 in rng q by A46, FUNCT_1:def 3;

then q . x1 in G ;

then consider g being Function of F,(bool the carrier of TM) such that

A50: GG . (q . x1) = rng g and

rng g is open and

rng g is Cover of q . x1 and

for a being set st a in F holds

g . a c= a and

A51: for a, b being set st a in F & b in F & a <> b holds

g . a misses g . b by A14;

A52: dom g = F by FUNCT_2:def 1;

x2 in GG . (q . x1) by A43, A47, A48;

then A53: ex y2 being object st

( y2 in F & x2 = g . y2 ) by A50, A52, FUNCT_1:def 3;

x1 in GG . (q . x1) by A43, A46;

then ex y1 being object st

( y1 in F & x1 = g . y1 ) by A50, A52, FUNCT_1:def 3;

hence x1 = x2 by A49, A51, A53; :: thesis: verum

rng q c= G ;

then Segm (card H) c= Segm (card G) by A54, A44, CARD_1:10;

then card H <= card G by NAT_1:39;

hence contradiction by A5, A38, XXREAL_0:2; :: thesis: verum