let TM be metrizable TopSpace; :: thesis: for I being Integer
for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
let I be Integer; :: thesis: for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds
( ind (A \/ B) <= I & A \/ B is finite-ind )
let A, B be finite-ind Subset of TM; :: thesis: ( A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I implies ( ind (A \/ B) <= I & A \/ B is finite-ind ) )
assume that
A1: A is closed and
A2: TM | (A \/ B) is second-countable and
A3: ind A <= I and
A4: ind B <= I ; :: thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )
- 1 <= ind A by TOPDIM_1:5;
then A5: - 1 <= I by A3, XXREAL_0:2;

per cases ( A \/ B is empty or not A \/ B is empty ) ;

suppose A \/ B is empty ; :: thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )

hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A5, TOPDIM_1:6; :: thesis: verum

end;

suppose A6: not A \/ B is empty ; :: thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind )

then A7: not TM is empty ;
( not A is empty or not B is empty ) by A6;
then ( 0 <= ind A or 0 <= ind B ) by A7;
then A8: I in NAT by A3, A4, INT_1:3;
reconsider AB = A \/ B as Subset of TM ;
set Tab = TM | AB;
A9: [#] (TM | AB) = AB by PRE_TOPC:def 5;
then reconsider a = A, b = B as Subset of (TM | AB) by XBOOLE_1:7;
A /\ ([#] (TM | AB)) = a by XBOOLE_1:28;
then A10: a is closed by A1, TSP_1:def 2;
then consider F being closed countable Subset-Family of (TM | AB) such that
A11: a ` = union F by TOPGEN_4:def 6;
reconsider a = a, b = b as finite-ind Subset of (TM | AB) by TOPDIM_1:21;
reconsider AA = {a} as Subset-Family of (TM | AB) ;
union (AA \/ F) = (union AA) \/ (union F) by ZFMISC_1:78
.= a \/ (a `) by A11, ZFMISC_1:25
.= [#] (TM | AB) by PRE_TOPC:2 ;
then A12: AA \/ F is Cover of (TM | AB) by SETFAM_1:def 11;
AA is closed by A10, TARSKI:def 1;
then A13: AA \/ F is closed by TOPS_2:16;
for D being Subset of (TM | AB) st D in AA \/ F holds
( D is finite-ind & ind D <= I )

proof

let D be Subset of (TM | AB); :: thesis: ( D in AA \/ F implies ( D is finite-ind & ind D <= I ) )
assume A14: D in AA \/ F ; :: thesis: ( D is finite-ind & ind D <= I )

per cases ( D in AA or D in F ) by A14, XBOOLE_0:def 3;

suppose D in AA ; :: thesis: ( D is finite-ind & ind D <= I )

then D = a by TARSKI:def 1;
hence ( D is finite-ind & ind D <= I ) by A3, TOPDIM_1:21; :: thesis: verum

end;

suppose A15: D in F ; :: thesis: ( D is finite-ind & ind D <= I )

a ` = b \ a by A9, XBOOLE_1:40;
then A16: a ` c= b by XBOOLE_1:36;
D c= a ` by A11, A15, ZFMISC_1:74;
then A17: D c= b by A16;
then ( ind b = ind B & ind D <= ind b ) by TOPDIM_1:19, TOPDIM_1:21;
hence ( D is finite-ind & ind D <= I ) by A4, A17, TOPDIM_1:19, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then A18: ( AA \/ F is finite-ind & ind (AA \/ F) <= I ) by A5, TOPDIM_1:11;
A19: AA \/ F is countable by CARD_2:85;
then TM | AB is finite-ind by A2, A8, A12, A13, A18, Lm3;
then A20: A \/ B is finite-ind by TOPDIM_1:18;
ind (TM | AB) <= I by A2, A8, A12, A13, A18, A19, Lm3;
hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A20, TOPDIM_1:17; :: thesis: verum

end;

end;