let I be Integer; :: thesis: for TM being metrizable TopSpace st TM is second-countable & 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 ) holds
( TM is finite-ind & ind TM <= I )
defpred S1[ Nat] means for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 ) holds
( TM is finite-ind & ind TM <= $1 - 1 );
let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & 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 ) implies ( TM is finite-ind & ind TM <= I ) )
assume A1: TM is second-countable ; :: thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= I + 1 ) or ( TM is finite-ind & ind TM <= I ) )
given F being finite Subset-Family of TM such that A2: ( F is Cover of TM & F is finite-ind & ind F <= 0 ) and
A3: card F <= I + 1 ; :: thesis: ( TM is finite-ind & ind TM <= I )
reconsider i1 = I + 1 as Element of NAT by A3, INT_1:3;
A4: S1[ 0 ]
proof
let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st
( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 ) implies ( TM is finite-ind & ind TM <= 0 - 1 ) )
assume TM is second-countable ; :: thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= 0 ) or ( TM is finite-ind & ind TM <= 0 - 1 ) )
given F being finite Subset-Family of TM such that A5: F is Cover of TM and
F is finite-ind and
ind F <= 0 and
A6: card F <= 0 ; :: thesis: ( TM is finite-ind & ind TM <= 0 - 1 )
F = {} by A6;
then [#] TM = {} by A5, SETFAM_1:45, ZFMISC_1:2;
hence ( TM is finite-ind & ind TM <= 0 - 1 ) by TOPDIM_1:6; :: thesis: verum
end;
A7: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A8: S1[n] ; :: thesis: S1[n + 1]
let TM be metrizable TopSpace; :: thesis: ( TM is second-countable & 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 ) implies ( TM is finite-ind & ind TM <= (n + 1) - 1 ) )
assume A9: TM is second-countable ; :: thesis: ( for F being finite Subset-Family of TM holds
( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= n + 1 ) or ( TM is finite-ind & ind TM <= (n + 1) - 1 ) )
given F being finite Subset-Family of TM such that A10: F is Cover of TM and
A11: F is finite-ind and
A12: ind F <= 0 and
A13: card F <= n + 1 ; :: thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
per cases ( F = {} or F <> {} ) ;
suppose F = {} ; :: thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
then card F = 0 ;
hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A4, A9, A10, A11, A12; :: thesis: verum
end;
suppose F <> {} ; :: thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 )
then consider A being object such that
A14: A in F by XBOOLE_0:def 1;
reconsider A = A as Subset of TM by A14;
set AA = {A};
set FA = F \ {A};
A15: (F \ {A}) \/ {A} = F by A14, ZFMISC_1:116;
A16: [#] TM = union F by A10, SETFAM_1:45
.= (union (F \ {A})) \/ (union {A}) by A15, ZFMISC_1:78
.= (union (F \ {A})) \/ A by ZFMISC_1:25 ;
A17: F \ {A} c= F by XBOOLE_1:36;
then A18: ind (F \ {A}) <= 0 by A11, A12, TOPDIM_1:12;
not A in F \ {A} by ZFMISC_1:56;
then F \ {A} c< F by A14, A17;
then card (F \ {A}) < n + 1 by A13, CARD_2:48, XXREAL_0:2;
then A19: card (F \ {A}) <= n by NAT_1:13;
reconsider uFA = union (F \ {A}) as Subset of TM ;
set Tu = TM | uFA;
A20: [#] (TM | uFA) = uFA by PRE_TOPC:def 5;
then reconsider FA9 = F \ {A} as Subset-Family of (TM | uFA) by ZFMISC_1:82;
A21: TM | A is second-countable by A9;
F \ {A} is finite-ind by A11, A17, TOPDIM_1:12;
then A22: ( FA9 is finite-ind & ind (F \ {A}) = ind FA9 ) by TOPDIM_1:30;
A23: FA9 is Cover of (TM | uFA) by A20, SETFAM_1:def 11;
then A24: TM | uFA is finite-ind by A8, A9, A18, A19, A22;
then A25: ind (TM | uFA) = ind uFA by A20, TOPDIM_1:22;
ind (TM | uFA) <= n - 1 by A8, A9, A18, A19, A22, A23;
then A26: (ind uFA) + 1 <= (n - 1) + 1 by A25, XREAL_1:6;
A27: uFA is finite-ind by A24, TOPDIM_1:18;
( A is finite-ind & ind A <= 0 ) by A11, A12, A14, TOPDIM_1:11;
then ( [#] TM is finite-ind & ind ([#] TM) <= (ind uFA) + 1 ) by A16, A21, A27, TOPDIM_1:40;
hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A26, XXREAL_0:2; :: thesis: verum
end;
end;
end;
for n being Nat holds S1[n] from NAT_1:sch 2(A4, A7);
 then S1[i1] ;
hence ( TM is finite-ind & ind TM <= I ) by A1, A2, A3; :: thesis: verum