let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
defpred S1[ Nat] means for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= $1 holds
( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) );
reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;
A1: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A2: S1[n] ; :: thesis: S1[n + 1]
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= n + 1 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
assume that
A3: ( not TM1 is empty or not TM2 is empty ) and
A4: ((ind TM1) + (ind TM2)) + 2 <= n + 1 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
set T12 = [:TM1,TM2:];
per cases ( TM1 is empty or TM2 is empty or ( not TM1 is empty & not TM2 is empty ) ) ;
suppose A5: TM1 is empty ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then ind TM1 = - 1 by TOPDIM_1:6;
then 0 + (- 1) <= (ind TM2) + (ind TM1) by A3, XREAL_1:6;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A5, TOPDIM_1:6; :: thesis: verum
end;
suppose A6: TM2 is empty ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then ind TM2 = - 1 by TOPDIM_1:6;
then 0 + (- 1) <= (ind TM1) + (ind TM2) by A3, XREAL_1:6;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A6, TOPDIM_1:6; :: thesis: verum
end;
suppose A7: ( not TM1 is empty & not TM2 is empty ) ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
then reconsider i1 = ind TM1, i2 = ind TM2 as Nat by TARSKI:1;
A8: for p being Point of [:TM1,TM2:]
for U being open Subset of [:TM1,TM2:] st p in U holds
ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
proof
let p be Point of [:TM1,TM2:]; :: thesis: for U being open Subset of [:TM1,TM2:] st p in U holds
ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
let U be open Subset of [:TM1,TM2:]; :: thesis: ( p in U implies ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 ) )
consider F being Subset-Family of [:TM1,TM2:] such that
A9: U = union F and
A10: for e being set st e in F holds
ex X1 being Subset of TM1 ex X2 being Subset of TM2 st
( e = [:X1,X2:] & X1 is open & X2 is open ) by BORSUK_1:5;
assume p in U ; :: thesis: ex W being open Subset of [:TM1,TM2:] st
( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= (i1 + i2) - 1 )
then consider U12 being set such that
A11: p in U12 and
A12: U12 in F by A9, TARSKI:def 4;
A13: U12 c= U by A9, A12, ZFMISC_1:74;
consider U1 being Subset of TM1, U2 being Subset of TM2 such that
A14: U12 = [:U1,U2:] and
A15: U1 is open and
A16: U2 is open by A10, A12;
consider p1, p2 being object such that
A17: p1 in U1 and
A18: p2 in U2 and
A19: p = [p1,p2] by A11, A14, ZFMISC_1:def 2;
reconsider p1 = p1 as Point of TM1 by A17;
consider W1 being open Subset of TM1 such that
A20: p1 in W1 and
A21: W1 c= U1 and
Fr W1 is finite-ind and
A22: ind (Fr W1) <= i1 - 1 by A15, A17, TOPDIM_1:16;
set ClW1 = Cl W1;
A23: ( ind (TM1 | (Cl W1)) = ind (Cl W1) & ind (Cl W1) <= i1 ) by TOPDIM_1:17, TOPDIM_1:19;
reconsider p2 = p2 as Point of TM2 by A18;
consider W2 being open Subset of TM2 such that
A24: p2 in W2 and
A25: W2 c= U2 and
Fr W2 is finite-ind and
A26: ind (Fr W2) <= i2 - 1 by A16, A18, TOPDIM_1:16;
reconsider W12 = [:W1,W2:] as open Subset of [:TM1,TM2:] by BORSUK_1:6;
take W12 ; :: thesis: ( p in W12 & W12 c= U & Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )
W12 c= U12 by A14, A25, A21, ZFMISC_1:96;
hence ( p in W12 & W12 c= U ) by A13, A19, A24, A20, ZFMISC_1:87; :: thesis: ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 )
((i1 + i2) + 1) + 1 <= n + 1 by A4;
then A27: (i1 + i2) + 1 <= n by XREAL_1:6;
set FrW1 = Fr W1;
A28: ind (TM1 | (Fr W1)) = ind (Fr W1) by TOPDIM_1:17;
set ClW2 = Cl W2;
reconsider F1C2 = [:(Fr W1),(Cl W2):] as Subset of [:TM1,TM2:] ;
A29: [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] = [:TM1,TM2:] | F1C2 by BORSUK_3:22;
( ind (TM2 | (Cl W2)) = ind (Cl W2) & ind (Cl W2) <= i2 ) by TOPDIM_1:17, TOPDIM_1:19;
then A30: (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) <= (i1 - 1) + i2 by A22, A28, XREAL_1:7;
then ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= ((i1 + i2) - 1) + 2 by XREAL_1:6;
then A31: ( W2 c= Cl W2 & ((ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2)))) + 2 <= n ) by A27, PRE_TOPC:18, XXREAL_0:2;
then [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] is finite-ind by A2, A7, A24;
then A32: F1C2 is finite-ind by A29, TOPDIM_1:18;
set FrW2 = Fr W2;
reconsider C1F2 = [:(Cl W1),(Fr W2):] as Subset of [:TM1,TM2:] ;
A33: [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] = [:TM1,TM2:] | C1F2 by BORSUK_3:22;
ind (TM2 | (Fr W2)) = ind (Fr W2) by TOPDIM_1:17;
then A34: (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) <= i1 + (i2 - 1) by A26, A23, XREAL_1:7;
then ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= (i1 + (i2 - 1)) + 2 by XREAL_1:6;
then A35: ((ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2)))) + 2 <= n by A27, XXREAL_0:2;
( W1 c= Cl W1 & [#] (TM1 | (Cl W1)) = Cl W1 ) by PRE_TOPC:18, PRE_TOPC:def 5;
then A36: not TM1 | (Cl W1) is empty by A20;
then [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] is finite-ind by A2, A35;
then A37: C1F2 is finite-ind by A33, TOPDIM_1:18;
ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (ind (TM1 | (Cl W1))) + (ind (TM2 | (Fr W2))) by A2, A35, A36;
then ind [:(TM1 | (Cl W1)),(TM2 | (Fr W2)):] <= (i1 + i2) - 1 by A34, XXREAL_0:2;
then A38: ind C1F2 <= (i1 + i2) - 1 by A33, A37, TOPDIM_1:17;
A39: ( F1C2 is closed & [:TM1,TM2:] | (C1F2 \/ F1C2) is second-countable ) by TOPALG_3:15;
ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (ind (TM1 | (Fr W1))) + (ind (TM2 | (Cl W2))) by A2, A7, A24, A31;
then ind [:(TM1 | (Fr W1)),(TM2 | (Cl W2)):] <= (i1 - 1) + i2 by A30, XXREAL_0:2;
then ind F1C2 <= (i1 + i2) - 1 by A29, A32, TOPDIM_1:17;
then ( C1F2 \/ F1C2 is finite-ind & ind (C1F2 \/ F1C2) <= (i1 + i2) - 1 ) by A39, A32, A37, A38, Th5;
hence ( Fr W12 is finite-ind & ind (Fr W12) <= (i1 + i2) - 1 ) by Th10; :: thesis: verum
end;
then [:TM1,TM2:] is finite-ind by TOPDIM_1:15;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A8, TOPDIM_1:16; :: thesis: verum
end;
end;
end;
A40: S1[ 0 ]
proof
let TM1, TM2 be second-countable finite-ind metrizable TopSpace; :: thesis: ( ( not TM1 is empty or not TM2 is empty ) & ((ind TM1) + (ind TM2)) + 2 <= 0 implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) )
assume that
A41: ( not TM1 is empty or not TM2 is empty ) and
A42: ((ind TM1) + (ind TM2)) + 2 <= 0 ; :: thesis: ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) )
reconsider i1 = (ind TM1) + 1, i2 = (ind TM2) + 1 as Nat by Lm1;
i1 + i2 <= 0 by A42;
hence ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) by A41; :: thesis: verum
end;
A43: for n being Nat holds S1[n] from NAT_1:sch 2(A40, A1);
 ((ind TM1) + (ind TM2)) + 2 = i1 + i2 ;
hence ( ( not TM1 is empty or not TM2 is empty ) implies ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) ) by A43; :: thesis: verum