let I be Integer; 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 S1[ 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; ( 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
; 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 S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A4:
S1[
n]
;
S1[n + 1]
let TM be
metrizable TopSpace;
( 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
;
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};
( 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;
( 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;
( 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;
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;
( 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
;
a = b
end;
A25:
S1[ 0 ]
proof
let TM be
metrizable TopSpace;
( 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
;
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
;
( 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;
verum
end;
for n being Nat holds S1[n]
from NAT_1:sch 2(A25, A3);
then
S1[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; verum