let n be Nat; :: thesis:
defpred S₁[ 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₂[ 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₂[n] holds
S₁[n + 1]

proof

defpred S₃[ set ] means verum;
let n be Nat; :: thesis:
assume A2: S₂[n] ; :: thesis:
let T be metrizable TopSpace; :: thesis:
assume that
A3: T is second-countable and
A4: T is finite-ind and
A5: ind T <= n + 1 ; :: thesis:
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₁( 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₄[ set ] means ( $1 in uB & S₃[$1] );
consider S being Subset-Family of T such that
A9: S = { H₁(b) where b is Subset of T : S₄[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 )

proof

let a be Subset of (T | (union S)); :: thesis:
assume a in S9 ; :: thesis:
then consider b being Subset of T such that
A12: a = H₁(b) and
A13: S₄[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:

end;

then A14: ( S9 is finite-ind & ind S9 <= n ) by TOPDIM_1:11;
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

let p be Point of T; :: thesis:
let U be open Subset of T; :: thesis:
assume p in U ; :: thesis:
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:
H₁(a) in S by A9, A16;
then H₁(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:

end;

take union S ; :: thesis:
take (union S) ` ; :: thesis:
A18: card { H₁(b) where b is Subset of T : ( b in uB & S₃[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

proof

let a be Subset of (T | (union S)); :: according to TOPS_2:def 2 :: thesis:
assume a in S9 ; :: thesis:
then ex b being Subset of T st
( a = H₁(b) & S₄[b] ) by A9;
hence a is closed by TSEP_1:8; :: thesis:

end;

S9 is Cover of (T | (union S)) by A10, SETFAM_1:def 11;
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:

end;

A21: S₂[ 0 ] by TOPDIM_1:36;
A22: for n being Nat st S₂[n] holds
S₂[n + 1]

proof

let n be Nat; :: thesis:
assume A23: S₂[n] ; :: thesis:
let T be metrizable TopSpace; :: thesis:
assume A24: T is second-countable ; :: thesis:
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:

per cases ;

suppose T is empty ; :: thesis:

hence ( T is finite-ind & ind T <= n + 1 ) by TOPDIM_1:6; :: thesis:

end;

suppose A29: not T is empty ; :: thesis:

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₃[ 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₃[x,y] )

proof

let x be object ; :: thesis:
assume x in NAT ; :: thesis:
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:
thus y in [:(bool the carrier of T),(bool the carrier of T):] ; :: thesis:
let i be Nat; :: thesis:
let a, b be Subset of T; :: thesis:
assume that
A46: x = i and
A47: y = [a,b] ; :: thesis:
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:

end;

consider P12 being sequence of [:(bool the carrier of T),(bool the carrier of T):] such that
A49: for x being object st x in NAT holds
S₃[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

proof

let i be Nat; :: thesis:
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

let A be Subset of T; :: according to TOPS_2:def 2 :: thesis:
assume A in fi ; :: thesis:
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:

end;

then A57: union fi is closed by TOPS_2:21;
( 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:

end;

for i being Nat holds
( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma )

proof

let i be Nat; :: thesis:
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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A66: x in (Union (pr1 P12)) /\ (g . i) ; :: thesis:
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:

end;

y1 \/ y2 = g . i by A49, A60, A61, A62;
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:

end;

then consider G1 being Subset-Family of Tu1 such that
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

let i be Nat; :: thesis:
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

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A86: x in (Union (pr2 P12)) /\ (g . i) ; :: thesis:
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:

end;

y1 \/ y2 = g . i by A49, A79, A81, A82;
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:

end;

then consider G2 being Subset-Family of Tu2 such that
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

let x be object ; :: according to TARSKI:def 3 :: thesis:
A99: dom P12 = NAT by FUNCT_2:def 1;
assume x in [#] T ; :: thesis:
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:

end;

then A106: (Union (pr1 P12)) \/ (Union (pr2 P12)) = [#] T ;
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:

end;

A108: for n being Nat holds S₂[n] from NAT_1:sch 2(A21, A22);
let T be metrizable TopSpace; :: thesis:
assume A109: T is second-countable ; :: thesis:
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:
assume that
A110: T is finite-ind and
A111: ind T <= n ; :: thesis:

per cases ;

suppose A112: n = 0 ; :: thesis:

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

end;

suppose n > 0 ; :: thesis:

then reconsider n1 = n - 1 as Element of NAT by NAT_1:20;
( S₂[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:

end;