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 S_{1}[ 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: S_{1}[ 0 ]
_{1}[n] holds

S_{1}[n + 1]
_{1}[n]
from NAT_1:sch 2(A4, A7);

then S_{1}[i1]
;

hence ( TM is finite-ind & ind TM <= I ) by A1, A2, A3; :: thesis: verum

( 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 S

( 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: S

proof

A7:
for n being Nat st S
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;( 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

S

proof

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

assume A8: S_{1}[n]
; :: thesis: S_{1}[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 )

end;assume A8: S

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 <> {} )
;

end;

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;hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A4, A9, A10, A11, A12; :: thesis: verum

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;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

then S

hence ( TM is finite-ind & ind TM <= I ) by A1, A2, A3; :: thesis: verum