let n be Nat; :: thesis: for TM being metrizable TopSpace st TM is finite-ind holds
for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let TM be metrizable TopSpace; :: thesis: ( TM is finite-ind implies for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A1: TM is finite-ind ; :: thesis: for A being Subset of TM st ind (A `) <= n & TM | (A `) is second-countable holds
for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set cTM = [#] TM;
let A be Subset of TM; :: thesis: ( ind (A `) <= n & TM | (A `) is second-countable implies for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume that
A2: ind (A `) <= n and
A3: TM | (A `) is second-countable ; :: thesis: for A1, A2 being closed Subset of TM st A = A1 \/ A2 holds
ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
let A1, A2 be closed Subset of TM; :: thesis: ( A = A1 \/ A2 implies ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 ) )
assume A4: A = A1 \/ A2 ; :: thesis: ex X1, X2 being closed Subset of TM st
( [#] TM = X1 \/ X2 & A1 c= X1 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X1 /\ A2 & ind ((X1 /\ X2) \ (A1 /\ A2)) <= n - 1 )
set A12 = A1 /\ A2;
set T912 = TM | (([#] TM) \ (A1 /\ A2));
A5: [#] (TM | (([#] TM) \ (A1 /\ A2))) = ([#] TM) \ (A1 /\ A2) by PRE_TOPC:def 5;
A ` c= ([#] TM) \ (A1 /\ A2) by A4, XBOOLE_1:29, XBOOLE_1:34;
then reconsider A19 = A1 \ (A1 /\ A2), A29 = A2 \ (A1 /\ A2), A9 = A ` as Subset of (TM | (([#] TM) \ (A1 /\ A2))) by A5, XBOOLE_1:33;
A2 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A2 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A29 by XBOOLE_1:28 ;
then reconsider A29 = A29 as closed Subset of (TM | (([#] TM) \ (A1 /\ A2))) by PRE_TOPC:13;
A1 /\ ([#] (TM | (([#] TM) \ (A1 /\ A2)))) = (A1 /\ ([#] TM)) \ (A1 /\ A2) by A5, XBOOLE_1:49
.= A19 by XBOOLE_1:28 ;
then reconsider A19 = A19 as closed Subset of (TM | (([#] TM) \ (A1 /\ A2))) by PRE_TOPC:13;
A1 \ A2 = A19 by XBOOLE_1:47;
then A19 misses A2 by XBOOLE_1:79;
then A6: A19 misses A29 by XBOOLE_1:36, XBOOLE_1:63;
A7: ind (A `) = ind A9 by A1, TOPDIM_1:21;
(TM | (([#] TM) \ (A1 /\ A2))) | A9 is second-countable by A3, METRIZTS:9;
then consider L being Subset of (TM | (([#] TM) \ (A1 /\ A2))) such that
A8: L separates A19,A29 and
A9: ind (L /\ A9) <= n - 1 by A1, A2, A6, A7, Th11;
consider U, W being open Subset of (TM | (([#] TM) \ (A1 /\ A2))) such that
A10: A19 c= U and
A11: A29 c= W and
A12: U misses W and
A13: L = (U \/ W) ` by A8, METRIZTS:def 3;
[#] (TM | (([#] TM) \ (A1 /\ A2))) c= [#] TM by PRE_TOPC:def 4;
then reconsider L9 = L, U9 = U, W9 = W as Subset of TM by XBOOLE_1:1;
A14: ( A1 = (A1 \ (A1 /\ A2)) \/ (A1 /\ A2) & A2 = (A2 \ (A1 /\ A2)) \/ (A1 /\ A2) ) by XBOOLE_1:17, XBOOLE_1:45;
L misses A
proof
assume L meets A ; :: thesis: contradiction
then consider x being object such that
A15: x in L and
A16: x in A by XBOOLE_0:3;
A17: ( x in A1 or x in A2 ) by A4, A16, XBOOLE_0:def 3;
not x in A1 /\ A2 by A5, A15, XBOOLE_0:def 5;
then ( x in A19 or x in A29 ) by A17, XBOOLE_0:def 5;
then x in U \/ W by A10, A11, XBOOLE_0:def 3;
hence contradiction by A13, A15, XBOOLE_0:def 5; :: thesis: verum
end;
then A18: L = L9 \ A by XBOOLE_1:83
.= (L /\ ([#] TM)) \ A by XBOOLE_1:28
.= L /\ A9 by XBOOLE_1:49 ;
A19: ([#] TM) \ (([#] TM) \ (A1 /\ A2)) = ([#] TM) /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:28 ;
A20: A1 \ (A1 \ (A1 /\ A2)) = A1 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
(A1 /\ A2) ` is open ;
then reconsider U9 = U9, W9 = W9 as open Subset of TM by A5, TSEP_1:9;
take X2 = W9 ` ; :: thesis: ex X2 being closed Subset of TM st
( [#] TM = X2 \/ X2 & A1 c= X2 & A2 c= X2 & A1 /\ X2 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X2) \ (A1 /\ A2)) <= n - 1 )
take X1 = U9 ` ; :: thesis: ( [#] TM = X2 \/ X1 & A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A21: W9 c= X1 by A12, SUBSET_1:23;
A22: W \/ (([#] TM) \ (U \/ W)) = W \/ (X1 /\ X2) by XBOOLE_1:53
.= (W9 \/ X1) /\ (W \/ X2) by XBOOLE_1:24
.= (W9 \/ X1) /\ ([#] TM) by XBOOLE_1:45
.= X1 /\ ([#] TM) by A21, XBOOLE_1:12
.= X1 by XBOOLE_1:28 ;
thus X2 \/ X1 = ([#] TM) \ (U9 /\ W9) by XBOOLE_1:54
.= ([#] TM) \ {} by A12
.= [#] TM ; :: thesis: ( A1 c= X2 & A2 c= X1 & A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A23: U9 c= X2 by A12, SUBSET_1:23;
A24: U \/ (([#] TM) \ (U \/ W)) = U \/ (X1 /\ X2) by XBOOLE_1:53
.= (U9 \/ X1) /\ (U \/ X2) by XBOOLE_1:24
.= ([#] TM) /\ (U \/ X2) by XBOOLE_1:45
.= ([#] TM) /\ X2 by A23, XBOOLE_1:12
.= X2 by XBOOLE_1:28 ;
([#] TM) \ (([#] TM) \ (A1 /\ A2)) c= ([#] TM) \ (U \/ W) by A5, XBOOLE_1:34;
hence A25: ( A1 c= X2 & A2 c= X1 ) by A10, A11, A14, A19, A24, A22, XBOOLE_1:13; :: thesis: ( A1 /\ X1 = A1 /\ A2 & A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
then A26: A1 /\ A2 c= A1 /\ X1 by XBOOLE_1:26;
A1 /\ X1 = (([#] TM) /\ A1) \ U9 by XBOOLE_1:49
.= A1 \ U9 by XBOOLE_1:28 ;
then A1 /\ X1 c= A1 /\ A2 by A10, A20, XBOOLE_1:34;
hence A1 /\ X1 = A1 /\ A2 by A26; :: thesis: ( A1 /\ A2 = X2 /\ A2 & ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 )
A27: A2 \ (A2 \ (A1 /\ A2)) = A2 /\ (A1 /\ A2) by XBOOLE_1:48
.= A1 /\ A2 by XBOOLE_1:17, XBOOLE_1:28 ;
A28: A1 /\ A2 c= A2 /\ X2 by A25, XBOOLE_1:26;
A2 /\ X2 = (([#] TM) /\ A2) \ W9 by XBOOLE_1:49
.= A2 \ W9 by XBOOLE_1:28 ;
then A2 /\ X2 c= A1 /\ A2 by A11, A27, XBOOLE_1:34;
hence A1 /\ A2 = X2 /\ A2 by A28; :: thesis: ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1
(X2 /\ X1) \ (A1 /\ A2) = (([#] TM) \ (W9 \/ U9)) \ (A1 /\ A2) by XBOOLE_1:53
.= ([#] TM) \ ((W9 \/ U9) \/ (A1 /\ A2)) by XBOOLE_1:41
.= L by A5, A13, XBOOLE_1:41 ;
hence ind ((X2 /\ X1) \ (A1 /\ A2)) <= n - 1 by A1, A9, A18, TOPDIM_1:21; :: thesis: verum