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

ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

defpred S_{1}[ Nat] means for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= $1 - 1 holds

ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) );

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= I implies ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

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

A2: ind TM <= I ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

- 1 <= ind ([#] TM) by A1, TOPDIM_1:5;

then - 1 <= I by A2, XXREAL_0:2;

then (- 1) + 1 <= I + 1 by XREAL_1:6;

then reconsider i1 = I + 1 as Element of NAT by INT_1:3;

A3: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]
_{1}[ 0 ]
_{1}[n]
from NAT_1:sch 2(A25, A3);

then S_{1}[i1]
;

hence ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) by A1, A2; :: thesis: verum

ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

defpred S

ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) );

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= I implies ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

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

A2: ind TM <= I ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

- 1 <= ind ([#] TM) by A1, TOPDIM_1:5;

then - 1 <= I by A2, XXREAL_0:2;

then (- 1) + 1 <= I + 1 by XREAL_1:6;

then reconsider i1 = I + 1 as Element of NAT by INT_1:3;

A3: for n being Nat st S

S

proof

A25:
S
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A4: S_{1}[n]
; :: thesis: S_{1}[n + 1]

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= (n + 1) - 1 implies ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

A5: TM is second-countable and

A6: TM is finite-ind and

A7: ind TM <= (n + 1) - 1 ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

consider A, B being Subset of TM such that

A8: [#] TM = A \/ B and

A9: A misses B and

A10: ind A <= n - 1 and

A11: ind B <= 0 by A5, A6, A7, Lm3;

set BB = {B};

for b being Subset of TM st b in {B} holds

( b is finite-ind & ind b <= 0 ) by A6, A11, TARSKI:def 1;

then A12: ( {B} is finite-ind & ind {B} <= 0 ) by TOPDIM_1:11;

set TA = TM | A;

ind (TM | A) = ind A by A6, TOPDIM_1:17;

then consider F being finite Subset-Family of (TM | A) such that

A13: F is Cover of (TM | A) and

A14: F is finite-ind and

A15: ind F <= 0 and

A16: card F <= n and

A17: for A, B being Subset of (TM | A) st A in F & B in F & A meets B holds

A = B by A4, A5, A6, A10;

[#] (TM | A) c= [#] TM by PRE_TOPC:def 4;

then bool ([#] (TM | A)) c= bool ([#] TM) by ZFMISC_1:67;

then reconsider F9 = F as finite Subset-Family of TM by XBOOLE_1:1;

take G = F9 \/ {B}; :: thesis: ( G is Cover of TM & G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

A18: union F9 = [#] (TM | A) by A13, SETFAM_1:45

.= A by PRE_TOPC:def 5 ;

then union G = A \/ (union {B}) by ZFMISC_1:78

.= [#] TM by A8, ZFMISC_1:25 ;

hence G is Cover of TM by SETFAM_1:def 11; :: thesis: ( G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

( F9 is finite-ind & ind F9 = ind F ) by A14, TOPDIM_1:29;

hence ( G is finite-ind & ind G <= 0 ) by A12, A15, TOPDIM_1:13; :: thesis: ( card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

card {B} = 1 by CARD_1:30;

then A19: card G <= (card F9) + 1 by CARD_2:43;

(card F9) + 1 <= n + 1 by A16, XREAL_1:6;

hence card G <= n + 1 by A19, XXREAL_0:2; :: thesis: for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B

let a, b be Subset of TM; :: thesis: ( a in G & b in G & a meets b implies a = b )

assume that

A20: ( a in G & b in G ) and

A21: a meets b ; :: thesis: a = b

end;assume A4: S

let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & TM is finite-ind & ind TM <= (n + 1) - 1 implies ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

A5: TM is second-countable and

A6: TM is finite-ind and

A7: ind TM <= (n + 1) - 1 ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

consider A, B being Subset of TM such that

A8: [#] TM = A \/ B and

A9: A misses B and

A10: ind A <= n - 1 and

A11: ind B <= 0 by A5, A6, A7, Lm3;

set BB = {B};

for b being Subset of TM st b in {B} holds

( b is finite-ind & ind b <= 0 ) by A6, A11, TARSKI:def 1;

then A12: ( {B} is finite-ind & ind {B} <= 0 ) by TOPDIM_1:11;

set TA = TM | A;

ind (TM | A) = ind A by A6, TOPDIM_1:17;

then consider F being finite Subset-Family of (TM | A) such that

A13: F is Cover of (TM | A) and

A14: F is finite-ind and

A15: ind F <= 0 and

A16: card F <= n and

A17: for A, B being Subset of (TM | A) st A in F & B in F & A meets B holds

A = B by A4, A5, A6, A10;

[#] (TM | A) c= [#] TM by PRE_TOPC:def 4;

then bool ([#] (TM | A)) c= bool ([#] TM) by ZFMISC_1:67;

then reconsider F9 = F as finite Subset-Family of TM by XBOOLE_1:1;

take G = F9 \/ {B}; :: thesis: ( G is Cover of TM & G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

A18: union F9 = [#] (TM | A) by A13, SETFAM_1:45

.= A by PRE_TOPC:def 5 ;

then union G = A \/ (union {B}) by ZFMISC_1:78

.= [#] TM by A8, ZFMISC_1:25 ;

hence G is Cover of TM by SETFAM_1:def 11; :: thesis: ( G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

( F9 is finite-ind & ind F9 = ind F ) by A14, TOPDIM_1:29;

hence ( G is finite-ind & ind G <= 0 ) by A12, A15, TOPDIM_1:13; :: thesis: ( card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B ) )

card {B} = 1 by CARD_1:30;

then A19: card G <= (card F9) + 1 by CARD_2:43;

(card F9) + 1 <= n + 1 by A16, XREAL_1:6;

hence card G <= n + 1 by A19, XXREAL_0:2; :: thesis: for A, B being Subset of TM st A in G & B in G & A meets B holds

A = B

let a, b be Subset of TM; :: thesis: ( a in G & b in G & a meets b implies a = b )

assume that

A20: ( a in G & b in G ) and

A21: a meets b ; :: thesis: a = b

per cases
( ( a in F & b in F ) or ( a in F & b in {B} ) or ( a in {B} & b in F ) or ( a in {B} & b in {B} ) )
by A20, XBOOLE_0:def 3;

end;

suppose A22:
( a in F & b in {B} )
; :: thesis: a = b

then
b = B
by TARSKI:def 1;

hence a = b by A9, A18, A21, A22, XBOOLE_1:63, ZFMISC_1:74; :: thesis: verum

end;hence a = b by A9, A18, A21, A22, XBOOLE_1:63, ZFMISC_1:74; :: thesis: verum

suppose A23:
( a in {B} & b in F )
; :: thesis: a = b

then
a = B
by TARSKI:def 1;

hence a = b by A9, A18, A21, A23, XBOOLE_1:63, ZFMISC_1:74; :: thesis: verum

end;hence a = b by A9, A18, A21, A23, XBOOLE_1:63, ZFMISC_1:74; :: thesis: verum

proof

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

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

TM is second-countable and

A26: TM is finite-ind and

A27: ind TM <= 0 - 1 ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

ind ([#] TM) >= - 1 by A26, TOPDIM_1:5;

then ind ([#] TM) = - 1 by A27, XXREAL_0:1;

then A28: [#] TM = {} TM by A26, TOPDIM_1:6;

reconsider F = {} as empty Subset-Family of TM by TOPGEN_4:18;

take F ; :: thesis: ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

F c= {({} TM)} ;

hence ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) by A28, SETFAM_1:def 11, TOPDIM_1:10, ZFMISC_1:2; :: thesis: verum

end;( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) )

assume that

TM is second-countable and

A26: TM is finite-ind and

A27: ind TM <= 0 - 1 ; :: thesis: ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

ind ([#] TM) >= - 1 by A26, TOPDIM_1:5;

then ind ([#] TM) = - 1 by A27, XXREAL_0:1;

then A28: [#] TM = {} TM by A26, TOPDIM_1:6;

reconsider F = {} as empty Subset-Family of TM by TOPGEN_4:18;

take F ; :: thesis: ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) )

F c= {({} TM)} ;

hence ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) by A28, SETFAM_1:def 11, TOPDIM_1:10, ZFMISC_1:2; :: thesis: verum

then S

hence ex F being finite Subset-Family of TM st

( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds

A = B ) ) by A1, A2; :: thesis: verum