let I be Integer; :: thesis:
defpred S₁[ 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:
assume that
A1: ( TM is second-countable & TM is finite-ind ) and
A2: ind TM <= I ; :: thesis:
- 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₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
let TM be metrizable TopSpace; :: thesis:
assume that
A5: TM is second-countable and
A6: TM is finite-ind and
A7: ind TM <= (n + 1) - 1 ; :: thesis:
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:
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:
( 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 {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:
let a, b be Subset of TM; :: thesis:
assume that
A20: ( a in G & b in G ) and
A21: a meets b ; :: thesis:

per cases by A20, XBOOLE_0:def 3;

suppose ( a in F & b in F ) ; :: thesis:

hence a = b by A17, A21; :: thesis:

end;

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

then b = B by TARSKI:def 1;
hence a = b by A9, A18, A21, A22, XBOOLE_1:63, ZFMISC_1:74; :: thesis:

end;

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

then a = B by TARSKI:def 1;
hence a = b by A9, A18, A21, A23, XBOOLE_1:63, ZFMISC_1:74; :: thesis:

end;

suppose A24: ( a in {B} & b in {B} ) ; :: thesis:

then a = B by TARSKI:def 1;
hence a = b by A24, TARSKI:def 1; :: thesis:

end;

A25: S₁[ 0 ]

proof

let TM be metrizable TopSpace; :: thesis:
assume that
TM is second-countable and
A26: TM is finite-ind and
A27: ind TM <= 0 - 1 ; :: thesis:
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 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:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A25, A3);
then S₁[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: