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

.= (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

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

then A18: L =
L9 \ A
by XBOOLE_1:83
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 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

.= (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