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;

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

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 )

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

then A18:
( AA \/ F is finite-ind & ind (AA \/ F) <= I )
by A5, TOPDIM_1:11;
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;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;

end;

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;hence ( D is finite-ind & ind D <= I ) by A3, TOPDIM_1:21; :: thesis: verum

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

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