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

( 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