let TM be metrizable TopSpace; :: thesis: for A, B being Subset of TM st A is with_finite_small_inductive_dimension & B is with_finite_small_inductive_dimension & TM | (A \/ B) is second-countable holds
( A \/ B is with_finite_small_inductive_dimension & ind (A \/ B) <= ((ind A) + (ind B)) + 1 )
let A, B be Subset of TM; :: thesis: ( A is with_finite_small_inductive_dimension & B is with_finite_small_inductive_dimension & TM | (A \/ B) is second-countable implies ( A \/ B is with_finite_small_inductive_dimension & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) )
assume that
A1: ( A is with_finite_small_inductive_dimension & B is with_finite_small_inductive_dimension ) and
A2: TM | (A \/ B) is second-countable ; :: thesis: ( A \/ B is with_finite_small_inductive_dimension & 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 10;
then reconsider a = A, b = B as Subset of (TM | (A \/ B)) by XBOOLE_1:7;
A5: a is with_finite_small_inductive_dimension by A1, TOPDIM_1:21;
then A6: 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 9;
then A7: bool ([#] ((TM | (A \/ B)) | b)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:79;
A8: b is with_finite_small_inductive_dimension by A1, TOPDIM_1:21;
then consider Fb being finite Subset-Family of ((TM | (A \/ B)) | b) such that
A9: Fb is Cover of ((TM | (A \/ B)) | b) and
A10: Fb is with_finite_small_inductive_dimension and
A11: ind Fb <= 0 and
A12: 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
A13: Fa is Cover of ((TM | (A \/ B)) | a) and
A14: Fa is with_finite_small_inductive_dimension and
A15: ind Fa <= 0 and
A16: 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, A5, Th7;
[#] ((TM | (A \/ B)) | a) c= [#] (TM | (A \/ B)) by PRE_TOPC:def 9;
then bool ([#] ((TM | (A \/ B)) | a)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:79;
then reconsider FA = Fa, FB = Fb as finite Subset-Family of (TM | (A \/ B)) by A7, XBOOLE_1:1;
A17: FB is with_finite_small_inductive_dimension by A10, TOPDIM_1:29;
ind ((TM | (A \/ B)) | b) = ind b by A8, 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 A12, A16, A6, CARD_2:62, XREAL_1:9;
then A18: card (FA \/ FB) <= (((ind A) + 1) + (ind B)) + 1 by XXREAL_0:2;
union (FA \/ FB) = (union Fa) \/ (union Fb) by ZFMISC_1:96
.= ([#] ((TM | (A \/ B)) | a)) \/ (union Fb) by A13, SETFAM_1:60
.= ([#] ((TM | (A \/ B)) | a)) \/ ([#] ((TM | (A \/ B)) | b)) by A9, SETFAM_1:60
.= a \/ ([#] ((TM | (A \/ B)) | b)) by PRE_TOPC:def 10
.= a \/ b by PRE_TOPC:def 10
.= [#] (TM | (A \/ B)) by PRE_TOPC:def 10 ;
then A19: FA \/ FB is Cover of (TM | (A \/ B)) by SETFAM_1:def 12;
A20: ind FB = ind Fb by A10, TOPDIM_1:29;
A21: FA is with_finite_small_inductive_dimension by A14, TOPDIM_1:29;
ind FA = ind Fa by A14, TOPDIM_1:29;
then A22: ind (FA \/ FB) <= 0 by A11, A15, A21, A17, A20, TOPDIM_1:13;
then TM | (A \/ B) is with_finite_small_inductive_dimension by A2, A17, A18, A21, A19, Th8;
then A23: A \/ B is with_finite_small_inductive_dimension by TOPDIM_1:18;
ind (TM | (A \/ B)) <= ((ind A) + 1) + (ind B) by A2, A17, A18, A21, A19, A22, Th8;
hence ( A \/ B is with_finite_small_inductive_dimension & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by A23, TOPDIM_1:17; :: thesis: verum