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 )
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;