let n be Nat; :: thesis: for T being metrizable TopSpace st T is second-countable holds

( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )

defpred S_{1}[ Nat] means for T being metrizable TopSpace st T is second-countable & T is finite-ind & ind T <= $1 holds

ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= $1 - 1 & ind B <= 0 );

defpred S_{2}[ Nat] means for T being metrizable TopSpace st T is second-countable & ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= $1 ) holds

( T is finite-ind & ind T <= $1 );

A1: for n being Nat st S_{2}[n] holds

S_{1}[n + 1]
_{2}[ 0 ]
by TOPDIM_1:36;

A22: for n being Nat st S_{2}[n] holds

S_{2}[n + 1]
_{2}[n]
from NAT_1:sch 2(A21, A22);

let T be metrizable TopSpace; :: thesis: ( T is second-countable implies ( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) ) )

assume A109: T is second-countable ; :: thesis: ( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )

thus ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) by A108, A109; :: thesis: ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) )

assume that

A110: T is finite-ind and

A111: ind T <= n ; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )

defpred S

ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= $1 - 1 & ind B <= 0 );

defpred S

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= $1 ) holds

( T is finite-ind & ind T <= $1 );

A1: for n being Nat st S

S

proof

A21:
S
defpred S_{3}[ set ] means verum;

let n be Nat; :: thesis: ( S_{2}[n] implies S_{1}[n + 1] )

assume A2: S_{2}[n]
; :: thesis: S_{1}[n + 1]

let T be metrizable TopSpace; :: thesis: ( T is second-countable & T is finite-ind & ind T <= n + 1 implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 ) )

assume that

A3: T is second-countable and

A4: T is finite-ind and

A5: ind T <= n + 1 ; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 )

consider B being Basis of T such that

A6: for A being Subset of T st A in B holds

( Fr A is finite-ind & ind (Fr A) <= (n + 1) - 1 ) by A4, A5, TOPDIM_1:31;

deffunc H_{1}( Subset of T) -> Element of bool the carrier of T = Fr $1;

consider uB being Basis of T such that

A7: uB c= B and

A8: uB is countable by A3, METRIZTS:24;

defpred S_{4}[ set ] means ( $1 in uB & S_{3}[$1] );

consider S being Subset-Family of T such that

A9: S = { H_{1}(b) where b is Subset of T : S_{4}[b] }
from LMOD_7:sch 5();

set uS = union S;

set TS = T | (union S);

A10: [#] (T | (union S)) = union S by PRE_TOPC:def 5;

then reconsider S9 = S as Subset-Family of (T | (union S)) by ZFMISC_1:82;

A11: T | ((union S) `) is second-countable by A3;

for a being Subset of (T | (union S)) st a in S9 holds

( a is finite-ind & ind a <= n )

A15: for p being Point of T

for U being open Subset of T st p in U holds

ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

( [#] T = (union S) \/ B & union S misses B & ind (union S) <= (n + 1) - 1 & ind B <= 0 )

take (union S) ` ; :: thesis: ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 )

A18: card { H_{1}(b) where b is Subset of T : ( b in uB & S_{3}[b] ) } c= card uB
from BORSUK_2:sch 1();

card uB c= omega by A8;

then card S c= omega by A9, A18;

then A19: S9 is countable ;

A20: S9 is closed

then ind (T | (union S)) <= n by A2, A3, A14, A19, A20;

hence ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 ) by A4, A11, A15, PRE_TOPC:2, SUBSET_1:23, TOPDIM_1:17, TOPDIM_1:38; :: thesis: verum

end;let n be Nat; :: thesis: ( S

assume A2: S

let T be metrizable TopSpace; :: thesis: ( T is second-countable & T is finite-ind & ind T <= n + 1 implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 ) )

assume that

A3: T is second-countable and

A4: T is finite-ind and

A5: ind T <= n + 1 ; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= (n + 1) - 1 & ind B <= 0 )

consider B being Basis of T such that

A6: for A being Subset of T st A in B holds

( Fr A is finite-ind & ind (Fr A) <= (n + 1) - 1 ) by A4, A5, TOPDIM_1:31;

deffunc H

consider uB being Basis of T such that

A7: uB c= B and

A8: uB is countable by A3, METRIZTS:24;

defpred S

consider S being Subset-Family of T such that

A9: S = { H

set uS = union S;

set TS = T | (union S);

A10: [#] (T | (union S)) = union S by PRE_TOPC:def 5;

then reconsider S9 = S as Subset-Family of (T | (union S)) by ZFMISC_1:82;

A11: T | ((union S) `) is second-countable by A3;

for a being Subset of (T | (union S)) st a in S9 holds

( a is finite-ind & ind a <= n )

proof

then A14:
( S9 is finite-ind & ind S9 <= n )
by TOPDIM_1:11;
let a be Subset of (T | (union S)); :: thesis: ( a in S9 implies ( a is finite-ind & ind a <= n ) )

assume a in S9 ; :: thesis: ( a is finite-ind & ind a <= n )

then consider b being Subset of T such that

A12: a = H_{1}(b)
and

A13: S_{4}[b]
by A9;

( Fr b is finite-ind & ind (Fr b) <= (n + 1) - 1 ) by A6, A7, A13;

hence ( a is finite-ind & ind a <= n ) by A12, TOPDIM_1:21; :: thesis: verum

end;assume a in S9 ; :: thesis: ( a is finite-ind & ind a <= n )

then consider b being Subset of T such that

A12: a = H

A13: S

( Fr b is finite-ind & ind (Fr b) <= (n + 1) - 1 ) by A6, A7, A13;

hence ( a is finite-ind & ind a <= n ) by A12, TOPDIM_1:21; :: thesis: verum

A15: for p being Point of T

for U being open Subset of T st p in U holds

ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

proof

take
union S
; :: thesis: ex B being Subset of T st
let p be Point of T; :: thesis: for U being open Subset of T st p in U holds

ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

let U be open Subset of T; :: thesis: ( p in U implies ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W ) )

assume p in U ; :: thesis: ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

then consider a being Subset of T such that

A16: a in uB and

A17: ( p in a & a c= U ) by YELLOW_9:31;

uB c= the topology of T by TOPS_2:64;

then reconsider a = a as open Subset of T by A16, PRE_TOPC:def 2;

take a ; :: thesis: ( p in a & a c= U & (union S) ` misses Fr a )

H_{1}(a) in S
by A9, A16;

then H_{1}(a) c= union S
by ZFMISC_1:74;

hence ( p in a & a c= U & (union S) ` misses Fr a ) by A17, SUBSET_1:24; :: thesis: verum

end;ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

let U be open Subset of T; :: thesis: ( p in U implies ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W ) )

assume p in U ; :: thesis: ex W being open Subset of T st

( p in W & W c= U & (union S) ` misses Fr W )

then consider a being Subset of T such that

A16: a in uB and

A17: ( p in a & a c= U ) by YELLOW_9:31;

uB c= the topology of T by TOPS_2:64;

then reconsider a = a as open Subset of T by A16, PRE_TOPC:def 2;

take a ; :: thesis: ( p in a & a c= U & (union S) ` misses Fr a )

H

then H

hence ( p in a & a c= U & (union S) ` misses Fr a ) by A17, SUBSET_1:24; :: thesis: verum

( [#] T = (union S) \/ B & union S misses B & ind (union S) <= (n + 1) - 1 & ind B <= 0 )

take (union S) ` ; :: thesis: ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 )

A18: card { H

card uB c= omega by A8;

then card S c= omega by A9, A18;

then A19: S9 is countable ;

A20: S9 is closed

proof

S9 is Cover of (T | (union S))
by A10, SETFAM_1:def 11;
let a be Subset of (T | (union S)); :: according to TOPS_2:def 2 :: thesis: ( not a in S9 or a is closed )

assume a in S9 ; :: thesis: a is closed

then ex b being Subset of T st

( a = H_{1}(b) & S_{4}[b] )
by A9;

hence a is closed by TSEP_1:8; :: thesis: verum

end;assume a in S9 ; :: thesis: a is closed

then ex b being Subset of T st

( a = H

hence a is closed by TSEP_1:8; :: thesis: verum

then ind (T | (union S)) <= n by A2, A3, A14, A19, A20;

hence ( [#] T = (union S) \/ ((union S) `) & union S misses (union S) ` & ind (union S) <= (n + 1) - 1 & ind ((union S) `) <= 0 ) by A4, A11, A15, PRE_TOPC:2, SUBSET_1:23, TOPDIM_1:17, TOPDIM_1:38; :: thesis: verum

A22: for n being Nat st S

S

proof

A108:
for n being Nat holds S
let n be Nat; :: thesis: ( S_{2}[n] implies S_{2}[n + 1] )

assume A23: S_{2}[n]
; :: thesis: S_{2}[n + 1]

let T be metrizable TopSpace; :: thesis: ( T is second-countable & ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n + 1 ) implies ( T is finite-ind & ind T <= n + 1 ) )

assume A24: T is second-countable ; :: thesis: ( for F being Subset-Family of T holds

( not F is closed or not F is Cover of T or not F is countable or not F is finite-ind or not ind F <= n + 1 ) or ( T is finite-ind & ind T <= n + 1 ) )

given F being Subset-Family of T such that A25: F is closed and

A26: F is Cover of T and

A27: F is countable and

A28: ( F is finite-ind & ind F <= n + 1 ) ; :: thesis: ( T is finite-ind & ind T <= n + 1 )

end;assume A23: S

let T be metrizable TopSpace; :: thesis: ( T is second-countable & ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n + 1 ) implies ( T is finite-ind & ind T <= n + 1 ) )

assume A24: T is second-countable ; :: thesis: ( for F being Subset-Family of T holds

( not F is closed or not F is Cover of T or not F is countable or not F is finite-ind or not ind F <= n + 1 ) or ( T is finite-ind & ind T <= n + 1 ) )

given F being Subset-Family of T such that A25: F is closed and

A26: F is Cover of T and

A27: F is countable and

A28: ( F is finite-ind & ind F <= n + 1 ) ; :: thesis: ( T is finite-ind & ind T <= n + 1 )

per cases
( T is empty or not T is empty )
;

end;

suppose A29:
not T is empty
; :: thesis: ( T is finite-ind & ind T <= n + 1 )

set cT = the carrier of T;

A30: not F is empty by A26, A29, SETFAM_1:45, ZFMISC_1:2;

then consider f being sequence of F such that

A31: rng f = F by A27, CARD_3:96;

dom f = NAT by A30, FUNCT_2:def 1;

then reconsider f = f as SetSequence of T by A31, FUNCT_2:2;

consider g being SetSequence of T such that

A32: union (rng f) = union (rng g) and

A33: for i, j being Nat st i <> j holds

g . i misses g . j and

A34: for n being Nat ex fn being finite Subset-Family of T st

( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) by TOPDIM_1:33;

defpred S_{3}[ object , object ] means for i being Nat

for A, B being Subset of T st $1 = i & $2 = [A,B] holds

( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 );

A35: for x being object st x in NAT holds

ex y being object st

( y in [:(bool the carrier of T),(bool the carrier of T):] & S_{3}[x,y] )

A49: for x being object st x in NAT holds

S_{3}[x,P12 . x]
from FUNCT_2:sch 1(A35);

set P1 = pr1 P12;

set P2 = pr2 P12;

set U1 = Union (pr1 P12);

set U2 = Union (pr2 P12);

set Tu1 = T | (Union (pr1 P12));

set Tu2 = T | (Union (pr2 P12));

reconsider Tu1 = T | (Union (pr1 P12)) as metrizable TopSpace ;

A50: dom (pr1 P12) = NAT by FUNCT_2:def 1;

A51: [#] Tu1 = Union (pr1 P12) by PRE_TOPC:def 5;

then reconsider P1 = pr1 P12 as SetSequence of Tu1 by A50, FUNCT_2:2, ZFMISC_1:82;

reconsider Tu2 = T | (Union (pr2 P12)) as metrizable TopSpace ;

A52: dom (pr2 P12) = NAT by FUNCT_2:def 1;

A53: for i being Nat holds g . i is F_sigma

( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )

A73: ( G1 is closed & G1 is finite-ind & ind G1 <= n & G1 is countable ) and

A74: Union P1 = union G1 by Lm2;

A75: G1 is Cover of Tu1 by A51, A74, SETFAM_1:def 11;

then A76: Tu1 is finite-ind by A23, A24, A73;

then A77: Union (pr1 P12) is finite-ind by TOPDIM_1:18;

A78: [#] Tu2 = Union (pr2 P12) by PRE_TOPC:def 5;

then reconsider P2 = pr2 P12 as SetSequence of Tu2 by A52, FUNCT_2:2, ZFMISC_1:82;

for i being Nat holds

( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma )

A93: ( G2 is closed & G2 is finite-ind & ind G2 <= 0 & G2 is countable ) and

A94: Union P2 = union G2 by Lm2;

A95: G2 is Cover of Tu2 by A78, A94, SETFAM_1:def 11;

then Tu2 is finite-ind by A23, A24, A93;

then A96: Union (pr2 P12) is finite-ind by TOPDIM_1:18;

ind Tu1 <= n by A23, A24, A73, A75;

then ind (Union (pr1 P12)) <= n by A77, TOPDIM_1:17;

then A97: (ind (Union (pr1 P12))) + 1 <= n + 1 by XREAL_1:6;

A98: Union (pr1 P12) is finite-ind by A76, TOPDIM_1:18;

[#] T c= (Union (pr1 P12)) \/ (Union (pr2 P12))

ind Tu2 <= 0 by A24, A93, A95, TOPDIM_1:36;

then A107: ind (Union (pr2 P12)) <= 0 by A96, TOPDIM_1:17;

T | (Union (pr2 P12)) is second-countable by A24;

then ( (Union (pr1 P12)) \/ (Union (pr2 P12)) is finite-ind & ind ((Union (pr1 P12)) \/ (Union (pr2 P12))) <= (ind (Union (pr1 P12))) + 1 ) by A96, A107, A98, TOPDIM_1:40;

hence ( T is finite-ind & ind T <= n + 1 ) by A106, A97, XXREAL_0:2; :: thesis: verum

end;A30: not F is empty by A26, A29, SETFAM_1:45, ZFMISC_1:2;

then consider f being sequence of F such that

A31: rng f = F by A27, CARD_3:96;

dom f = NAT by A30, FUNCT_2:def 1;

then reconsider f = f as SetSequence of T by A31, FUNCT_2:2;

consider g being SetSequence of T such that

A32: union (rng f) = union (rng g) and

A33: for i, j being Nat st i <> j holds

g . i misses g . j and

A34: for n being Nat ex fn being finite Subset-Family of T st

( fn = { (f . i) where i is Element of NAT : i < n } & g . n = (f . n) \ (union fn) ) by TOPDIM_1:33;

defpred S

for A, B being Subset of T st $1 = i & $2 = [A,B] holds

( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 );

A35: for x being object st x in NAT holds

ex y being object st

( y in [:(bool the carrier of T),(bool the carrier of T):] & S

proof

consider P12 being sequence of [:(bool the carrier of T),(bool the carrier of T):] such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st

( y in [:(bool the carrier of T),(bool the carrier of T):] & S_{3}[x,y] ) )

assume x in NAT ; :: thesis: ex y being object st

( y in [:(bool the carrier of T),(bool the carrier of T):] & S_{3}[x,y] )

then reconsider N = x as Element of NAT ;

reconsider gN = g . N as Subset of T ;

dom f = NAT by FUNCT_2:def 1;

then A36: f . N in F by A31, FUNCT_1:def 3;

then A37: f . N is finite-ind by A28;

ex fn being finite Subset-Family of T st

( fn = { (f . i) where i is Element of NAT : i < N } & g . N = (f . N) \ (union fn) ) by A34;

then A38: g . N c= f . N by XBOOLE_1:36;

then A39: g . N is finite-ind by A37, TOPDIM_1:19;

A40: ind (g . N) <= ind (f . N) by A37, A38, TOPDIM_1:19;

ind (f . N) <= n + 1 by A28, A36, TOPDIM_1:11;

then A41: ind (g . N) <= n + 1 by A40, XXREAL_0:2;

ind (T | gN) = ind gN by A39, TOPDIM_1:17;

then consider A, B being Subset of (T | gN) such that

A42: A \/ B = [#] (T | gN) and

A misses B and

A43: ( ind A <= (n + 1) - 1 & ind B <= 0 ) by A1, A23, A24, A39, A41;

A44: A is finite-ind by A39;

[#] (T | gN) = gN by PRE_TOPC:def 5;

then reconsider A9 = A, B9 = B as Subset of T by XBOOLE_1:1;

B is finite-ind by A39;

then A45: ( B9 is finite-ind & ind B9 = ind B ) by TOPDIM_1:22;

take y = [A9,B9]; :: thesis: ( y in [:(bool the carrier of T),(bool the carrier of T):] & S_{3}[x,y] )

thus y in [:(bool the carrier of T),(bool the carrier of T):] ; :: thesis: S_{3}[x,y]

let i be Nat; :: thesis: for A, B being Subset of T st x = i & y = [A,B] holds

( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 )

let a, b be Subset of T; :: thesis: ( x = i & y = [a,b] implies ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) )

assume that

A46: x = i and

A47: y = [a,b] ; :: thesis: ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 )

A48: a = A9 by A47, XTUPLE_0:1;

A9 \/ B9 = g . i by A42, A46, PRE_TOPC:def 5;

hence ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) by A43, A44, A45, A47, A48, TOPDIM_1:22, XTUPLE_0:1; :: thesis: verum

end;( y in [:(bool the carrier of T),(bool the carrier of T):] & S

assume x in NAT ; :: thesis: ex y being object st

( y in [:(bool the carrier of T),(bool the carrier of T):] & S

then reconsider N = x as Element of NAT ;

reconsider gN = g . N as Subset of T ;

dom f = NAT by FUNCT_2:def 1;

then A36: f . N in F by A31, FUNCT_1:def 3;

then A37: f . N is finite-ind by A28;

ex fn being finite Subset-Family of T st

( fn = { (f . i) where i is Element of NAT : i < N } & g . N = (f . N) \ (union fn) ) by A34;

then A38: g . N c= f . N by XBOOLE_1:36;

then A39: g . N is finite-ind by A37, TOPDIM_1:19;

A40: ind (g . N) <= ind (f . N) by A37, A38, TOPDIM_1:19;

ind (f . N) <= n + 1 by A28, A36, TOPDIM_1:11;

then A41: ind (g . N) <= n + 1 by A40, XXREAL_0:2;

ind (T | gN) = ind gN by A39, TOPDIM_1:17;

then consider A, B being Subset of (T | gN) such that

A42: A \/ B = [#] (T | gN) and

A misses B and

A43: ( ind A <= (n + 1) - 1 & ind B <= 0 ) by A1, A23, A24, A39, A41;

A44: A is finite-ind by A39;

[#] (T | gN) = gN by PRE_TOPC:def 5;

then reconsider A9 = A, B9 = B as Subset of T by XBOOLE_1:1;

B is finite-ind by A39;

then A45: ( B9 is finite-ind & ind B9 = ind B ) by TOPDIM_1:22;

take y = [A9,B9]; :: thesis: ( y in [:(bool the carrier of T),(bool the carrier of T):] & S

thus y in [:(bool the carrier of T),(bool the carrier of T):] ; :: thesis: S

let i be Nat; :: thesis: for A, B being Subset of T st x = i & y = [A,B] holds

( A \/ B = g . i & A is finite-ind & B is finite-ind & ind A <= n & ind B <= 0 )

let a, b be Subset of T; :: thesis: ( x = i & y = [a,b] implies ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) )

assume that

A46: x = i and

A47: y = [a,b] ; :: thesis: ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 )

A48: a = A9 by A47, XTUPLE_0:1;

A9 \/ B9 = g . i by A42, A46, PRE_TOPC:def 5;

hence ( a \/ b = g . i & a is finite-ind & b is finite-ind & ind a <= n & ind b <= 0 ) by A43, A44, A45, A47, A48, TOPDIM_1:22, XTUPLE_0:1; :: thesis: verum

A49: for x being object st x in NAT holds

S

set P1 = pr1 P12;

set P2 = pr2 P12;

set U1 = Union (pr1 P12);

set U2 = Union (pr2 P12);

set Tu1 = T | (Union (pr1 P12));

set Tu2 = T | (Union (pr2 P12));

reconsider Tu1 = T | (Union (pr1 P12)) as metrizable TopSpace ;

A50: dom (pr1 P12) = NAT by FUNCT_2:def 1;

A51: [#] Tu1 = Union (pr1 P12) by PRE_TOPC:def 5;

then reconsider P1 = pr1 P12 as SetSequence of Tu1 by A50, FUNCT_2:2, ZFMISC_1:82;

reconsider Tu2 = T | (Union (pr2 P12)) as metrizable TopSpace ;

A52: dom (pr2 P12) = NAT by FUNCT_2:def 1;

A53: for i being Nat holds g . i is F_sigma

proof

for i being Nat holds
let i be Nat; :: thesis: g . i is F_sigma

consider fi being finite Subset-Family of T such that

A54: fi = { (f . j) where j is Element of NAT : j < i } and

A55: g . i = (f . i) \ (union fi) by A34;

fi is closed

( dom f = NAT & i in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;

then f . i in F by A31, FUNCT_1:def 3;

then f . i is closed by A25;

then A58: f . i is F_sigma by A29, TOPGEN_4:43;

((union fi) `) /\ (f . i) = (([#] T) /\ (f . i)) \ (union fi) by XBOOLE_1:49

.= g . i by A55, XBOOLE_1:28 ;

hence g . i is F_sigma by A29, A57, A58, TOPGEN_4:39; :: thesis: verum

end;consider fi being finite Subset-Family of T such that

A54: fi = { (f . j) where j is Element of NAT : j < i } and

A55: g . i = (f . i) \ (union fi) by A34;

fi is closed

proof

then A57:
union fi is closed
by TOPS_2:21;
let A be Subset of T; :: according to TOPS_2:def 2 :: thesis: ( not A in fi or A is closed )

assume A in fi ; :: thesis: A is closed

then A56: ex j being Element of NAT st

( A = f . j & j < i ) by A54;

dom f = NAT by FUNCT_2:def 1;

then A in F by A31, A56, FUNCT_1:def 3;

hence A is closed by A25; :: thesis: verum

end;assume A in fi ; :: thesis: A is closed

then A56: ex j being Element of NAT st

( A = f . j & j < i ) by A54;

dom f = NAT by FUNCT_2:def 1;

then A in F by A31, A56, FUNCT_1:def 3;

hence A is closed by A25; :: thesis: verum

( dom f = NAT & i in NAT ) by FUNCT_2:def 1, ORDINAL1:def 12;

then f . i in F by A31, FUNCT_1:def 3;

then f . i is closed by A25;

then A58: f . i is F_sigma by A29, TOPGEN_4:43;

((union fi) `) /\ (f . i) = (([#] T) /\ (f . i)) \ (union fi) by XBOOLE_1:49

.= g . i by A55, XBOOLE_1:28 ;

hence g . i is F_sigma by A29, A57, A58, TOPGEN_4:39; :: thesis: verum

( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )

proof

then consider G1 being Subset-Family of Tu1 such that
let i be Nat; :: thesis: ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )

consider y1, y2 being object such that

A59: y1 in bool the carrier of T and

A60: y2 in bool the carrier of T and

A61: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1 as Subset of T by A59;

reconsider y2 = y2 as set by TARSKI:1;

A62: i in NAT by ORDINAL1:def 12;

then A63: ( y1 is finite-ind & ind y1 <= n ) by A49, A60, A61;

( [y1,y2] `1 = y1 & dom P12 = NAT ) by FUNCT_2:def 1;

then A64: y1 = P1 . i by A61, A62, MCART_1:def 12;

A65: (Union (pr1 P12)) /\ (g . i) c= P1 . i

then P1 . i c= g . i by A64, XBOOLE_1:7;

then P1 . i c= (Union (pr1 P12)) /\ (g . i) by A51, XBOOLE_1:19;

then ( P1 . i = (Union (pr1 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A65;

hence ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma ) by A63, A64, METRIZTS:10, TOPDIM_1:21; :: thesis: verum

end;consider y1, y2 being object such that

A59: y1 in bool the carrier of T and

A60: y2 in bool the carrier of T and

A61: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1 as Subset of T by A59;

reconsider y2 = y2 as set by TARSKI:1;

A62: i in NAT by ORDINAL1:def 12;

then A63: ( y1 is finite-ind & ind y1 <= n ) by A49, A60, A61;

( [y1,y2] `1 = y1 & dom P12 = NAT ) by FUNCT_2:def 1;

then A64: y1 = P1 . i by A61, A62, MCART_1:def 12;

A65: (Union (pr1 P12)) /\ (g . i) c= P1 . i

proof

y1 \/ y2 = g . i
by A49, A60, A61, A62;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union (pr1 P12)) /\ (g . i) or x in P1 . i )

assume A66: x in (Union (pr1 P12)) /\ (g . i) ; :: thesis: x in P1 . i

then A67: x in g . i by XBOOLE_0:def 4;

x in Union (pr1 P12) by A66, XBOOLE_0:def 4;

then consider j being Nat such that

A68: x in P1 . j by PROB_1:12;

consider z1, z2 being object such that

A69: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and

A70: P12 . j = [z1,z2] by ZFMISC_1:def 2;

A71: j in NAT by ORDINAL1:def 12;

reconsider z1 = z1, z2 = z2 as set by TARSKI:1;

( [z1,z2] `1 = z1 & dom P12 = NAT ) by FUNCT_2:def 1;

then A72: z1 = P1 . j by A70, MCART_1:def 12, A71;

z1 \/ z2 = g . j by A49, A69, A70, A71;

then x in g . j by A68, A72, XBOOLE_0:def 3;

then g . i meets g . j by A67, XBOOLE_0:3;

hence x in P1 . i by A33, A68; :: thesis: verum

end;assume A66: x in (Union (pr1 P12)) /\ (g . i) ; :: thesis: x in P1 . i

then A67: x in g . i by XBOOLE_0:def 4;

x in Union (pr1 P12) by A66, XBOOLE_0:def 4;

then consider j being Nat such that

A68: x in P1 . j by PROB_1:12;

consider z1, z2 being object such that

A69: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and

A70: P12 . j = [z1,z2] by ZFMISC_1:def 2;

A71: j in NAT by ORDINAL1:def 12;

reconsider z1 = z1, z2 = z2 as set by TARSKI:1;

( [z1,z2] `1 = z1 & dom P12 = NAT ) by FUNCT_2:def 1;

then A72: z1 = P1 . j by A70, MCART_1:def 12, A71;

z1 \/ z2 = g . j by A49, A69, A70, A71;

then x in g . j by A68, A72, XBOOLE_0:def 3;

then g . i meets g . j by A67, XBOOLE_0:3;

hence x in P1 . i by A33, A68; :: thesis: verum

then P1 . i c= g . i by A64, XBOOLE_1:7;

then P1 . i c= (Union (pr1 P12)) /\ (g . i) by A51, XBOOLE_1:19;

then ( P1 . i = (Union (pr1 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A65;

hence ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma ) by A63, A64, METRIZTS:10, TOPDIM_1:21; :: thesis: verum

A73: ( G1 is closed & G1 is finite-ind & ind G1 <= n & G1 is countable ) and

A74: Union P1 = union G1 by Lm2;

A75: G1 is Cover of Tu1 by A51, A74, SETFAM_1:def 11;

then A76: Tu1 is finite-ind by A23, A24, A73;

then A77: Union (pr1 P12) is finite-ind by TOPDIM_1:18;

A78: [#] Tu2 = Union (pr2 P12) by PRE_TOPC:def 5;

then reconsider P2 = pr2 P12 as SetSequence of Tu2 by A52, FUNCT_2:2, ZFMISC_1:82;

for i being Nat holds

( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma )

proof

then consider G2 being Subset-Family of Tu2 such that
let i be Nat; :: thesis: ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma )

consider y1, y2 being object such that

A79: y1 in bool the carrier of T and

A80: y2 in bool the carrier of T and

A81: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y2 = y2 as Subset of T by A80;

reconsider y1 = y1 as set by TARSKI:1;

A82: i in NAT by ORDINAL1:def 12;

then A83: ( y2 is finite-ind & ind y2 <= 0 ) by A49, A79, A81;

( [y1,y2] `2 = y2 & dom P12 = NAT ) by FUNCT_2:def 1;

then A84: y2 = P2 . i by A81, A82, MCART_1:def 13;

A85: (Union (pr2 P12)) /\ (g . i) c= P2 . i

then P2 . i c= g . i by A84, XBOOLE_1:7;

then P2 . i c= (Union (pr2 P12)) /\ (g . i) by A78, XBOOLE_1:19;

then ( P2 . i = (Union (pr2 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A85;

hence ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma ) by A83, A84, METRIZTS:10, TOPDIM_1:21; :: thesis: verum

end;consider y1, y2 being object such that

A79: y1 in bool the carrier of T and

A80: y2 in bool the carrier of T and

A81: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y2 = y2 as Subset of T by A80;

reconsider y1 = y1 as set by TARSKI:1;

A82: i in NAT by ORDINAL1:def 12;

then A83: ( y2 is finite-ind & ind y2 <= 0 ) by A49, A79, A81;

( [y1,y2] `2 = y2 & dom P12 = NAT ) by FUNCT_2:def 1;

then A84: y2 = P2 . i by A81, A82, MCART_1:def 13;

A85: (Union (pr2 P12)) /\ (g . i) c= P2 . i

proof

y1 \/ y2 = g . i
by A49, A79, A81, A82;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in (Union (pr2 P12)) /\ (g . i) or x in P2 . i )

assume A86: x in (Union (pr2 P12)) /\ (g . i) ; :: thesis: x in P2 . i

then A87: x in g . i by XBOOLE_0:def 4;

x in Union (pr2 P12) by A86, XBOOLE_0:def 4;

then consider j being Nat such that

A88: x in P2 . j by PROB_1:12;

consider z1, z2 being object such that

A89: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and

A90: P12 . j = [z1,z2] by ZFMISC_1:def 2;

A91: j in NAT by ORDINAL1:def 12;

reconsider z1 = z1, z2 = z2 as set by TARSKI:1;

( [z1,z2] `2 = z2 & dom P12 = NAT ) by FUNCT_2:def 1;

then A92: z2 = P2 . j by A90, MCART_1:def 13, A91;

z1 \/ z2 = g . j by A49, A89, A90, A91;

then x in g . j by A88, A92, XBOOLE_0:def 3;

then g . i meets g . j by A87, XBOOLE_0:3;

hence x in P2 . i by A33, A88; :: thesis: verum

end;assume A86: x in (Union (pr2 P12)) /\ (g . i) ; :: thesis: x in P2 . i

then A87: x in g . i by XBOOLE_0:def 4;

x in Union (pr2 P12) by A86, XBOOLE_0:def 4;

then consider j being Nat such that

A88: x in P2 . j by PROB_1:12;

consider z1, z2 being object such that

A89: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and

A90: P12 . j = [z1,z2] by ZFMISC_1:def 2;

A91: j in NAT by ORDINAL1:def 12;

reconsider z1 = z1, z2 = z2 as set by TARSKI:1;

( [z1,z2] `2 = z2 & dom P12 = NAT ) by FUNCT_2:def 1;

then A92: z2 = P2 . j by A90, MCART_1:def 13, A91;

z1 \/ z2 = g . j by A49, A89, A90, A91;

then x in g . j by A88, A92, XBOOLE_0:def 3;

then g . i meets g . j by A87, XBOOLE_0:3;

hence x in P2 . i by A33, A88; :: thesis: verum

then P2 . i c= g . i by A84, XBOOLE_1:7;

then P2 . i c= (Union (pr2 P12)) /\ (g . i) by A78, XBOOLE_1:19;

then ( P2 . i = (Union (pr2 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A85;

hence ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma ) by A83, A84, METRIZTS:10, TOPDIM_1:21; :: thesis: verum

A93: ( G2 is closed & G2 is finite-ind & ind G2 <= 0 & G2 is countable ) and

A94: Union P2 = union G2 by Lm2;

A95: G2 is Cover of Tu2 by A78, A94, SETFAM_1:def 11;

then Tu2 is finite-ind by A23, A24, A93;

then A96: Union (pr2 P12) is finite-ind by TOPDIM_1:18;

ind Tu1 <= n by A23, A24, A73, A75;

then ind (Union (pr1 P12)) <= n by A77, TOPDIM_1:17;

then A97: (ind (Union (pr1 P12))) + 1 <= n + 1 by XREAL_1:6;

A98: Union (pr1 P12) is finite-ind by A76, TOPDIM_1:18;

[#] T c= (Union (pr1 P12)) \/ (Union (pr2 P12))

proof

then A106:
(Union (pr1 P12)) \/ (Union (pr2 P12)) = [#] T
;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in [#] T or x in (Union (pr1 P12)) \/ (Union (pr2 P12)) )

A99: dom P12 = NAT by FUNCT_2:def 1;

assume x in [#] T ; :: thesis: x in (Union (pr1 P12)) \/ (Union (pr2 P12))

then x in Union g by A26, A31, A32, SETFAM_1:45;

then consider i being Nat such that

A100: x in g . i by PROB_1:12;

consider y1, y2 being object such that

A101: ( y1 in bool the carrier of T & y2 in bool the carrier of T ) and

A102: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as set by TARSKI:1;

A103: i in NAT by ORDINAL1:def 12;

[y1,y2] `1 = y1 ;

then A104: y1 = P1 . i by A99, A102, MCART_1:def 12, A103;

[y1,y2] `2 = y2 ;

then A105: y2 = P2 . i by A99, A102, MCART_1:def 13, A103;

y1 \/ y2 = g . i by A49, A101, A102, A103;

then ( x in P1 . i or x in P2 . i ) by A100, A104, A105, XBOOLE_0:def 3;

then ( x in Union (pr1 P12) or x in Union (pr2 P12) ) by PROB_1:12;

hence x in (Union (pr1 P12)) \/ (Union (pr2 P12)) by XBOOLE_0:def 3; :: thesis: verum

end;A99: dom P12 = NAT by FUNCT_2:def 1;

assume x in [#] T ; :: thesis: x in (Union (pr1 P12)) \/ (Union (pr2 P12))

then x in Union g by A26, A31, A32, SETFAM_1:45;

then consider i being Nat such that

A100: x in g . i by PROB_1:12;

consider y1, y2 being object such that

A101: ( y1 in bool the carrier of T & y2 in bool the carrier of T ) and

A102: P12 . i = [y1,y2] by ZFMISC_1:def 2;

reconsider y1 = y1, y2 = y2 as set by TARSKI:1;

A103: i in NAT by ORDINAL1:def 12;

[y1,y2] `1 = y1 ;

then A104: y1 = P1 . i by A99, A102, MCART_1:def 12, A103;

[y1,y2] `2 = y2 ;

then A105: y2 = P2 . i by A99, A102, MCART_1:def 13, A103;

y1 \/ y2 = g . i by A49, A101, A102, A103;

then ( x in P1 . i or x in P2 . i ) by A100, A104, A105, XBOOLE_0:def 3;

then ( x in Union (pr1 P12) or x in Union (pr2 P12) ) by PROB_1:12;

hence x in (Union (pr1 P12)) \/ (Union (pr2 P12)) by XBOOLE_0:def 3; :: thesis: verum

ind Tu2 <= 0 by A24, A93, A95, TOPDIM_1:36;

then A107: ind (Union (pr2 P12)) <= 0 by A96, TOPDIM_1:17;

T | (Union (pr2 P12)) is second-countable by A24;

then ( (Union (pr1 P12)) \/ (Union (pr2 P12)) is finite-ind & ind ((Union (pr1 P12)) \/ (Union (pr2 P12))) <= (ind (Union (pr1 P12))) + 1 ) by A96, A107, A98, TOPDIM_1:40;

hence ( T is finite-ind & ind T <= n + 1 ) by A106, A97, XXREAL_0:2; :: thesis: verum

let T be metrizable TopSpace; :: thesis: ( T is second-countable implies ( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) ) )

assume A109: T is second-countable ; :: thesis: ( ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) & ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) ) )

thus ( ex F being Subset-Family of T st

( F is closed & F is Cover of T & F is countable & F is finite-ind & ind F <= n ) implies ( T is finite-ind & ind T <= n ) ) by A108, A109; :: thesis: ( T is finite-ind & ind T <= n implies ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) )

assume that

A110: T is finite-ind and

A111: ind T <= n ; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

per cases
( n = 0 or n > 0 )
;

end;

suppose A112:
n = 0
; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

take
{} T
; :: thesis: ex B being Subset of T st

( [#] T = ({} T) \/ B & {} T misses B & ind ({} T) <= n - 1 & ind B <= 0 )

take [#] T ; :: thesis: ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 )

thus ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 ) by A111, A112, TOPDIM_1:6; :: thesis: verum

end;( [#] T = ({} T) \/ B & {} T misses B & ind ({} T) <= n - 1 & ind B <= 0 )

take [#] T ; :: thesis: ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 )

thus ( [#] T = ({} T) \/ ([#] T) & {} T misses [#] T & ind ({} T) <= n - 1 & ind ([#] T) <= 0 ) by A111, A112, TOPDIM_1:6; :: thesis: verum

suppose
n > 0
; :: thesis: ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 )

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;

( S_{2}[n1] & n1 + 1 = n )
by A108;

hence ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by A1, A109, A110, A111; :: thesis: verum

end;( S

hence ex A, B being Subset of T st

( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by A1, A109, A110, A111; :: thesis: verum