let I be Integer; 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; ( 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
; ( 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
; ( TM is finite-ind & ind TM <= I )
reconsider i1 = I + 1 as Element of NAT by A3, INT_1:3;
A4:
S1[ 0 ]
A7:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A8:
S1[
n]
;
S1[n + 1]
let TM be
metrizable TopSpace;
( 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
;
( 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
;
( TM is finite-ind & ind TM <= (n + 1) - 1 )
per cases
( F = {} or F <> {} )
;
suppose
F <> {}
;
( 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;
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; verum