let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds
( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
let A, B be Subset of TM; :: thesis: ( A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable implies ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) )
assume that
A1: ( A is finite-ind & B is finite-ind ) and
A2: TM | (A \/ B) is second-countable ; :: thesis: ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
set AB = A \/ B;
set Tab = TM | (A \/ B);
[#] (TM | (A \/ B)) = A \/ B by PRE_TOPC:def 5;
then reconsider a = A, b = B as Subset of (TM | (A \/ B)) by XBOOLE_1:7;
A3: a is finite-ind by A1, TOPDIM_1:21;
then A4: ind ((TM | (A \/ B)) | a) = ind a by TOPDIM_1:17
.= ind A by A1, TOPDIM_1:21 ;
[#] ((TM | (A \/ B)) | b) c= [#] (TM | (A \/ B)) by PRE_TOPC:def 4;
then A5: bool ([#] ((TM | (A \/ B)) | b)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67;
A6: b is finite-ind by A1, TOPDIM_1:21;
then consider Fb being finite Subset-Family of ((TM | (A \/ B)) | b) such that
A7: Fb is Cover of ((TM | (A \/ B)) | b) and
A8: Fb is finite-ind and
A9: ind Fb <= 0 and
A10: card Fb <= (ind ((TM | (A \/ B)) | b)) + 1 and
for a9, b9 being Subset of ((TM | (A \/ B)) | b) st a9 in Fb & b9 in Fb & a9 meets b9 holds
a9 = b9 by A2, Th7;
consider Fa being finite Subset-Family of ((TM | (A \/ B)) | a) such that
A11: Fa is Cover of ((TM | (A \/ B)) | a) and
A12: Fa is finite-ind and
A13: ind Fa <= 0 and
A14: card Fa <= (ind ((TM | (A \/ B)) | a)) + 1 and
for a9, b9 being Subset of ((TM | (A \/ B)) | a) st a9 in Fa & b9 in Fa & a9 meets b9 holds
a9 = b9 by A2, A3, Th7;
[#] ((TM | (A \/ B)) | a) c= [#] (TM | (A \/ B)) by PRE_TOPC:def 4;
then bool ([#] ((TM | (A \/ B)) | a)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67;
then reconsider FA = Fa, FB = Fb as finite Subset-Family of (TM | (A \/ B)) by A5, XBOOLE_1:1;
A15: FB is finite-ind by A8, TOPDIM_1:29;
ind ((TM | (A \/ B)) | b) = ind b by A6, TOPDIM_1:17
.= ind B by A1, TOPDIM_1:21 ;
then ( card (FA \/ FB) <= (card FA) + (card FB) & (card FA) + (card FB) <= ((ind A) + 1) + ((ind B) + 1) ) by A10, A14, A4, CARD_2:43, XREAL_1:7;
then A16: card (FA \/ FB) <= (((ind A) + 1) + (ind B)) + 1 by XXREAL_0:2;
union (FA \/ FB) = (union Fa) \/ (union Fb) by ZFMISC_1:78
.= ([#] ((TM | (A \/ B)) | a)) \/ (union Fb) by A11, SETFAM_1:45
.= ([#] ((TM | (A \/ B)) | a)) \/ ([#] ((TM | (A \/ B)) | b)) by A7, SETFAM_1:45
.= a \/ ([#] ((TM | (A \/ B)) | b)) by PRE_TOPC:def 5
.= a \/ b by PRE_TOPC:def 5
.= [#] (TM | (A \/ B)) by PRE_TOPC:def 5 ;
then A17: FA \/ FB is Cover of (TM | (A \/ B)) by SETFAM_1:def 11;
A18: ind FB = ind Fb by A8, TOPDIM_1:29;
A19: FA is finite-ind by A12, TOPDIM_1:29;
ind FA = ind Fa by A12, TOPDIM_1:29;
then A20: ind (FA \/ FB) <= 0 by A9, A13, A19, A15, A18, TOPDIM_1:13;
then TM | (A \/ B) is finite-ind by A2, A15, A16, A19, A17, Th8;
then A21: A \/ B is finite-ind by TOPDIM_1:18;
ind (TM | (A \/ B)) <= ((ind A) + 1) + (ind B) by A2, A15, A16, A19, A17, A20, Th8;
hence ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by A21, TOPDIM_1:17; :: thesis: verum