:: TOPDIM_2 semantic presentation begin definition let X be set ; let Fx be Subset-Family of X; attrFx is finite-order means :Def1: :: TOPDIM_2:def 1 ex n being Nat st for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds meet Gx is empty ; end; :: deftheorem Def1 defines finite-order TOPDIM_2:def_1_:_ for X being set for Fx being Subset-Family of X holds ( Fx is finite-order iff ex n being Nat st for Gx being Subset-Family of X st Gx c= Fx & n in card Gx holds meet Gx is empty ); registration let X be set ; cluster finite-order for Element of bool (bool X); existence ex b1 being Subset-Family of X st b1 is finite-order proof reconsider E = {} as Subset-Family of X by XBOOLE_1:2; take E ; ::_thesis: E is finite-order take 0 ; :: according to TOPDIM_2:def_1 ::_thesis: for Gx being Subset-Family of X st Gx c= E & 0 in card Gx holds meet Gx is empty let G be Subset-Family of X; ::_thesis: ( G c= E & 0 in card G implies meet G is empty ) thus ( G c= E & 0 in card G implies meet G is empty ) ; ::_thesis: verum end; cluster finite -> finite-order for Element of bool (bool X); coherence for b1 being Subset-Family of X st b1 is finite holds b1 is finite-order proof let F be Subset-Family of X; ::_thesis: ( F is finite implies F is finite-order ) assume F is finite ; ::_thesis: F is finite-order then reconsider f = F as finite Subset-Family of X ; take n = card f; :: according to TOPDIM_2:def_1 ::_thesis: for Gx being Subset-Family of X st Gx c= F & n in card Gx holds meet Gx is empty let G be Subset-Family of X; ::_thesis: ( G c= F & n in card G implies meet G is empty ) assume that A1: G c= F and A2: n in card G ; ::_thesis: meet G is empty card G c= card F by A1, CARD_1:11; hence meet G is empty by A2, NAT_1:44; ::_thesis: verum end; end; definition let X be set ; let Fx be Subset-Family of X; func order Fx -> ext-real number means :Def2: :: TOPDIM_2:def 2 ( ( for Gx being Subset-Family of X st it + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = it + 1 & ( not meet Gx is empty or Gx is empty ) ) ) if Fx is finite-order otherwise it = +infty ; existence ( ( Fx is finite-order implies ex b1 being ext-real number st ( ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b1 being ext-real number st b1 = +infty ) ) proof defpred S1[ Nat] means for Gx being Subset-Family of X st Gx c= Fx & $1 in card Gx holds meet Gx is empty ; now__::_thesis:_(_Fx_is_finite-order_implies_ex_O_being_set_st_ (_(_for_Gx_being_Subset-Family_of_X_st_O_+_1_in_card_Gx_&_Gx_c=_Fx_holds_ meet_Gx_is_empty_)_&_ex_Gx_being_Subset-Family_of_X_st_ (_Gx_c=_Fx_&_card_Gx_=_O_+_1_&_(_not_meet_Gx_is_empty_or_Gx_is_empty_)_)_)_) assume Fx is finite-order ; ::_thesis: ex O being set st ( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ) then A1: ex n being Nat st S1[n] by Def1; consider k being Nat such that A2: S1[k] and A3: for n being Nat st S1[n] holds k <= n from NAT_1:sch_5(A1); take O = k - 1; ::_thesis: ( ( for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ) thus for Gx being Subset-Family of X st O + 1 in card Gx & Gx c= Fx holds meet Gx is empty by A2; ::_thesis: ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) thus ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) ::_thesis: verum proof percases ( k = 0 or k > 0 ) ; supposeA4: k = 0 ; ::_thesis: ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) reconsider E = {} as Subset-Family of X by XBOOLE_1:2; take E ; ::_thesis: ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) ) thus ( E c= Fx & card E = O + 1 & ( not meet E is empty or E is empty ) ) by A4, XBOOLE_1:2; ::_thesis: verum end; suppose k > 0 ; ::_thesis: ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O + 1 & ( not meet Gx is empty or Gx is empty ) ) then reconsider k1 = k - 1 as Element of NAT by NAT_1:20; assume A5: for Gx being Subset-Family of X st Gx c= Fx & card Gx = O + 1 holds ( meet Gx is empty & not Gx is empty ) ; ::_thesis: contradiction S1[k1] proof A6: card (card (k1 + 1)) = card (k1 + 1) ; then A7: card (k1 + 1) = k by CARD_1:40; let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & k1 in card Gx implies meet Gx is empty ) assume that A8: Gx c= Fx and A9: k1 in card Gx ; ::_thesis: meet Gx is empty card (card k1) = card k1 ; then card k1 = k1 by CARD_1:40; then nextcard k1 = card k by A6, NAT_1:42; then card k c= card Gx by A9, CARD_3:90; then consider f being Function such that A10: ( f is one-to-one & dom f = k ) and A11: rng f c= Gx by CARD_1:10; reconsider R = rng f as Subset-Family of X by A11, XBOOLE_1:1; k,R are_equipotent by A10, WELLORD2:def_4; then A12: k = card R by A7, CARD_1:5; then A13: not R is empty by A6; R c= Fx by A8, A11, XBOOLE_1:1; then meet R is empty by A5, A12; then meet Gx c= {} by A11, A13, SETFAM_1:6; hence meet Gx is empty ; ::_thesis: verum end; then k1 + 1 <= k1 by A3; hence contradiction by NAT_1:13; ::_thesis: verum end; end; end; end; hence ( ( Fx is finite-order implies ex b1 being ext-real number st ( ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) & ( not Fx is finite-order implies ex b1 being ext-real number st b1 = +infty ) ) ; ::_thesis: verum end; uniqueness for b1, b2 being ext-real number holds ( ( Fx is finite-order & ( for Gx being Subset-Family of X st b1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = b1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st b2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = b2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies b1 = b2 ) & ( not Fx is finite-order & b1 = +infty & b2 = +infty implies b1 = b2 ) ) proof let O1, O2 be ext-real number ; ::_thesis: ( ( Fx is finite-order & ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies O1 = O2 ) & ( not Fx is finite-order & O1 = +infty & O2 = +infty implies O1 = O2 ) ) now__::_thesis:_(_Fx_is_finite-order_&_(_for_Gx_being_Subset-Family_of_X_st_O1_+_1_in_card_Gx_&_Gx_c=_Fx_holds_ meet_Gx_is_empty_)_&_ex_G1_being_Subset-Family_of_X_st_ (_G1_c=_Fx_&_card_G1_=_O1_+_1_&_(_not_meet_G1_is_empty_or_G1_is_empty_)_)_&_(_for_Gx_being_Subset-Family_of_X_st_O2_+_1_in_card_Gx_&_Gx_c=_Fx_holds_ meet_Gx_is_empty_)_&_ex_G2_being_Subset-Family_of_X_st_ (_G2_c=_Fx_&_card_G2_=_O2_+_1_&_(_not_meet_G2_is_empty_or_G2_is_empty_)_)_implies_O1_=_O2_) assume Fx is finite-order ; ::_thesis: ( ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex G1 being Subset-Family of X st ( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex G2 being Subset-Family of X st ( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 ) assume A14: for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ; ::_thesis: ( ex G1 being Subset-Family of X st ( G1 c= Fx & card G1 = O1 + 1 & ( not meet G1 is empty or G1 is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex G2 being Subset-Family of X st ( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 ) given G1 being Subset-Family of X such that A15: G1 c= Fx and A16: card G1 = O1 + 1 and A17: ( not meet G1 is empty or G1 is empty ) ; ::_thesis: ( ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex G2 being Subset-Family of X st ( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 ) assume A18: for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ; ::_thesis: ( ex G2 being Subset-Family of X st ( G2 c= Fx & card G2 = O2 + 1 & ( not meet G2 is empty or G2 is empty ) ) implies O1 = O2 ) given G2 being Subset-Family of X such that A19: G2 c= Fx and A20: card G2 = O2 + 1 and A21: ( not meet G2 is empty or G2 is empty ) ; ::_thesis: O1 = O2 not card G2 in card G1 by A15, A17, A18, A20; then A22: card G1 c= card G2 by CARD_1:3; not card G1 in card G2 by A14, A16, A19, A21; then card G1 = card G2 by A22, CARD_1:3; hence O1 = O2 by A16, A20, XXREAL_3:11; ::_thesis: verum end; hence ( ( Fx is finite-order & ( for Gx being Subset-Family of X st O1 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O1 + 1 & ( not meet Gx is empty or Gx is empty ) ) & ( for Gx being Subset-Family of X st O2 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = O2 + 1 & ( not meet Gx is empty or Gx is empty ) ) implies O1 = O2 ) & ( not Fx is finite-order & O1 = +infty & O2 = +infty implies O1 = O2 ) ) ; ::_thesis: verum end; consistency for b1 being ext-real number holds verum ; end; :: deftheorem Def2 defines order TOPDIM_2:def_2_:_ for X being set for Fx being Subset-Family of X for b3 being ext-real number holds ( ( Fx is finite-order implies ( b3 = order Fx iff ( ( for Gx being Subset-Family of X st b3 + 1 in card Gx & Gx c= Fx holds meet Gx is empty ) & ex Gx being Subset-Family of X st ( Gx c= Fx & card Gx = b3 + 1 & ( not meet Gx is empty or Gx is empty ) ) ) ) ) & ( not Fx is finite-order implies ( b3 = order Fx iff b3 = +infty ) ) ); registration let X be set ; let F be finite-order Subset-Family of X; cluster(order F) + 1 -> natural ; coherence (order F) + 1 is natural proof consider G being Subset-Family of X such that A1: G c= F and A2: card G = (order F) + 1 and A3: ( not meet G is empty or G is empty ) by Def2; consider n being Nat such that A4: for H being Subset-Family of X st H c= F & n in card H holds meet H is empty by Def1; card n = card (card n) ; then A5: card n = n by CARD_1:40; then not card n in card G by A1, A3, A4; then card G c= n by A5, CARD_1:4; then reconsider G = G as finite Subset-Family of X ; (order F) + 1 = ((card G) - 1) + 1 by A2; hence (order F) + 1 is natural ; ::_thesis: verum end; cluster order F -> ext-real integer ; coherence order F is integer proof reconsider O1 = (order F) + 1 as Nat ; (order F) + 1 = (O1 - 1) + 1 ; hence order F is integer by XXREAL_3:11; ::_thesis: verum end; end; theorem Th1: :: TOPDIM_2:1 for n being Nat for X being set for Fx being Subset-Family of X st order Fx <= n holds Fx is finite-order proof let n be Nat; ::_thesis: for X being set for Fx being Subset-Family of X st order Fx <= n holds Fx is finite-order let X be set ; ::_thesis: for Fx being Subset-Family of X st order Fx <= n holds Fx is finite-order let Fx be Subset-Family of X; ::_thesis: ( order Fx <= n implies Fx is finite-order ) assume order Fx <= n ; ::_thesis: Fx is finite-order then order Fx <> +infty by XXREAL_0:4; hence Fx is finite-order by Def2; ::_thesis: verum end; theorem :: TOPDIM_2:2 for n being Nat for X being set for Fx being Subset-Family of X st order Fx <= n holds for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds meet Gx is empty proof let n be Nat; ::_thesis: for X being set for Fx being Subset-Family of X st order Fx <= n holds for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds meet Gx is empty let X be set ; ::_thesis: for Fx being Subset-Family of X st order Fx <= n holds for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds meet Gx is empty let Fx be Subset-Family of X; ::_thesis: ( order Fx <= n implies for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds meet Gx is empty ) card (n + 1) = card (card (n + 1)) ; then A1: card (n + 1) = n + 1 by CARD_1:40; card (n + 2) = card (card (n + 2)) ; then A2: card (n + 2) = n + 2 by CARD_1:40; assume A3: order Fx <= n ; ::_thesis: for Gx being Subset-Family of X st Gx c= Fx & n + 1 in card Gx holds meet Gx is empty then reconsider f = Fx as finite-order Subset-Family of X by Th1; (order f) + 1 <= n + 1 by A3, XREAL_1:6; then (order f) + 1 < (n + 1) + 1 by NAT_1:13; then A4: (order f) + 1 in n + 2 by NAT_1:44; let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty ) assume that A5: Gx c= Fx and A6: n + 1 in card Gx ; ::_thesis: meet Gx is empty nextcard (n + 1) c= card Gx by A6, CARD_3:90; then card ((n + 1) + 1) c= card Gx by A1, NAT_1:42; hence meet Gx is empty by A5, A2, A4, Def2; ::_thesis: verum end; theorem Th3: :: TOPDIM_2:3 for n being Nat for X being set for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds meet G is empty ) holds order Fx <= n proof let n be Nat; ::_thesis: for X being set for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds meet G is empty ) holds order Fx <= n let X be set ; ::_thesis: for Fx being Subset-Family of X st ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds meet G is empty ) holds order Fx <= n let Fx be Subset-Family of X; ::_thesis: ( ( for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds meet G is empty ) implies order Fx <= n ) set n1 = n + 1; assume A1: for G being finite Subset-Family of X st G c= Fx & n + 1 < card G holds meet G is empty ; ::_thesis: order Fx <= n A2: now__::_thesis:_for_Gx_being_Subset-Family_of_X_st_Gx_c=_Fx_&_n_+_1_in_card_Gx_holds_ meet_Gx_is_empty card (card ((n + 1) + 1)) = card ((n + 1) + 1) ; then A3: card ((n + 1) + 1) = (n + 1) + 1 by CARD_1:40; let Gx be Subset-Family of X; ::_thesis: ( Gx c= Fx & n + 1 in card Gx implies meet Gx is empty ) assume that A4: Gx c= Fx and A5: n + 1 in card Gx ; ::_thesis: meet Gx is empty card (card (n + 1)) = card (n + 1) ; then card (n + 1) = n + 1 by CARD_1:40; then nextcard (n + 1) = card ((n + 1) + 1) by NAT_1:42; then card ((n + 1) + 1) c= card Gx by A5, CARD_3:90; then consider f being Function such that A6: ( f is one-to-one & dom f = (n + 1) + 1 ) and A7: rng f c= Gx by CARD_1:10; reconsider R = rng f as Subset-Family of X by A7, XBOOLE_1:1; (n + 1) + 1,R are_equipotent by A6, WELLORD2:def_4; then A8: (n + 1) + 1 = card R by A3, CARD_1:5; then reconsider R = R as finite Subset-Family of X ; n + 1 < card R by A8, NAT_1:13; then A9: meet R is empty by A1, A4, A7, XBOOLE_1:1; not R is empty by A8; then meet Gx c= {} by A7, A9, SETFAM_1:6; hence meet Gx is empty ; ::_thesis: verum end; then reconsider f = Fx as finite-order Subset-Family of X by Def1; consider Gx being Subset-Family of X such that A10: Gx c= f and A11: card Gx = (order f) + 1 and A12: ( not meet Gx is empty or Gx is empty ) by Def2; assume order Fx > n ; ::_thesis: contradiction then (order f) + 1 > n + 1 by XREAL_1:6; then n + 1 in card Gx by A11, NAT_1:44; hence contradiction by A2, A10, A12; ::_thesis: verum end; begin Lm1: for T being TopSpace for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat proof let T be TopSpace; ::_thesis: for Af being finite-ind Subset of T holds (ind Af) + 1 is Nat let Af be finite-ind Subset of T; ::_thesis: (ind Af) + 1 is Nat Af in (Seq_of_ind T) . (1 + (ind Af)) by TOPDIM_1:def_5; then (ind Af) + 1 in dom (Seq_of_ind T) by FUNCT_1:def_2; hence (ind Af) + 1 is Nat ; ::_thesis: verum end; Lm2: for n being Nat for T being TopSpace for g being SetSequence of T st ( for i being Nat holds ( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds ex G being Subset-Family of T st ( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) proof let n be Nat; ::_thesis: for T being TopSpace for g being SetSequence of T st ( for i being Nat holds ( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds ex G being Subset-Family of T st ( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) let T be TopSpace; ::_thesis: for g being SetSequence of T st ( for i being Nat holds ( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) holds ex G being Subset-Family of T st ( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) let g be SetSequence of T; ::_thesis: ( ( for i being Nat holds ( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ) implies ex G being Subset-Family of T st ( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) ) assume A1: for i being Nat holds ( g . i is finite-ind & ind (g . i) <= n & g . i is F_sigma ) ; ::_thesis: ex G being Subset-Family of T st ( G is closed & G is finite-ind & ind G <= n & G is countable & Union g = union G ) defpred S1[ set , set ] means for n being Nat for F being Subset-Family of T st n = $1 & F = $2 holds ( union F = g . n & F is closed & F is countable ); A2: for x being set st x in NAT holds ex y being set st ( y in bool (bool the carrier of T) & S1[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in bool (bool the carrier of T) & S1[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in bool (bool the carrier of T) & S1[x,y] ) then reconsider n = x as Element of NAT ; g . n is F_sigma by A1; then consider y being closed countable Subset-Family of T such that A3: g . n = union y by TOPGEN_4:def_6; take y ; ::_thesis: ( y in bool (bool the carrier of T) & S1[x,y] ) thus ( y in bool (bool the carrier of T) & S1[x,y] ) by A3; ::_thesis: verum end; consider f being SetSequence of (bool the carrier of T) such that A4: for x being set st x in NAT holds S1[x,f . x] from FUNCT_2:sch_1(A2); take F = Union f; ::_thesis: ( F is closed & F is finite-ind & ind F <= n & F is countable & Union g = union F ) thus F is closed ::_thesis: ( F is finite-ind & ind F <= n & F is countable & Union g = union F ) proof let A be Subset of T; :: according to TOPS_2:def_2 ::_thesis: ( not A in F or A is closed ) assume A in F ; ::_thesis: A is closed then consider n being Element of NAT such that A5: A in f . n by PROB_1:12; f . n is closed by A4; hence A is closed by A5, TOPS_2:def_2; ::_thesis: verum end; for A being Subset of T st A in F holds ( A is finite-ind & ind A <= n ) proof let A be Subset of T; ::_thesis: ( A in F implies ( A is finite-ind & ind A <= n ) ) assume A in F ; ::_thesis: ( A is finite-ind & ind A <= n ) then consider i being Element of NAT such that A6: A in f . i by PROB_1:12; union (f . i) = g . i by A4; then A7: A c= g . i by A6, ZFMISC_1:74; A8: ind (g . i) <= n by A1; A9: g . i is finite-ind by A1; then ind A <= ind (g . i) by A7, TOPDIM_1:19; hence ( A is finite-ind & ind A <= n ) by A7, A8, A9, TOPDIM_1:19, XXREAL_0:2; ::_thesis: verum end; hence ( F is finite-ind & ind F <= n ) by TOPDIM_1:11; ::_thesis: ( F is countable & Union g = union F ) for x being set st x in dom f holds f . x is countable by A4; hence F is countable by CARD_4:11; ::_thesis: Union g = union F thus Union g c= union F :: according to XBOOLE_0:def_10 ::_thesis: union F c= Union g proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Union g or x in union F ) assume x in Union g ; ::_thesis: x in union F then consider i being Element of NAT such that A10: x in g . i by PROB_1:12; union (f . i) = g . i by A4; then consider y being set such that A11: x in y and A12: y in f . i by A10, TARSKI:def_4; y in F by A12, PROB_1:12; hence x in union F by A11, TARSKI:def_4; ::_thesis: verum end; thus union F c= Union g ::_thesis: verum proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in union F or x in Union g ) assume x in union F ; ::_thesis: x in Union g then consider y being set such that A13: x in y and A14: y in F by TARSKI:def_4; consider i being Element of NAT such that A15: y in f . i by A14, PROB_1:12; union (f . i) = g . i by A4; then x in g . i by A13, A15, TARSKI:def_4; hence x in Union g by PROB_1:12; ::_thesis: verum end; end; Lm3: for n being Nat 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 ) ) ) proof 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 S1[ 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 S2[ 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 S2[n] holds S1[n + 1] proof defpred S3[ set ] means verum; let n be Nat; ::_thesis: ( S2[n] implies S1[n + 1] ) assume A2: S2[n] ; ::_thesis: S1[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 H1( 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 S4[ set ] means ( $1 in uB & S3[$1] ); consider S being Subset-Family of T such that A9: S = { H1(b) where b is Subset of T : S4[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: ( 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 = H1(b) and A13: S4[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; 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: 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 ) H1(a) in S by A9, A16; then H1(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; take union S ; ::_thesis: ex B being Subset of T st ( [#] 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 { H1(b) where b is Subset of T : ( b in uB & S3[b] ) } c= card uB from BORSUK_2:sch_1(); card uB c= omega by A8, CARD_3:def_14; then card S c= omega by A9, A18, XBOOLE_1:1; then A19: S9 is countable by CARD_3:def_14; A20: S9 is closed proof 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 = H1(b) & S4[b] ) by A9; hence a is closed by TSEP_1:8; ::_thesis: verum 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: verum end; A21: S2[ 0 ] by TOPDIM_1:36; A22: for n being Nat st S2[n] holds S2[n + 1] proof let n be Nat; ::_thesis: ( S2[n] implies S2[n + 1] ) assume A23: S2[n] ; ::_thesis: S2[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 ) percases ( T is empty or not T is empty ) ; suppose T is empty ; ::_thesis: ( T is finite-ind & ind T <= n + 1 ) hence ( T is finite-ind & ind T <= n + 1 ) by TOPDIM_1:6; ::_thesis: verum end; supposeA29: 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 Function of NAT,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 S3[ set , set ] 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 set st x in NAT holds ex y being set st ( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] ) proof let x be set ; ::_thesis: ( x in NAT implies ex y being set st ( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[x,y] ) ) assume x in NAT ; ::_thesis: ex y being set st ( y in [:(bool the carrier of T),(bool the carrier of T):] & S3[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, TOPDIM_1:4; 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):] & S3[x,y] ) thus y in [:(bool the carrier of T),(bool the carrier of T):] ; ::_thesis: S3[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; consider P12 being Function of NAT,[:(bool the carrier of T),(bool the carrier of T):] such that A49: for x being set st x in NAT holds S3[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: 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 proof 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, TOPS_2:def_2; ::_thesis: verum 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, TOPS_2:def_2; 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; 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: ( P1 . i is finite-ind & ind (P1 . i) <= n & P1 . i is F_sigma ) consider y1, y2 being set 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; 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 set ; :: 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 Element of NAT such that A68: x in P1 . j by PROB_1:12; consider z1, z2 being set 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; ( [z1,z2] `1 = z1 & dom P12 = NAT ) by FUNCT_2:def_1; then A71: z1 = P1 . j by A70, MCART_1:def_12; z1 \/ z2 = g . j by A49, A69, A70; then x in g . j by A68, A71, 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; 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, XBOOLE_0:def_10; 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; then consider G1 being Subset-Family of Tu1 such that A72: ( G1 is closed & G1 is finite-ind & ind G1 <= n & G1 is countable ) and A73: Union P1 = union G1 by Lm2; A74: G1 is Cover of Tu1 by A51, A73, SETFAM_1:def_11; then A75: Tu1 is finite-ind by A23, A24, A72; then A76: Union (pr1 P12) is finite-ind by TOPDIM_1:18; A77: [#] 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: ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma ) consider y1, y2 being set such that A78: y1 in bool the carrier of T and A79: y2 in bool the carrier of T and A80: P12 . i = [y1,y2] by ZFMISC_1:def_2; reconsider y2 = y2 as Subset of T by A79; A81: i in NAT by ORDINAL1:def_12; then A82: ( y2 is finite-ind & ind y2 <= 0 ) by A49, A78, A80; ( [y1,y2] `2 = y2 & dom P12 = NAT ) by FUNCT_2:def_1; then A83: y2 = P2 . i by A80, A81, MCART_1:def_13; A84: (Union (pr2 P12)) /\ (g . i) c= P2 . i proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (Union (pr2 P12)) /\ (g . i) or x in P2 . i ) assume A85: x in (Union (pr2 P12)) /\ (g . i) ; ::_thesis: x in P2 . i then A86: x in g . i by XBOOLE_0:def_4; x in Union (pr2 P12) by A85, XBOOLE_0:def_4; then consider j being Element of NAT such that A87: x in P2 . j by PROB_1:12; consider z1, z2 being set such that A88: ( z1 in bool the carrier of T & z2 in bool the carrier of T ) and A89: P12 . j = [z1,z2] by ZFMISC_1:def_2; ( [z1,z2] `2 = z2 & dom P12 = NAT ) by FUNCT_2:def_1; then A90: z2 = P2 . j by A89, MCART_1:def_13; z1 \/ z2 = g . j by A49, A88, A89; then x in g . j by A87, A90, XBOOLE_0:def_3; then g . i meets g . j by A86, XBOOLE_0:3; hence x in P2 . i by A33, A87; ::_thesis: verum end; y1 \/ y2 = g . i by A49, A78, A80, A81; then P2 . i c= g . i by A83, XBOOLE_1:7; then P2 . i c= (Union (pr2 P12)) /\ (g . i) by A77, XBOOLE_1:19; then ( P2 . i = (Union (pr2 P12)) /\ (g . i) & g . i is F_sigma ) by A53, A84, XBOOLE_0:def_10; hence ( P2 . i is finite-ind & ind (P2 . i) <= 0 & P2 . i is F_sigma ) by A82, A83, METRIZTS:10, TOPDIM_1:21; ::_thesis: verum end; then consider G2 being Subset-Family of Tu2 such that A91: ( G2 is closed & G2 is finite-ind & ind G2 <= 0 & G2 is countable ) and A92: Union P2 = union G2 by Lm2; A93: G2 is Cover of Tu2 by A77, A92, SETFAM_1:def_11; then Tu2 is finite-ind by A23, A24, A91; then A94: Union (pr2 P12) is finite-ind by TOPDIM_1:18; ind Tu1 <= n by A23, A24, A72, A74; then ind (Union (pr1 P12)) <= n by A76, TOPDIM_1:17; then A95: (ind (Union (pr1 P12))) + 1 <= n + 1 by XREAL_1:6; A96: Union (pr1 P12) is finite-ind by A75, TOPDIM_1:18; [#] T c= (Union (pr1 P12)) \/ (Union (pr2 P12)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] T or x in (Union (pr1 P12)) \/ (Union (pr2 P12)) ) A97: 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 Element of NAT such that A98: x in g . i by PROB_1:12; consider y1, y2 being set such that A99: ( y1 in bool the carrier of T & y2 in bool the carrier of T ) and A100: P12 . i = [y1,y2] by ZFMISC_1:def_2; [y1,y2] `1 = y1 ; then A101: y1 = P1 . i by A97, A100, MCART_1:def_12; [y1,y2] `2 = y2 ; then A102: y2 = P2 . i by A97, A100, MCART_1:def_13; y1 \/ y2 = g . i by A49, A99, A100; then ( x in P1 . i or x in P2 . i ) by A98, A101, A102, 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; then A103: (Union (pr1 P12)) \/ (Union (pr2 P12)) = [#] T by XBOOLE_0:def_10; ind Tu2 <= 0 by A24, A91, A93, TOPDIM_1:36; then A104: ind (Union (pr2 P12)) <= 0 by A94, 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 A94, A104, A96, TOPDIM_1:40; hence ( T is finite-ind & ind T <= n + 1 ) by A103, A95, TOPDIM_1:def_4, XXREAL_0:2; ::_thesis: verum end; end; end; A105: for n being Nat holds S2[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 A106: 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 A105, A106; ::_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 A107: T is finite-ind and A108: 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 ) percases ( n = 0 or n > 0 ) ; supposeA109: n = 0 ; ::_thesis: ex A, B being Subset of T st ( [#] 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 A108, A109, TOPDIM_1:6, XBOOLE_1:65; ::_thesis: verum end; 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 ) then reconsider n1 = n - 1 as Element of NAT by NAT_1:20; ( S2[n1] & n1 + 1 = n ) by A105; hence ex A, B being Subset of T st ( [#] T = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by A1, A106, A107, A108; ::_thesis: verum end; end; end; theorem :: TOPDIM_2:4 for n being Nat for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st ( F is closed & F is Cover of TM & F is countable & F is finite-ind & ind F <= n ) holds ( TM is finite-ind & ind TM <= n ) by Lm3; theorem Th5: :: TOPDIM_2:5 for TM being metrizable TopSpace for I being Integer for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds ( ind (A \/ B) <= I & A \/ B is finite-ind ) proof let TM be metrizable TopSpace; ::_thesis: for I being Integer for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds ( ind (A \/ B) <= I & A \/ B is finite-ind ) let I be Integer; ::_thesis: for A, B being finite-ind Subset of TM st A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I holds ( ind (A \/ B) <= I & A \/ B is finite-ind ) let A, B be finite-ind Subset of TM; ::_thesis: ( A is closed & TM | (A \/ B) is second-countable & ind A <= I & ind B <= I implies ( ind (A \/ B) <= I & A \/ B is finite-ind ) ) assume that A1: A is closed and A2: TM | (A \/ B) is second-countable and A3: ind A <= I and A4: ind B <= I ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind ) - 1 <= ind A by TOPDIM_1:5; then A5: - 1 <= I by A3, XXREAL_0:2; percases ( A \/ B is empty or not A \/ B is empty ) ; suppose A \/ B is empty ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind ) hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A5, TOPDIM_1:6; ::_thesis: verum end; supposeA6: not A \/ B is empty ; ::_thesis: ( ind (A \/ B) <= I & A \/ B is finite-ind ) then A7: not TM is empty ; ( not A is empty or not B is empty ) by A6; then ( 0 <= ind A or 0 <= ind B ) by A7; then A8: I in NAT by A3, A4, INT_1:3; reconsider AB = A \/ B as Subset of TM ; set Tab = TM | AB; A9: [#] (TM | AB) = AB by PRE_TOPC:def_5; then reconsider a = A, b = B as Subset of (TM | AB) by XBOOLE_1:7; A /\ ([#] (TM | AB)) = a by XBOOLE_1:28; then A10: a is closed by A1, TSP_1:def_2; then consider F being closed countable Subset-Family of (TM | AB) such that A11: a ` = union F by TOPGEN_4:def_6; reconsider a = a, b = b as finite-ind Subset of (TM | AB) by TOPDIM_1:21; reconsider AA = {a} as Subset-Family of (TM | AB) ; union (AA \/ F) = (union AA) \/ (union F) by ZFMISC_1:78 .= a \/ (a `) by A11, ZFMISC_1:25 .= [#] (TM | AB) by PRE_TOPC:2 ; then A12: AA \/ F is Cover of (TM | AB) by SETFAM_1:def_11; AA is closed proof let D be Subset of (TM | AB); :: according to TOPS_2:def_2 ::_thesis: ( not D in AA or D is closed ) assume D in AA ; ::_thesis: D is closed hence D is closed by A10, TARSKI:def_1; ::_thesis: verum end; then A13: AA \/ F is closed by TOPS_2:16; for D being Subset of (TM | AB) st D in AA \/ F holds ( D is finite-ind & ind D <= I ) proof let D be Subset of (TM | AB); ::_thesis: ( D in AA \/ F implies ( D is finite-ind & ind D <= I ) ) assume A14: D in AA \/ F ; ::_thesis: ( D is finite-ind & ind D <= I ) percases ( D in AA or D in F ) by A14, XBOOLE_0:def_3; suppose D in AA ; ::_thesis: ( D is finite-ind & ind D <= I ) then D = a by TARSKI:def_1; hence ( D is finite-ind & ind D <= I ) by A3, TOPDIM_1:21; ::_thesis: verum end; supposeA15: D in F ; ::_thesis: ( D is finite-ind & ind D <= I ) a ` = b \ a by A9, XBOOLE_1:40; then A16: a ` c= b by XBOOLE_1:36; D c= a ` by A11, A15, ZFMISC_1:74; then A17: D c= b by A16, XBOOLE_1:1; then ( ind b = ind B & ind D <= ind b ) by TOPDIM_1:19, TOPDIM_1:21; hence ( D is finite-ind & ind D <= I ) by A4, A17, TOPDIM_1:19, XXREAL_0:2; ::_thesis: verum end; end; end; then A18: ( AA \/ F is finite-ind & ind (AA \/ F) <= I ) by A5, TOPDIM_1:11; A19: AA \/ F is countable by CARD_2:85; then TM | AB is finite-ind by A2, A8, A12, A13, A18, Lm3; then A20: A \/ B is finite-ind by TOPDIM_1:18; ind (TM | AB) <= I by A2, A8, A12, A13, A18, A19, Lm3; hence ( ind (A \/ B) <= I & A \/ B is finite-ind ) by A20, TOPDIM_1:17; ::_thesis: verum end; end; end; theorem :: TOPDIM_2:6 for n being Nat for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds ex A, B being Subset of TM st ( [#] TM = A \/ B & A misses B & ind A <= n - 1 & ind B <= 0 ) by Lm3; theorem Th7: :: TOPDIM_2:7 for I being Integer for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= I holds ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) proof let I be Integer; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= I holds ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) defpred S1[ Nat] means for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= $1 - 1 holds ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ); let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= I implies ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) ) assume that A1: ( TM is second-countable & TM is finite-ind ) and A2: ind TM <= I ; ::_thesis: ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) - 1 <= ind ([#] TM) by A1, TOPDIM_1:5; then - 1 <= I by A2, XXREAL_0:2; then (- 1) + 1 <= I + 1 by XREAL_1:6; then reconsider i1 = I + 1 as Element of NAT by INT_1:3; A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= (n + 1) - 1 implies ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) ) assume that A5: TM is second-countable and A6: TM is finite-ind and A7: ind TM <= (n + 1) - 1 ; ::_thesis: ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) consider A, B being Subset of TM such that A8: [#] TM = A \/ B and A9: A misses B and A10: ind A <= n - 1 and A11: ind B <= 0 by A5, A6, A7, Lm3; set BB = {B}; for b being Subset of TM st b in {B} holds ( b is finite-ind & ind b <= 0 ) by A6, A11, TARSKI:def_1; then A12: ( {B} is finite-ind & ind {B} <= 0 ) by TOPDIM_1:11; set TA = TM | A; ind (TM | A) = ind A by A6, TOPDIM_1:17; then consider F being finite Subset-Family of (TM | A) such that A13: F is Cover of (TM | A) and A14: F is finite-ind and A15: ind F <= 0 and A16: card F <= n and A17: for A, B being Subset of (TM | A) st A in F & B in F & A meets B holds A = B by A4, A5, A6, A10; [#] (TM | A) c= [#] TM by PRE_TOPC:def_4; then bool ([#] (TM | A)) c= bool ([#] TM) by ZFMISC_1:67; then reconsider F9 = F as finite Subset-Family of TM by XBOOLE_1:1; take G = F9 \/ {B}; ::_thesis: ( G is Cover of TM & G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds A = B ) ) A18: union F9 = [#] (TM | A) by A13, SETFAM_1:45 .= A by PRE_TOPC:def_5 ; then union G = A \/ (union {B}) by ZFMISC_1:78 .= [#] TM by A8, ZFMISC_1:25 ; hence G is Cover of TM by SETFAM_1:def_11; ::_thesis: ( G is finite-ind & ind G <= 0 & card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds A = B ) ) ( F9 is finite-ind & ind F9 = ind F ) by A14, TOPDIM_1:29; hence ( G is finite-ind & ind G <= 0 ) by A12, A15, TOPDIM_1:13; ::_thesis: ( card G <= n + 1 & ( for A, B being Subset of TM st A in G & B in G & A meets B holds A = B ) ) card {B} = 1 by CARD_1:30; then A19: card G <= (card F9) + 1 by CARD_2:43; (card F9) + 1 <= n + 1 by A16, XREAL_1:6; hence card G <= n + 1 by A19, XXREAL_0:2; ::_thesis: for A, B being Subset of TM st A in G & B in G & A meets B holds A = B let a, b be Subset of TM; ::_thesis: ( a in G & b in G & a meets b implies a = b ) assume that A20: ( a in G & b in G ) and A21: a meets b ; ::_thesis: a = b percases ( ( a in F & b in F ) or ( a in F & b in {B} ) or ( a in {B} & b in F ) or ( a in {B} & b in {B} ) ) by A20, XBOOLE_0:def_3; suppose ( a in F & b in F ) ; ::_thesis: a = b hence a = b by A17, A21; ::_thesis: verum end; supposeA22: ( a in F & b in {B} ) ; ::_thesis: a = b then b = B by TARSKI:def_1; hence a = b by A9, A18, A21, A22, XBOOLE_1:63, ZFMISC_1:74; ::_thesis: verum end; supposeA23: ( a in {B} & b in F ) ; ::_thesis: a = b then a = B by TARSKI:def_1; hence a = b by A9, A18, A21, A23, XBOOLE_1:63, ZFMISC_1:74; ::_thesis: verum end; supposeA24: ( a in {B} & b in {B} ) ; ::_thesis: a = b then a = B by TARSKI:def_1; hence a = b by A24, TARSKI:def_1; ::_thesis: verum end; end; end; A25: S1[ 0 ] proof let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= 0 - 1 implies ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) ) assume that TM is second-countable and A26: TM is finite-ind and A27: ind TM <= 0 - 1 ; ::_thesis: ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) ind ([#] TM) >= - 1 by A26, TOPDIM_1:5; then ind ([#] TM) = - 1 by A27, XXREAL_0:1; then A28: [#] TM = {} TM by A26, TOPDIM_1:6; reconsider F = {} as empty Subset-Family of TM by TOPGEN_4:18; take F ; ::_thesis: ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) F c= {({} TM)} by XBOOLE_1:2; hence ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) by A28, SETFAM_1:def_11, TOPDIM_1:10, ZFMISC_1:2; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A25, A3); then S1[i1] ; hence ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 & ( for A, B being Subset of TM st A in F & B in F & A meets B holds A = B ) ) by A1, A2; ::_thesis: verum end; theorem Th8: :: TOPDIM_2:8 for I being Integer for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) holds ( TM is finite-ind & ind TM <= I ) proof let I be Integer; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) holds ( TM is finite-ind & ind TM <= I ) defpred S1[ Nat] means for TM being metrizable TopSpace st TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= $1 ) holds ( TM is finite-ind & ind TM <= $1 - 1 ); let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= I + 1 ) implies ( TM is finite-ind & ind TM <= I ) ) assume A1: TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds ( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= I + 1 ) or ( TM is finite-ind & ind TM <= I ) ) given F being finite Subset-Family of TM such that A2: ( F is Cover of TM & F is finite-ind & ind F <= 0 ) and A3: card F <= I + 1 ; ::_thesis: ( TM is finite-ind & ind TM <= I ) reconsider i1 = I + 1 as Element of NAT by A3, INT_1:3; A4: S1[ 0 ] proof let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= 0 ) implies ( TM is finite-ind & ind TM <= 0 - 1 ) ) assume TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds ( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= 0 ) or ( TM is finite-ind & ind TM <= 0 - 1 ) ) given F being finite Subset-Family of TM such that A5: F is Cover of TM and F is finite-ind and ind F <= 0 and A6: card F <= 0 ; ::_thesis: ( TM is finite-ind & ind TM <= 0 - 1 ) F = {} by A6; then [#] TM = {} by A5, SETFAM_1:45, ZFMISC_1:2; hence ( TM is finite-ind & ind TM <= 0 - 1 ) by TOPDIM_1:6, TOPDIM_1:def_4; ::_thesis: verum end; A7: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A8: S1[n] ; ::_thesis: S1[n + 1] let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & ex F being finite Subset-Family of TM st ( F is Cover of TM & F is finite-ind & ind F <= 0 & card F <= n + 1 ) implies ( TM is finite-ind & ind TM <= (n + 1) - 1 ) ) assume A9: TM is second-countable ; ::_thesis: ( for F being finite Subset-Family of TM holds ( not F is Cover of TM or not F is finite-ind or not ind F <= 0 or not card F <= n + 1 ) or ( TM is finite-ind & ind TM <= (n + 1) - 1 ) ) given F being finite Subset-Family of TM such that A10: F is Cover of TM and A11: F is finite-ind and A12: ind F <= 0 and A13: card F <= n + 1 ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 ) percases ( F = {} or F <> {} ) ; suppose F = {} ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 ) then card F = 0 ; hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A4, A9, A10, A11, A12; ::_thesis: verum end; suppose F <> {} ; ::_thesis: ( TM is finite-ind & ind TM <= (n + 1) - 1 ) then consider A being set such that A14: A in F by XBOOLE_0:def_1; reconsider A = A as Subset of TM by A14; set AA = {A}; set FA = F \ {A}; A15: (F \ {A}) \/ {A} = F by A14, ZFMISC_1:116; A16: [#] TM = union F by A10, SETFAM_1:45 .= (union (F \ {A})) \/ (union {A}) by A15, ZFMISC_1:78 .= (union (F \ {A})) \/ A by ZFMISC_1:25 ; A17: F \ {A} c= F by XBOOLE_1:36; then A18: ind (F \ {A}) <= 0 by A11, A12, TOPDIM_1:12; not A in F \ {A} by ZFMISC_1:56; then F \ {A} c< F by A14, A17, XBOOLE_0:def_8; then card (F \ {A}) < n + 1 by A13, CARD_2:48, XXREAL_0:2; then A19: card (F \ {A}) <= n by NAT_1:13; reconsider uFA = union (F \ {A}) as Subset of TM ; set Tu = TM | uFA; A20: [#] (TM | uFA) = uFA by PRE_TOPC:def_5; then reconsider FA9 = F \ {A} as Subset-Family of (TM | uFA) by ZFMISC_1:82; A21: TM | A is second-countable by A9; F \ {A} is finite-ind by A11, A17, TOPDIM_1:12; then A22: ( FA9 is finite-ind & ind (F \ {A}) = ind FA9 ) by TOPDIM_1:30; A23: FA9 is Cover of (TM | uFA) by A20, SETFAM_1:def_11; then A24: TM | uFA is finite-ind by A8, A9, A18, A19, A22; then A25: ind (TM | uFA) = ind uFA by A20, TOPDIM_1:22; ind (TM | uFA) <= n - 1 by A8, A9, A18, A19, A22, A23; then A26: (ind uFA) + 1 <= (n - 1) + 1 by A25, XREAL_1:6; A27: uFA is finite-ind by A24, TOPDIM_1:18; ( A is finite-ind & ind A <= 0 ) by A11, A12, A14, TOPDIM_1:11; then ( [#] TM is finite-ind & ind ([#] TM) <= (ind uFA) + 1 ) by A16, A21, A27, TOPDIM_1:40; hence ( TM is finite-ind & ind TM <= (n + 1) - 1 ) by A26, TOPDIM_1:def_4, XXREAL_0:2; ::_thesis: verum end; end; end; for n being Nat holds S1[n] from NAT_1:sch_2(A4, A7); then S1[i1] ; hence ( TM is finite-ind & ind TM <= I ) by A1, A2, A3; ::_thesis: verum end; Lm4: for TM being metrizable TopSpace for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) proof let TM be metrizable TopSpace; ::_thesis: for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) let A, B be Subset of TM; ::_thesis: ( A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable implies ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) ) assume that A1: ( A is finite-ind & B is finite-ind ) and A2: TM | (A \/ B) is second-countable ; ::_thesis: ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) set AB = A \/ B; set Tab = TM | (A \/ B); [#] (TM | (A \/ B)) = A \/ B by PRE_TOPC:def_5; then reconsider a = A, b = B as Subset of (TM | (A \/ B)) by XBOOLE_1:7; A3: a is finite-ind by A1, TOPDIM_1:21; then A4: ind ((TM | (A \/ B)) | a) = ind a by TOPDIM_1:17 .= ind A by A1, TOPDIM_1:21 ; [#] ((TM | (A \/ B)) | b) c= [#] (TM | (A \/ B)) by PRE_TOPC:def_4; then A5: bool ([#] ((TM | (A \/ B)) | b)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67; A6: b is finite-ind by A1, TOPDIM_1:21; then consider Fb being finite Subset-Family of ((TM | (A \/ B)) | b) such that A7: Fb is Cover of ((TM | (A \/ B)) | b) and A8: Fb is finite-ind and A9: ind Fb <= 0 and A10: card Fb <= (ind ((TM | (A \/ B)) | b)) + 1 and for a9, b9 being Subset of ((TM | (A \/ B)) | b) st a9 in Fb & b9 in Fb & a9 meets b9 holds a9 = b9 by A2, Th7; consider Fa being finite Subset-Family of ((TM | (A \/ B)) | a) such that A11: Fa is Cover of ((TM | (A \/ B)) | a) and A12: Fa is finite-ind and A13: ind Fa <= 0 and A14: card Fa <= (ind ((TM | (A \/ B)) | a)) + 1 and for a9, b9 being Subset of ((TM | (A \/ B)) | a) st a9 in Fa & b9 in Fa & a9 meets b9 holds a9 = b9 by A2, A3, Th7; [#] ((TM | (A \/ B)) | a) c= [#] (TM | (A \/ B)) by PRE_TOPC:def_4; then bool ([#] ((TM | (A \/ B)) | a)) c= bool ([#] (TM | (A \/ B))) by ZFMISC_1:67; then reconsider FA = Fa, FB = Fb as finite Subset-Family of (TM | (A \/ B)) by A5, XBOOLE_1:1; A15: FB is finite-ind by A8, TOPDIM_1:29; ind ((TM | (A \/ B)) | b) = ind b by A6, TOPDIM_1:17 .= ind B by A1, TOPDIM_1:21 ; then ( card (FA \/ FB) <= (card FA) + (card FB) & (card FA) + (card FB) <= ((ind A) + 1) + ((ind B) + 1) ) by A10, A14, A4, CARD_2:43, XREAL_1:7; then A16: card (FA \/ FB) <= (((ind A) + 1) + (ind B)) + 1 by XXREAL_0:2; union (FA \/ FB) = (union Fa) \/ (union Fb) by ZFMISC_1:78 .= ([#] ((TM | (A \/ B)) | a)) \/ (union Fb) by A11, SETFAM_1:45 .= ([#] ((TM | (A \/ B)) | a)) \/ ([#] ((TM | (A \/ B)) | b)) by A7, SETFAM_1:45 .= a \/ ([#] ((TM | (A \/ B)) | b)) by PRE_TOPC:def_5 .= a \/ b by PRE_TOPC:def_5 .= [#] (TM | (A \/ B)) by PRE_TOPC:def_5 ; then A17: FA \/ FB is Cover of (TM | (A \/ B)) by SETFAM_1:def_11; A18: ind FB = ind Fb by A8, TOPDIM_1:29; A19: FA is finite-ind by A12, TOPDIM_1:29; ind FA = ind Fa by A12, TOPDIM_1:29; then A20: ind (FA \/ FB) <= 0 by A9, A13, A19, A15, A18, TOPDIM_1:13; then TM | (A \/ B) is finite-ind by A2, A15, A16, A19, A17, Th8; then A21: A \/ B is finite-ind by TOPDIM_1:18; ind (TM | (A \/ B)) <= ((ind A) + 1) + (ind B) by A2, A15, A16, A19, A17, A20, Th8; hence ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by A21, TOPDIM_1:17; ::_thesis: verum end; registration let TM be second-countable metrizable TopSpace; let A, B be finite-ind Subset of TM; clusterA \/ B -> finite-ind for Subset of TM; coherence for b1 being Subset of TM st b1 = A \/ B holds b1 is with_finite_small_inductive_dimension proof TM | (A \/ B) is second-countable ; hence for b1 being Subset of TM st b1 = A \/ B holds b1 is with_finite_small_inductive_dimension by Lm4; ::_thesis: verum end; end; theorem :: TOPDIM_2:9 for TM being metrizable TopSpace for A, B being Subset of TM st A is finite-ind & B is finite-ind & TM | (A \/ B) is second-countable holds ( A \/ B is finite-ind & ind (A \/ B) <= ((ind A) + (ind B)) + 1 ) by Lm4; theorem Th10: :: TOPDIM_2:10 for T1, T2 being TopSpace for A1 being Subset of T1 for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] proof let T1, T2 be TopSpace; ::_thesis: for A1 being Subset of T1 for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] let A1 be Subset of T1; ::_thesis: for A2 being Subset of T2 holds Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] let A2 be Subset of T2; ::_thesis: Fr [:A1,A2:] = [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] A1: [:(Cl A1),(Cl A2):] /\ [:(Cl (A1 `)),([#] T2):] = [:((Cl A1) /\ (Cl (A1 `))),((Cl A2) /\ ([#] T2)):] by ZFMISC_1:100 .= [:(Fr A1),(Cl A2):] by XBOOLE_1:28 ; A2: [:(Cl A1),(Cl A2):] /\ [:([#] T1),(Cl (A2 `)):] = [:((Cl A1) /\ ([#] T1)),((Cl A2) /\ (Cl (A2 `))):] by ZFMISC_1:100 .= [:(Cl A1),(Fr A2):] by XBOOLE_1:28 ; Cl ([#] T1) = [#] T1 by TOPS_1:2; then A3: Cl [:([#] T1),(A2 `):] = [:([#] T1),(Cl (A2 `)):] by TOPALG_3:14; Cl ([#] T2) = [#] T2 by TOPS_1:2; then A4: Cl [:(A1 `),([#] T2):] = [:(Cl (A1 `)),([#] T2):] by TOPALG_3:14; Cl ([:A1,A2:] `) = Cl ([:([#] T1),([#] T2):] \ [:A1,A2:]) by BORSUK_1:def_2 .= Cl ([:(([#] T1) \ A1),([#] T2):] \/ [:([#] T1),(([#] T2) \ A2):]) by ZFMISC_1:103 .= [:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):] by A4, A3, PRE_TOPC:20 ; hence Fr [:A1,A2:] = [:(Cl A1),(Cl A2):] /\ ([:(Cl (A1 `)),([#] T2):] \/ [:([#] T1),(Cl (A2 `)):]) by TOPALG_3:14 .= [:(Fr A1),(Cl A2):] \/ [:(Cl A1),(Fr A2):] by A1, A2, XBOOLE_1:23 ; ::_thesis: verum end; Lm5: for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds ( [:TM1,TM2:] is finite-ind & ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) ) proof 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:]; percases ( TM1 is empty or TM2 is empty or ( not TM1 is empty & not TM2 is empty ) ) ; supposeA5: 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; supposeA6: 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; supposeA7: ( 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 ; 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 set 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, XBOOLE_1:1, 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 end; registration let TM1, TM2 be second-countable finite-ind metrizable TopSpace; cluster[:TM1,TM2:] -> finite-ind ; coherence [:TM1,TM2:] is with_finite_small_inductive_dimension proof percases ( ( TM1 is empty & TM2 is empty ) or not TM1 is empty or not TM2 is empty ) ; suppose ( TM1 is empty & TM2 is empty ) ; ::_thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension hence [:TM1,TM2:] is with_finite_small_inductive_dimension ; ::_thesis: verum end; suppose ( not TM1 is empty or not TM2 is empty ) ; ::_thesis: [:TM1,TM2:] is with_finite_small_inductive_dimension hence [:TM1,TM2:] is with_finite_small_inductive_dimension by Lm5; ::_thesis: verum end; end; end; end; theorem Th11: :: TOPDIM_2:11 for n being Nat for TM being metrizable TopSpace for A, B being Subset of TM st A is closed & B is closed & A misses B holds for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) proof let n be Nat; ::_thesis: for TM being metrizable TopSpace for A, B being Subset of TM st A is closed & B is closed & A misses B holds for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) let TM be metrizable TopSpace; ::_thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) let A, B be Subset of TM; ::_thesis: ( A is closed & B is closed & A misses B implies for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) ) assume that A1: ( A is closed & B is closed ) and A2: A misses B ; ::_thesis: for H being Subset of TM st ind H <= n & TM | H is second-countable & TM | H is finite-ind holds ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) let H be Subset of TM; ::_thesis: ( ind H <= n & TM | H is second-countable & TM | H is finite-ind implies ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) ) assume that A3: ind H <= n and A4: ( TM | H is second-countable & TM | H is finite-ind ) ; ::_thesis: ex L being Subset of TM st ( L separates A,B & ind (L /\ H) <= n - 1 ) H is finite-ind by A4, TOPDIM_1:18; then ind H = ind (TM | H) by TOPDIM_1:17; then consider a, b being Subset of (TM | H) such that A5: [#] (TM | H) = a \/ b and a misses b and A6: ind a <= n - 1 and A7: ind b <= 0 by A3, A4, Lm3; [#] (TM | H) c= [#] TM by PRE_TOPC:def_4; then reconsider aa = a, bb = b as Subset of TM by XBOOLE_1:1; A8: bb is finite-ind by A4, TOPDIM_1:22; A9: H = aa \/ bb by A5, PRE_TOPC:def_5; then A10: bb /\ H = bb by XBOOLE_1:7, XBOOLE_1:28; ( ind b = ind bb & (TM | H) | b = TM | bb ) by A4, METRIZTS:9, TOPDIM_1:22; then consider L being Subset of TM such that A11: L separates A,B and A12: L misses bb by A1, A2, A4, A7, A8, TOPDIM_1:37; take L ; ::_thesis: ( L separates A,B & ind (L /\ H) <= n - 1 ) ( L /\ H misses bb & L /\ H c= H ) by A10, A12, XBOOLE_1:17, XBOOLE_1:76; then ( aa is finite-ind & L /\ H c= aa ) by A4, A9, TOPDIM_1:22, XBOOLE_1:73; then ( ind a = ind aa & ind (L /\ H) <= ind aa ) by TOPDIM_1:19, TOPDIM_1:21; hence ( L separates A,B & ind (L /\ H) <= n - 1 ) by A6, A11, XXREAL_0:2; ::_thesis: verum end; theorem :: TOPDIM_2:12 for n being Nat for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds for A, B being Subset of TM st A is closed & B is closed & A misses B holds ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) proof let n be Nat; ::_thesis: for TM being metrizable TopSpace st TM is finite-ind & TM is second-countable & ind TM <= n holds for A, B being Subset of TM st A is closed & B is closed & A misses B holds ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) let TM be metrizable TopSpace; ::_thesis: ( TM is finite-ind & TM is second-countable & ind TM <= n implies for A, B being Subset of TM st A is closed & B is closed & A misses B holds ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) ) assume that A1: ( TM is finite-ind & TM is second-countable ) and A2: ind TM <= n ; ::_thesis: for A, B being Subset of TM st A is closed & B is closed & A misses B holds ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) A3: TM | ([#] TM) is second-countable by A1; let A, B be Subset of TM; ::_thesis: ( A is closed & B is closed & A misses B implies ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) ) assume that A4: ( A is closed & B is closed ) and A5: A misses B ; ::_thesis: ex L being Subset of TM st ( L separates A,B & ind L <= n - 1 ) consider L being Subset of TM such that A6: ( L separates A,B & ind (L /\ ([#] TM)) <= n - 1 ) by A4, A1, A2, A3, A5, Th11; take L ; ::_thesis: ( L separates A,B & ind L <= n - 1 ) thus ( L separates A,B & ind L <= n - 1 ) by A6, XBOOLE_1:28; ::_thesis: verum end; theorem Th13: :: TOPDIM_2:13 for n being Nat for TM being metrizable TopSpace for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) ) proof let n be Nat; ::_thesis: for TM being metrizable TopSpace for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) ) let TM be metrizable TopSpace; ::_thesis: for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & H /\ (Fr W) is finite-ind & ind (H /\ (Fr W)) <= n - 1 ) ) let M be Subset of TM; ::_thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) assume A1: TM | M is second-countable ; ::_thesis: ( ( M is finite-ind & ind M <= n ) iff for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) hereby ::_thesis: ( ( for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) implies ( M is finite-ind & ind M <= n ) ) assume that A2: M is finite-ind and A3: ind M <= n ; ::_thesis: for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) let p be Point of TM; ::_thesis: for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) let U be open Subset of TM; ::_thesis: ( p in U implies ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) assume A4: p in U ; ::_thesis: ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) reconsider P = {p} as Subset of TM by A4, ZFMISC_1:31; ( not TM is empty & not p in U ` ) by A4, XBOOLE_0:def_5; then consider L being Subset of TM such that A5: L separates P,U ` and A6: ind (L /\ M) <= n - 1 by A1, A2, A3, Th11, ZFMISC_1:50; consider W, W1 being open Subset of TM such that A7: P c= W and A8: U ` c= W1 and A9: W misses W1 and A10: L = (W \/ W1) ` by A5, METRIZTS:def_3; take W = W; ::_thesis: ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ( W c= W1 ` & W1 ` c= (U `) ` ) by A8, A9, SUBSET_1:12, SUBSET_1:23; hence ( p in W & W c= U ) by A7, XBOOLE_1:1, ZFMISC_1:31; ::_thesis: ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) Cl W misses W1 by A9, TSEP_1:36; then (Cl W) \ W1 = Cl W by XBOOLE_1:83; then Fr W = ((Cl W) \ W1) \ W by TOPS_1:42 .= (Cl W) \ (W \/ W1) by XBOOLE_1:41 .= (Cl W) /\ L by A10, SUBSET_1:13 ; then Fr W c= L by XBOOLE_1:17; then A11: M /\ (Fr W) c= M /\ L by XBOOLE_1:27; M /\ L c= M by XBOOLE_1:17; then A12: M /\ L is finite-ind by A2, TOPDIM_1:19; then ind (M /\ (Fr W)) <= ind (M /\ L) by A11, TOPDIM_1:19; hence ( M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A6, A11, A12, TOPDIM_1:19, XXREAL_0:2; ::_thesis: verum end; set Tm = TM | M; assume A13: for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ; ::_thesis: ( M is finite-ind & ind M <= n ) A14: for p being Point of (TM | M) for U being open Subset of (TM | M) st p in U holds ex W being open Subset of (TM | M) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) proof A15: [#] (TM | M) = M by PRE_TOPC:def_5; let p be Point of (TM | M); ::_thesis: for U being open Subset of (TM | M) st p in U holds ex W being open Subset of (TM | M) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) let U be open Subset of (TM | M); ::_thesis: ( p in U implies ex W being open Subset of (TM | M) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) ) assume A16: p in U ; ::_thesis: ex W being open Subset of (TM | M) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) p in M by A15, A16; then reconsider p9 = p as Point of TM ; consider U9 being Subset of TM such that A17: U9 is open and A18: U = U9 /\ the carrier of (TM | M) by TSP_1:def_1; p9 in U9 by A16, A18, XBOOLE_0:def_4; then consider W9 being open Subset of TM such that A19: ( p9 in W9 & W9 c= U9 ) and A20: M /\ (Fr W9) is finite-ind and A21: ind (M /\ (Fr W9)) <= n - 1 by A13, A17; reconsider W = W9 /\ the carrier of (TM | M) as Subset of (TM | M) by XBOOLE_1:17; reconsider W = W as open Subset of (TM | M) by TSP_1:def_1; take W ; ::_thesis: ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= n - 1 ) thus ( p in W & W c= U ) by A16, A18, A19, XBOOLE_0:def_4, XBOOLE_1:26; ::_thesis: ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) reconsider FrW = Fr W as Subset of TM by A15, XBOOLE_1:1; A22: FrW c= (Fr W9) /\ M by A15, TOPDIM_1:1; then A23: FrW is finite-ind by A20, TOPDIM_1:19; ind FrW <= ind ((Fr W9) /\ M) by A20, A22, TOPDIM_1:19; then ind (Fr W) <= ind ((Fr W9) /\ M) by A23, TOPDIM_1:21; hence ( Fr W is finite-ind & ind (Fr W) <= n - 1 ) by A21, A23, TOPDIM_1:21, XXREAL_0:2; ::_thesis: verum end; then A24: TM | M is finite-ind by TOPDIM_1:15; then A25: M is finite-ind by TOPDIM_1:18; ind (TM | M) <= n by A14, A24, TOPDIM_1:16; hence ( M is finite-ind & ind M <= n ) by A25, TOPDIM_1:17; ::_thesis: verum end; theorem :: TOPDIM_2:14 for n being Nat for TM being metrizable TopSpace for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) ) proof let n be Nat; ::_thesis: for TM being metrizable TopSpace for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) ) let TM be metrizable TopSpace; ::_thesis: for H being Subset of TM st TM | H is second-countable holds ( ( H is finite-ind & ind H <= n ) iff ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( H /\ (Fr A) is finite-ind & ind (H /\ (Fr A)) <= n - 1 ) ) set cTM = [#] TM; set TOP = the topology of TM; let M be Subset of TM; ::_thesis: ( TM | M is second-countable implies ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ) ) assume A1: TM | M is second-countable ; ::_thesis: ( ( M is finite-ind & ind M <= n ) iff ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ) hereby ::_thesis: ( ex Bas being Basis of TM st for A being Subset of TM st A in Bas holds ( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) implies ( M is finite-ind & ind M <= n ) ) defpred S1[ set , set ] means for p being Point of TM for A being Subset of TM st $1 = [p,A] holds ( $2 in the topology of TM & ( not p in A implies $2 = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = $2 & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ); assume A2: ( M is finite-ind & ind M <= n ) ; ::_thesis: ex RNG being Basis of TM st for B being Subset of TM st B in RNG holds ( M /\ (Fr b4) is finite-ind & ind (M /\ (Fr b4)) <= n - 1 ) A3: for x being set st x in [:([#] TM), the topology of TM:] holds ex y being set st S1[x,y] proof let x be set ; ::_thesis: ( x in [:([#] TM), the topology of TM:] implies ex y being set st S1[x,y] ) assume A4: x in [:([#] TM), the topology of TM:] ; ::_thesis: ex y being set st S1[x,y] consider p9, A9 being set such that A5: p9 in [#] TM and A6: A9 in the topology of TM and A7: x = [p9,A9] by A4, ZFMISC_1:def_2; reconsider A9 = A9 as open Subset of TM by A6, PRE_TOPC:def_2; reconsider p9 = p9 as Point of TM by A5; percases ( not p9 in A9 or p9 in A9 ) ; supposeA8: not p9 in A9 ; ::_thesis: ex y being set st S1[x,y] take {} TM ; ::_thesis: S1[x, {} TM] let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) ) assume A9: x = [p,A] ; ::_thesis: ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) p = p9 by A7, A9, XTUPLE_0:1; hence ( {} TM in the topology of TM & ( not p in A implies {} TM = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = {} TM & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A7, A8, A9, PRE_TOPC:def_2, XTUPLE_0:1; ::_thesis: verum end; suppose p9 in A9 ; ::_thesis: ex y being set st S1[x,y] then consider W being open Subset of TM such that A10: ( p9 in W & W c= A9 & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A1, A2, Th13; take W ; ::_thesis: S1[x,W] let p be Point of TM; ::_thesis: for A being Subset of TM st x = [p,A] holds ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) let A be Subset of TM; ::_thesis: ( x = [p,A] implies ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) ) assume A11: x = [p,A] ; ::_thesis: ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) ( p = p9 & A = A9 ) by A7, A11, XTUPLE_0:1; hence ( W in the topology of TM & ( not p in A implies W = {} TM ) & ( p in A implies ex W being open Subset of TM st ( W = W & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) ) by A10, PRE_TOPC:def_2; ::_thesis: verum end; end; end; consider f being Function such that A12: dom f = [:([#] TM), the topology of TM:] and A13: for x being set st x in [:([#] TM), the topology of TM:] holds S1[x,f . x] from CLASSES1:sch_1(A3); A14: rng f c= the topology of TM proof let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng f or y in the topology of TM ) assume y in rng f ; ::_thesis: y in the topology of TM then consider x being set such that A15: x in dom f and A16: f . x = y by FUNCT_1:def_3; ex p, A being set st ( p in [#] TM & A in the topology of TM & x = [p,A] ) by A12, A15, ZFMISC_1:def_2; hence y in the topology of TM by A12, A13, A15, A16; ::_thesis: verum end; then reconsider RNG = rng f as Subset-Family of TM by XBOOLE_1:1; now__::_thesis:_for_A_being_Subset_of_TM_st_A_is_open_holds_ for_p_being_Point_of_TM_st_p_in_A_holds_ ex_W_being_Subset_of_TM_st_ (_W_in_RNG_&_p_in_W_&_W_c=_A_) let A be Subset of TM; ::_thesis: ( A is open implies for p being Point of TM st p in A holds ex W being Subset of TM st ( W in RNG & p in W & W c= A ) ) assume A17: A is open ; ::_thesis: for p being Point of TM st p in A holds ex W being Subset of TM st ( W in RNG & p in W & W c= A ) A18: A in the topology of TM by A17, PRE_TOPC:def_2; let p be Point of TM; ::_thesis: ( p in A implies ex W being Subset of TM st ( W in RNG & p in W & W c= A ) ) assume A19: p in A ; ::_thesis: ex W being Subset of TM st ( W in RNG & p in W & W c= A ) A20: [p,A] in [:([#] TM), the topology of TM:] by A18, A19, ZFMISC_1:87; then consider W being open Subset of TM such that A21: ( W = f . [p,A] & p in W & W c= A ) and M /\ (Fr W) is finite-ind and ind (M /\ (Fr W)) <= n - 1 by A13, A19; reconsider W = W as Subset of TM ; take W = W; ::_thesis: ( W in RNG & p in W & W c= A ) thus ( W in RNG & p in W & W c= A ) by A12, A20, A21, FUNCT_1:def_3; ::_thesis: verum end; then reconsider RNG = RNG as Basis of TM by A14, YELLOW_9:32; take RNG = RNG; ::_thesis: for B being Subset of TM st B in RNG holds ( M /\ (Fr b3) is finite-ind & ind (M /\ (Fr b3)) <= n - 1 ) let B be Subset of TM; ::_thesis: ( B in RNG implies ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 ) ) assume B in RNG ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 ) then consider x being set such that A22: x in dom f and A23: f . x = B by FUNCT_1:def_3; consider p, A being set such that A24: p in [#] TM and A25: A in the topology of TM and A26: x = [p,A] by A12, A22, ZFMISC_1:def_2; reconsider A = A as open Subset of TM by A25, PRE_TOPC:def_2; percases ( p in A or not p in A ) ; suppose p in A ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 ) then ex W being open Subset of TM st ( W = f . [p,A] & p in W & W c= A & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) by A12, A13, A22, A26; hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A23, A26; ::_thesis: verum end; suppose not p in A ; ::_thesis: ( M /\ (Fr b2) is finite-ind & ind (M /\ (Fr b2)) <= n - 1 ) then B = {} TM by A12, A13, A22, A23, A24, A26; then A27: Fr B = {} by TOPGEN_1:14; 0 - 1 <= n - 1 by XREAL_1:9; hence ( M /\ (Fr B) is finite-ind & ind (M /\ (Fr B)) <= n - 1 ) by A27, TOPDIM_1:6; ::_thesis: verum end; end; end; given B being Basis of TM such that A28: for A being Subset of TM st A in B holds ( M /\ (Fr A) is finite-ind & ind (M /\ (Fr A)) <= n - 1 ) ; ::_thesis: ( M is finite-ind & ind M <= n ) for p being Point of TM for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) proof let p be Point of TM; ::_thesis: for U being open Subset of TM st p in U holds ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) let U be open Subset of TM; ::_thesis: ( p in U implies ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) ) assume A29: p in U ; ::_thesis: ex W being open Subset of TM st ( p in W & W c= U & M /\ (Fr W) is finite-ind & ind (M /\ (Fr W)) <= n - 1 ) consider a being Subset of TM such that A30: a in B and A31: ( p in a & a c= U ) by A29, YELLOW_9:31; B c= the topology of TM by TOPS_2:64; then reconsider a = a as open Subset of TM by A30, PRE_TOPC:def_2; take a ; ::_thesis: ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) thus ( p in a & a c= U & M /\ (Fr a) is finite-ind & ind (M /\ (Fr a)) <= n - 1 ) by A28, A30, A31; ::_thesis: verum end; hence ( M is finite-ind & ind M <= n ) by A1, Th13; ::_thesis: verum end; theorem :: TOPDIM_2:15 for TM1, TM2 being second-countable finite-ind metrizable TopSpace st ( not TM1 is empty or not TM2 is empty ) holds ind [:TM1,TM2:] <= (ind TM1) + (ind TM2) by Lm5; theorem :: TOPDIM_2:16 for TM2, TM1 being second-countable finite-ind metrizable TopSpace st ind TM2 = 0 holds ind [:TM1,TM2:] = ind TM1 proof let TM2, TM1 be second-countable finite-ind metrizable TopSpace; ::_thesis: ( ind TM2 = 0 implies ind [:TM1,TM2:] = ind TM1 ) assume A1: ind TM2 = 0 ; ::_thesis: ind [:TM1,TM2:] = ind TM1 then A2: not TM2 is empty by TOPDIM_1:6; then A3: ind [:TM1,TM2:] <= (ind TM1) + 0 by A1, Lm5; set x = the Point of TM2; reconsider X = { the Point of TM2} as Subset of TM2 by A2, ZFMISC_1:31; percases ( TM1 is empty or not TM1 is empty ) ; supposeA4: TM1 is empty ; ::_thesis: ind [:TM1,TM2:] = ind TM1 then ind TM1 = - 1 by TOPDIM_1:6; hence ind [:TM1,TM2:] = ind TM1 by A4, TOPDIM_1:6; ::_thesis: verum end; suppose not TM1 is empty ; ::_thesis: ind [:TM1,TM2:] = ind TM1 then ind [:(TM2 | X),TM1:] = ind TM1 by A2, BORSUK_3:13, TOPDIM_1:25; then A5: ind [:TM1,(TM2 | X):] = ind TM1 by TOPDIM_1:28; A6: [:TM1,(TM2 | X):] is SubSpace of [:TM1,TM2:] by BORSUK_3:15; then [#] [:TM1,(TM2 | X):] c= [#] [:TM1,TM2:] by PRE_TOPC:def_4; then reconsider cT12 = [#] [:TM1,(TM2 | X):] as Subset of [:TM1,TM2:] ; [:TM1,(TM2 | X):] = [:TM1,TM2:] | cT12 by A6, PRE_TOPC:def_5; then ind cT12 = ind TM1 by A5, TOPDIM_1:17; then ind TM1 <= ind [:TM1,TM2:] by TOPDIM_1:19; hence ind [:TM1,TM2:] = ind TM1 by A3, XXREAL_0:1; ::_thesis: verum end; end; end; begin theorem Th17: :: TOPDIM_2:17 for u being Point of (Euclid 1) for u1, r being real number st <*u1*> = u holds cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } proof let u be Point of (Euclid 1); ::_thesis: for u1, r being real number st <*u1*> = u holds cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } let u1, r be real number ; ::_thesis: ( <*u1*> = u implies cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ) assume A1: <*u1*> = u ; ::_thesis: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } set E1 = { q where q is Element of (Euclid 1) : dist (u,q) <= r } ; reconsider u1 = u1 as Real by XREAL_0:def_1; set R1 = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ; A2: { q where q is Element of (Euclid 1) : dist (u,q) <= r } c= { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } or x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ) assume x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } ; ::_thesis: x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } then consider q being Element of (Euclid 1) such that A3: x = q and A4: dist (u,q) <= r ; q is Tuple of 1, REAL by FINSEQ_2:131; then consider s1 being Real such that A5: q = <*s1*> by FINSEQ_2:97; <*u1*> - <*s1*> = <*(u1 - s1)*> by RVSUM_1:29; then sqr (<*u1*> - <*s1*>) = <*((u1 - s1) ^2)*> by RVSUM_1:55; then Sum (sqr (<*u1*> - <*s1*>)) = (u1 - s1) ^2 by RVSUM_1:73; then A6: sqrt (Sum (sqr (<*u1*> - <*s1*>))) = abs (u1 - s1) by COMPLEX1:72; A7: |.(<*u1*> - <*s1*>).| <= r by A1, A4, A5, EUCLID:def_6; then u1 - s1 <= r by A6, ABSVALUE:5; then (u1 - s1) + s1 <= r + s1 by XREAL_1:6; then A8: u1 - r <= (r + s1) - r by XREAL_1:9; - r <= u1 - s1 by A6, A7, ABSVALUE:5; then (- r) + s1 <= (u1 - s1) + s1 by XREAL_1:6; then (s1 - r) + r <= u1 + r by XREAL_1:6; hence x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A3, A5, A8; ::_thesis: verum end; { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } c= { q where q is Element of (Euclid 1) : dist (u,q) <= r } proof reconsider eu1 = <*u1*> as Element of REAL 1 by FINSEQ_2:98; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } or x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } ) assume x in { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } ; ::_thesis: x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } then consider s being Real such that A9: x = <*s*> and A10: u1 - r <= s and A11: s <= u1 + r ; s - r <= (u1 + r) - r by A11, XREAL_1:9; then A12: (s + (- r)) - s <= u1 - s by XREAL_1:9; reconsider es = <*s*> as Element of REAL 1 by FINSEQ_2:98; reconsider q1 = <*s*> as Element of (Euclid 1) by FINSEQ_2:98; <*u1*> - <*s*> = <*(u1 - s)*> by RVSUM_1:29; then sqr (<*u1*> - <*s*>) = <*((u1 - s) ^2)*> by RVSUM_1:55; then A13: Sum (sqr (<*u1*> - <*s*>)) = (u1 - s) ^2 by RVSUM_1:73; (u1 - r) + r <= s + r by A10, XREAL_1:6; then u1 - s <= (s + r) - s by XREAL_1:9; then abs (u1 - s) <= r by A12, ABSVALUE:5; then |.(<*u1*> - <*s*>).| <= r by A13, COMPLEX1:72; then ( the distance of (Euclid 1) . (u,q1) = dist (u,q1) & (Pitag_dist 1) . (eu1,es) <= r ) by EUCLID:def_6; hence x in { q where q is Element of (Euclid 1) : dist (u,q) <= r } by A1, A9; ::_thesis: verum end; then { q where q is Element of (Euclid 1) : dist (u,q) <= r } = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A2, XBOOLE_0:def_10; hence cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by METRIC_1:18; ::_thesis: verum end; Lm6: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8; theorem Th18: :: TOPDIM_2:18 for U being Point of (TOP-REAL 1) for u1, r being real number st <*u1*> = U & r > 0 holds Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} proof let U be Point of (TOP-REAL 1); ::_thesis: for u1, r being real number st <*u1*> = U & r > 0 holds Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} let u1, r be real number ; ::_thesis: ( <*u1*> = U & r > 0 implies Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} ) assume that A1: <*u1*> = U and A2: r > 0 ; ::_thesis: Fr (Ball (U,r)) = {<*(u1 - r)*>,<*(u1 + r)*>} reconsider u = U as Point of (Euclid 1) by Lm6; A3: Ball (u,r) = { <*s*> where s is Real : ( u1 - r < s & s < u1 + r ) } by A1, JORDAN2B:27; Ball (U,r) = Ball (u,r) by TOPREAL9:13; then Ball (U,r) is open by KURATO_2:1; then A4: Fr (Ball (U,r)) = (Cl (Ball (U,r))) \ (Ball (U,r)) by TOPS_1:42 .= (cl_Ball (U,r)) \ (Ball (U,r)) by A2, JORDAN:23 .= (cl_Ball (u,r)) \ (Ball (U,r)) by TOPREAL9:14 .= (cl_Ball (u,r)) \ (Ball (u,r)) by TOPREAL9:13 ; A5: cl_Ball (u,r) = { <*s*> where s is Real : ( u1 - r <= s & s <= u1 + r ) } by A1, Th17; thus Fr (Ball (U,r)) c= {<*(u1 - r)*>,<*(u1 + r)*>} :: according to XBOOLE_0:def_10 ::_thesis: {<*(u1 - r)*>,<*(u1 + r)*>} c= Fr (Ball (U,r)) proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in Fr (Ball (U,r)) or x in {<*(u1 - r)*>,<*(u1 + r)*>} ) assume A6: x in Fr (Ball (U,r)) ; ::_thesis: x in {<*(u1 - r)*>,<*(u1 + r)*>} reconsider X = x as Point of (Euclid 1) by Lm6, A6; x in cl_Ball (u,r) by A4, A6, XBOOLE_0:def_5; then consider s being Real such that A7: x = <*s*> and A8: u1 - r <= s and A9: s <= u1 + r by A5; assume A10: not x in {<*(u1 - r)*>,<*(u1 + r)*>} ; ::_thesis: contradiction then s <> u1 + r by A7, TARSKI:def_2; then A11: s < u1 + r by A9, XXREAL_0:1; s <> u1 - r by A7, A10, TARSKI:def_2; then u1 - r < s by A8, XXREAL_0:1; then X in Ball (u,r) by A3, A7, A11; hence contradiction by A4, A6, XBOOLE_0:def_5; ::_thesis: verum end; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in {<*(u1 - r)*>,<*(u1 + r)*>} or x in Fr (Ball (U,r)) ) assume x in {<*(u1 - r)*>,<*(u1 + r)*>} ; ::_thesis: x in Fr (Ball (U,r)) then A12: ( x = <*(u1 - r)*> or x = <*(u1 + r)*> ) by TARSKI:def_2; A13: ( u1 - r is Real & u1 + r is Real ) by XREAL_0:def_1; assume A14: not x in Fr (Ball (U,r)) ; ::_thesis: contradiction u1 + (- r) <= u1 + r by A2, XREAL_1:6; then x in cl_Ball (u,r) by A5, A12, A13; then x in Ball (u,r) by A4, A14, XBOOLE_0:def_5; then ex s being Real st ( x = <*s*> & u1 - r < s & s < u1 + r ) by A3; hence contradiction by A12, FINSEQ_1:76; ::_thesis: verum end; theorem Th19: :: TOPDIM_2:19 for T being TopSpace for A being countable Subset of T st T | A is T_4 holds ( A is finite-ind & ind A <= 0 ) proof let T be TopSpace; ::_thesis: for A being countable Subset of T st T | A is T_4 holds ( A is finite-ind & ind A <= 0 ) let A be countable Subset of T; ::_thesis: ( T | A is T_4 implies ( A is finite-ind & ind A <= 0 ) ) assume A1: T | A is T_4 ; ::_thesis: ( A is finite-ind & ind A <= 0 ) percases ( A = {} T or not A is empty ) ; suppose A = {} T ; ::_thesis: ( A is finite-ind & ind A <= 0 ) hence ( A is finite-ind & ind A <= 0 ) by TOPDIM_1:6; ::_thesis: verum end; supposeA2: not A is empty ; ::_thesis: ( A is finite-ind & ind A <= 0 ) then reconsider TT = T as non empty TopSpace ; reconsider a = A as non empty Subset of TT by A2; set Ta = TT | a; deffunc H1( Point of (TT | a)) -> Element of bool the carrier of (TT | a) = {$1}; defpred S1[ set ] means verum; defpred S2[ set ] means ( $1 in A & S1[$1] ); consider S being Subset-Family of (TT | a) such that A3: S = { H1(w) where w is Point of (TT | a) : S2[w] } from LMOD_7:sch_5(); for B being Subset of (TT | a) st B in S holds ( B is finite-ind & ind B <= 0 ) proof let B be Subset of (TT | a); ::_thesis: ( B in S implies ( B is finite-ind & ind B <= 0 ) ) assume B in S ; ::_thesis: ( B is finite-ind & ind B <= 0 ) then consider w being Point of (TT | a) such that A4: B = H1(w) and S2[w] by A3; card H1(w) = 1 by CARD_1:30; then ind H1(w) < 1 + 0 by TOPDIM_1:8; hence ( B is finite-ind & ind B <= 0 ) by A4, INT_1:7; ::_thesis: verum end; then A5: ( S is finite-ind & ind S <= 0 ) by TOPDIM_1:11; [#] (TT | a) c= union S proof let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] (TT | a) or x in union S ) assume A6: x in [#] (TT | a) ; ::_thesis: x in union S then x in a by PRE_TOPC:def_5; then ( x in {x} & {x} in S ) by A3, A6, TARSKI:def_1; hence x in union S by TARSKI:def_4; ::_thesis: verum end; then A7: S is Cover of (TT | a) by SETFAM_1:def_11; A8: S is closed proof let B be Subset of (TT | a); :: according to TOPS_2:def_2 ::_thesis: ( not B in S or B is closed ) assume B in S ; ::_thesis: B is closed then ex w being Point of (TT | a) st ( B = H1(w) & S2[w] ) by A3; hence B is closed by A1; ::_thesis: verum end; A9: card A c= omega by CARD_3:def_14; card { H1(w) where w is Point of (TT | a) : S2[w] } c= card A from BORSUK_2:sch_1(); then card S c= omega by A3, A9, XBOOLE_1:1; then A10: S is countable by CARD_3:def_14; [#] (TT | a) = A by PRE_TOPC:def_5; then A11: TT | a is countable by ORDERS_4:def_2; then TT | a is finite-ind by A1, A5, A7, A8, A10, TOPDIM_1:36; then A12: A is finite-ind by TOPDIM_1:18; ind (TT | a) <= 0 by A1, A5, A7, A8, A10, A11, TOPDIM_1:36; hence ( A is finite-ind & ind A <= 0 ) by A12, TOPDIM_1:17; ::_thesis: verum end; end; end; registration let TM be metrizable TopSpace; cluster countable -> finite-ind for Element of bool the carrier of TM; coherence for b1 being Subset of TM st b1 is countable holds b1 is finite-ind proof let A be Subset of TM; ::_thesis: ( A is countable implies A is finite-ind ) assume A1: A is countable ; ::_thesis: A is finite-ind TM | A is T_4 ; hence A is finite-ind by A1, Th19; ::_thesis: verum end; end; Lm7: ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 ) proof set T = TOP-REAL 0; TopStruct(# the carrier of (TOP-REAL 0), the topology of (TOP-REAL 0) #) = TopSpaceMetr (Euclid 0) by EUCLID:def_8; then A1: [#] (TOP-REAL 0) = {(<*> REAL)} by FINSEQ_2:94; card {(<*> REAL)} = 1 by CARD_1:30; then ind ([#] (TOP-REAL 0)) < 1 by A1, TOPDIM_1:8; hence ( TOP-REAL 0 is finite-ind & ind (TOP-REAL 0) = 0 ) by A1, NAT_1:25, TOPDIM_1:def_4; ::_thesis: verum end; Lm8: ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) proof set T = TOP-REAL 1; A1: for p being Point of (TOP-REAL 1) for U being open Subset of (TOP-REAL 1) st p in U holds ex W being open Subset of (TOP-REAL 1) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) proof let p be Point of (TOP-REAL 1); ::_thesis: for U being open Subset of (TOP-REAL 1) st p in U holds ex W being open Subset of (TOP-REAL 1) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) let U be open Subset of (TOP-REAL 1); ::_thesis: ( p in U implies ex W being open Subset of (TOP-REAL 1) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) ) assume A2: p in U ; ::_thesis: ex W being open Subset of (TOP-REAL 1) st ( p in W & W c= U & Fr W is finite-ind & ind (Fr W) <= 1 - 1 ) reconsider p9 = p as Point of (Euclid 1) by Lm6; set M = Euclid 1; A3: TopStruct(# the carrier of (TopSpaceMetr (Euclid 1)), the topology of (TopSpaceMetr (Euclid 1)) #) = TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) by EUCLID:def_8; then reconsider V = U as Subset of (TopSpaceMetr (Euclid 1)) ; V is open by A3, PRE_TOPC:30; then consider r being real number such that A4: r > 0 and A5: Ball (p9,r) c= U by A2, TOPMETR:15; reconsider B = Ball (p9,r) as open Subset of (TOP-REAL 1) by KURATO_2:1; take B ; ::_thesis: ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 ) p9 is Tuple of 1, REAL by FINSEQ_2:131; then consider p1 being Real such that A6: p9 = <*p1*> by FINSEQ_2:97; A7: Ball (p,r) = Ball (p9,r) by TOPREAL9:13; then A8: Fr B = {<*(p1 - r)*>,<*(p1 + r)*>} by A4, A6, Th18; TOP-REAL 1 is metrizable proof ex f being Function of [: the carrier of (TOP-REAL 1), the carrier of (TOP-REAL 1):],REAL st ( f is_metric_of the carrier of (TOP-REAL 1) & Family_open_set (SpaceMetr ( the carrier of (TOP-REAL 1),f)) = the topology of (TOP-REAL 1) ) by A3, PCOMPS_1:def_8; hence TOP-REAL 1 is metrizable by PCOMPS_1:def_8; ::_thesis: verum end; then (TOP-REAL 1) | (Fr B) is metrizable ; hence ( p in B & B c= U & Fr B is finite-ind & ind (Fr B) <= 1 - 1 ) by A4, A5, A7, Th19, A8, JORDAN:16; ::_thesis: verum end; then A9: TOP-REAL 1 is finite-ind by TOPDIM_1:15; A10: ind (TOP-REAL 1) >= 1 proof reconsider p = <*0*>, q = <*1*> as Point of (Euclid 1) by FINSEQ_2:98; TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8; then reconsider p9 = p as Point of (TOP-REAL 1) ; A11: Ball (p,1) = Ball (p9,1) by TOPREAL9:13; then reconsider B = Ball (p9,1) as open Subset of (TOP-REAL 1) by KURATO_2:1; assume ind (TOP-REAL 1) < 1 ; ::_thesis: contradiction then ind (TOP-REAL 1) < 1 + 0 ; then A12: ind (TOP-REAL 1) <= 0 by INT_1:7; p in B by JORDAN:16; then consider W being open Subset of (TOP-REAL 1) such that A13: p in W and A14: W c= B and A15: ( Fr W is finite-ind & ind (Fr W) <= 0 - 1 ) by A9, A12, TOPDIM_1:16; Fr W = {} (TOP-REAL 1) by A15; then A16: W is closed by TOPGEN_1:14; A17: W \/ (W `) = [#] (TOP-REAL 1) by PRE_TOPC:2; W misses W ` by SUBSET_1:24; then ( [#] (TOP-REAL 1) is convex & W,W ` are_separated ) by A16, CONNSP_1:2; then A18: W ` = {} (TOP-REAL 1) by A13, A17, CONNSP_1:15; A19: B = { <*s*> where s is Real : ( 0 - 1 < s & s < 0 + 1 ) } by A11, JORDAN2B:27; A20: TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) by EUCLID:def_8; not q in B proof assume q in B ; ::_thesis: contradiction then ex s being Real st ( q = <*s*> & 0 - 1 < s & s < 0 + 1 ) by A19; hence contradiction by FINSEQ_1:76; ::_thesis: verum end; then not q in W by A14; hence contradiction by A20, A18, XBOOLE_0:def_5; ::_thesis: verum end; ind (TOP-REAL 1) <= 1 by A1, A9, TOPDIM_1:16; hence ( TOP-REAL 1 is finite-ind & ind (TOP-REAL 1) = 1 ) by A1, A10, TOPDIM_1:15, XXREAL_0:1; ::_thesis: verum end; Lm9: for n being Nat holds ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n ) proof let n be Nat; ::_thesis: ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n ) defpred S1[ Nat] means ( TOP-REAL $1 is finite-ind & ind (TOP-REAL $1) <= $1 ); A1: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) A2: ( TopStruct(# the carrier of (TOP-REAL n), the topology of (TOP-REAL n) #) = TopSpaceMetr (Euclid n) & TopStruct(# the carrier of (TOP-REAL (n + 1)), the topology of (TOP-REAL (n + 1)) #) = TopSpaceMetr (Euclid (n + 1)) & TopStruct(# the carrier of (TOP-REAL 1), the topology of (TOP-REAL 1) #) = TopSpaceMetr (Euclid 1) ) by EUCLID:def_8; A3: n in NAT by ORDINAL1:def_12; then A4: [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):], TopSpaceMetr (Euclid (n + 1)) are_homeomorphic by TOPREAL7:25; TOP-REAL 1, TopSpaceMetr (Euclid 1) are_homeomorphic by A2, YELLOW14:19; then A5: ( TopSpaceMetr (Euclid 1) is finite-ind & ind (TopSpaceMetr (Euclid 1)) = 1 ) by Lm8, TOPDIM_1:24, TOPDIM_1:25; assume A6: S1[n] ; ::_thesis: S1[n + 1] A7: TOP-REAL n, TopSpaceMetr (Euclid n) are_homeomorphic by A2, YELLOW14:19; A8: TOP-REAL (n + 1), TopSpaceMetr (Euclid (n + 1)) are_homeomorphic by A2, YELLOW14:19; A9: ( TopSpaceMetr (Euclid n) is finite-ind & ind (TopSpaceMetr (Euclid n)) = ind (TOP-REAL n) ) by A6, A7, TOPDIM_1:24, TOPDIM_1:25; then A10: ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= (ind (TopSpaceMetr (Euclid n))) + 1 by Lm5, A2, A5; (ind (TopSpaceMetr (Euclid n))) + 1 <= n + 1 by A6, A9, XREAL_1:6; then ind [:(TopSpaceMetr (Euclid n)),(TopSpaceMetr (Euclid 1)):] <= n + 1 by A10, XXREAL_0:2; then A11: ind (TopSpaceMetr (Euclid (n + 1))) <= n + 1 by A3, A9, A5, A2, TOPDIM_1:25, TOPREAL7:25; TopSpaceMetr (Euclid (n + 1)) is finite-ind by A9, A5, A2, A4, TOPDIM_1:24; then TOP-REAL (n + 1) is finite-ind by A8, TOPDIM_1:24; hence S1[n + 1] by A11, A2, TOPDIM_1:25, YELLOW14:19; ::_thesis: verum end; A12: S1[ 0 ] by Lm7; for n being Nat holds S1[n] from NAT_1:sch_2(A12, A1); hence ( TOP-REAL n is finite-ind & ind (TOP-REAL n) <= n ) ; ::_thesis: verum end; registration let n be Nat; cluster TOP-REAL n -> finite-ind ; coherence TOP-REAL n is with_finite_small_inductive_dimension by Lm9; end; theorem :: TOPDIM_2:20 for n being Nat st n <= 1 holds ind (TOP-REAL n) = n proof let n be Nat; ::_thesis: ( n <= 1 implies ind (TOP-REAL n) = n ) assume n <= 1 ; ::_thesis: ind (TOP-REAL n) = n then ( n < 1 or n = 1 ) by XXREAL_0:1; then ( n = 0 or n = 1 ) by NAT_1:14; hence ind (TOP-REAL n) = n by Lm7, Lm8; ::_thesis: verum end; theorem :: TOPDIM_2:21 for n being Nat holds ind (TOP-REAL n) <= n by Lm9; Lm10: for TM being metrizable TopSpace for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) proof let TM be metrizable TopSpace; ::_thesis: for A being finite-ind Subset of TM st TM | A is second-countable & ind (TM | A) <= 0 holds for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) let A be finite-ind Subset of TM; ::_thesis: ( TM | A is second-countable & ind (TM | A) <= 0 implies for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) ) assume A1: ( TM | A is second-countable & ind (TM | A) <= 0 ) ; ::_thesis: for U1, U2 being open Subset of TM st A c= U1 \/ U2 holds ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) let U1, U2 be open Subset of TM; ::_thesis: ( A c= U1 \/ U2 implies ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) ) assume A2: A c= U1 \/ U2 ; ::_thesis: ex V1, V2 being open Subset of TM st ( V1 c= U1 & V2 c= U2 & V1 misses V2 & A c= V1 \/ V2 ) set U12 = U1 \/ U2; set TU = TM | (U1 \/ U2); A3: [#] (TM | (U1 \/ U2)) = U1 \/ U2 by PRE_TOPC:def_5; then reconsider u1 = U1, u2 = U2, a = A as Subset of (TM | (U1 \/ U2)) by A2, XBOOLE_1:7; A4: a is finite-ind by TOPDIM_1:21; A5: u1 ` misses u2 ` proof assume u1 ` meets u2 ` ; ::_thesis: contradiction then consider z being set such that A6: z in u1 ` and A7: z in u2 ` by XBOOLE_0:3; ( not z in U1 & not z in U2 ) by A6, A7, XBOOLE_0:def_5; hence contradiction by A3, A6, XBOOLE_0:def_3; ::_thesis: verum end; U2 /\ (U1 \/ U2) = u2 by XBOOLE_1:7, XBOOLE_1:28; then A8: u2 is open by A3, TSP_1:def_1; U1 /\ (U1 \/ U2) = u1 by XBOOLE_1:7, XBOOLE_1:28; then A9: u1 is open by A3, TSP_1:def_1; A10: ind a = ind A by TOPDIM_1:21; ( ind A <= 0 & (TM | (U1 \/ U2)) | a is second-countable ) by A1, METRIZTS:9, TOPDIM_1:17; then consider L being Subset of (TM | (U1 \/ U2)) such that A11: L separates u1 ` ,u2 ` and A12: ind (L /\ a) <= 0 - 1 by A4, A5, A9, A8, A10, Th11; consider v1, v2 being open Subset of (TM | (U1 \/ U2)) such that A13: ( u1 ` c= v1 & u2 ` c= v2 ) and A14: v1 misses v2 and A15: L = (v1 \/ v2) ` by A11, METRIZTS:def_3; reconsider V1 = v1, V2 = v2 as Subset of TM by A3, XBOOLE_1:1; reconsider V1 = V1, V2 = V2 as open Subset of TM by A3, TSEP_1:9; take V2 ; ::_thesis: ex V2 being open Subset of TM st ( V2 c= U1 & V2 c= U2 & V2 misses V2 & A c= V2 \/ V2 ) take V1 ; ::_thesis: ( V2 c= U1 & V1 c= U2 & V2 misses V1 & A c= V2 \/ V1 ) ( u1 ` misses v2 & u2 ` misses v1 ) by A13, A14, XBOOLE_1:63; hence ( V2 c= U1 & V1 c= U2 & V2 misses V1 ) by A14, SUBSET_1:24; ::_thesis: A c= V2 \/ V1 L /\ a c= a by XBOOLE_1:17; then A16: L /\ a is finite-ind by A4, TOPDIM_1:19; then ind (L /\ a) >= - 1 by TOPDIM_1:5; then ind (L /\ a) = - 1 by A12, XXREAL_0:1; then L /\ a is empty by A16, TOPDIM_1:6; then L misses a by XBOOLE_0:def_7; hence A c= V2 \/ V1 by A15, SUBSET_1:24; ::_thesis: verum end; theorem Th22: :: TOPDIM_2:22 for TM being metrizable TopSpace for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds for F being finite Subset-Family of TM st F is open & F is Cover of A holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) proof let TM be metrizable TopSpace; ::_thesis: for A being Subset of TM st TM | A is second-countable & TM | A is finite-ind & ind A <= 0 holds for F being finite Subset-Family of TM st F is open & F is Cover of A holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) defpred S1[ Nat] means for A being Subset of TM st TM | A is second-countable & A is finite-ind & ind A <= 0 holds for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= $1 holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ); let A be Subset of TM; ::_thesis: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume A1: ( TM | A is second-countable & TM | A is finite-ind & ind A <= 0 ) ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A implies ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume A2: ( F is open & F is Cover of A ) ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) A3: for n being Nat st S1[n] holds S1[n + 1] proof let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume A4: S1[n] ; ::_thesis: S1[n + 1] let A be Subset of TM; ::_thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume that A5: TM | A is second-countable and A6: A is finite-ind and A7: ind A <= 0 ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= n + 1 holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A & card F <= n + 1 implies ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume that A8: F is open and A9: F is Cover of A and A10: card F <= n + 1 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) percases ( card F <= n or card F = n + 1 ) by A10, NAT_1:8; suppose card F <= n ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) hence ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) by A4, A5, A6, A7, A8, A9; ::_thesis: verum end; supposeA11: card F = n + 1 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) percases ( n = 0 or n > 0 ) ; suppose n = 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) then consider x being set such that A12: F = {x} by A11, CARD_2:42; set g = F --> x; ( dom (F --> x) = F & rng (F --> x) = F ) by A12, FUNCOP_1:8, FUNCOP_1:13; then reconsider g = F --> x as Function of F,(bool the carrier of TM) by FUNCT_2:2; take g ; ::_thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) thus ( rng g is open & rng g is Cover of A ) by A8, A9, A12, FUNCOP_1:8; ::_thesis: ( ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds g . a misses g . b let a be set ; ::_thesis: ( a in F implies g . a c= a ) assume A13: a in F ; ::_thesis: g . a c= a then g . a = x by FUNCOP_1:7; hence g . a c= a by A12, A13, TARSKI:def_1; ::_thesis: verum end; let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies g . a misses g . b ) assume that A14: a in F and A15: ( b in F & a <> b ) ; ::_thesis: g . a misses g . b x = a by A12, A14, TARSKI:def_1; hence g . a misses g . b by A12, A15, TARSKI:def_1; ::_thesis: verum end; suppose n > 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) then reconsider n1 = n - 1 as Element of NAT by NAT_1:20; not F is empty by A11; then consider x being set such that A16: x in F by XBOOLE_0:def_1; A17: card (F \ {x}) = n1 + 1 by A11, A16, STIRL2_1:55; then not F \ {x} is empty ; then consider y being set such that A18: y in F \ {x} by XBOOLE_0:def_1; y in F by A18, XBOOLE_0:def_5; then reconsider x = x, y = y as open Subset of TM by A8, A16, TOPS_2:def_1; set X = {x}; set xy = x \/ y; set Y = {y}; set XY = {(x \/ y)}; A19: (F \ {x}) \/ {x} = F by A16, ZFMISC_1:116; set Fxy = (F \ {x}) \ {y}; A20: card ((F \ {x}) \ {y}) = n1 by A17, A18, STIRL2_1:55; set FXY = ((F \ {x}) \ {y}) \/ {(x \/ y)}; card {(x \/ y)} = 1 by CARD_1:30; then A21: card (((F \ {x}) \ {y}) \/ {(x \/ y)}) <= n1 + 1 by A20, CARD_2:43; F \ {x} is open by A8, TOPS_2:15; then A22: (F \ {x}) \ {y} is open by TOPS_2:15; A23: ((F \ {x}) \ {y}) \/ {y} = F \ {x} by A18, ZFMISC_1:116; for A being Subset of TM st A in {(x \/ y)} holds A is open by TARSKI:def_1; then A24: {(x \/ y)} is open by TOPS_2:def_1; percases ( (F \ {x}) \ {y} is Cover of A or not (F \ {x}) \ {y} is Cover of A ) ; supposeA25: (F \ {x}) \ {y} is Cover of A ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) card ((F \ {x}) \ {y}) <= n1 + 1 by A20, NAT_1:13; then consider g being Function of ((F \ {x}) \ {y}),(bool the carrier of TM) such that A26: rng g is open and A27: rng g is Cover of A and A28: for a being set st a in (F \ {x}) \ {y} holds g . a c= a and A29: for a, b being set st a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} & a <> b holds g . a misses g . b by A4, A5, A6, A7, A22, A25; A30: A c= union (rng g) by A27, SETFAM_1:def_11; set h = (x,y) --> (({} TM),({} TM)); A31: dom ((x,y) --> (({} TM),({} TM))) = {x,y} by FUNCT_4:62; not x in F \ {x} by ZFMISC_1:56; then A32: not x in (F \ {x}) \ {y} by ZFMISC_1:56; not y in (F \ {x}) \ {y} by ZFMISC_1:56; then A33: (F \ {x}) \ {y} misses {x,y} by A32, ZFMISC_1:51; A34: x <> y by A18, ZFMISC_1:56; then A35: rng ((x,y) --> (({} TM),({} TM))) = {({} TM),({} TM)} by FUNCT_4:64; A36: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1 .= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4 .= F by A18, A19, ZFMISC_1:116 ; A37: dom g = (F \ {x}) \ {y} by FUNCT_2:def_1; then A38: rng (g +* ((x,y) --> (({} TM),({} TM)))) = (rng g) \/ (rng ((x,y) --> (({} TM),({} TM)))) by A31, A33, NECKLACE:6; dom (g +* ((x,y) --> (({} TM),({} TM)))) = ((F \ {x}) \ {y}) \/ {x,y} by A31, A37, FUNCT_4:def_1; then reconsider gh = g +* ((x,y) --> (({} TM),({} TM))) as Function of F,(bool the carrier of TM) by A36, A38, FUNCT_2:2; take gh ; ::_thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) ( ((x,y) --> (({} TM),({} TM))) . y = {} TM & y in {x,y} ) by FUNCT_4:63, TARSKI:def_2; then A39: gh . y = {} TM by A31, FUNCT_4:13; for A being Subset of TM st A in {({} TM),({} TM)} holds A is open by TARSKI:def_2; then {({} TM),({} TM)} is open by TOPS_2:def_1; hence rng gh is open by A26, A35, A38, TOPS_2:13; ::_thesis: ( rng gh is Cover of A & ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) union (rng gh) = (union (rng g)) \/ (union (rng ((x,y) --> (({} TM),({} TM))))) by A38, ZFMISC_1:78 .= (union (rng g)) \/ (union {({} TM)}) by A35, ENUMSET1:29 .= (union (rng g)) \/ ({} TM) by ZFMISC_1:25 .= union (rng g) ; hence rng gh is Cover of A by A30, SETFAM_1:def_11; ::_thesis: ( ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) ( x in {x,y} & ((x,y) --> (({} TM),({} TM))) . x = {} TM ) by A34, FUNCT_4:63, TARSKI:def_2; then A40: gh . x = {} TM by A31, FUNCT_4:13; hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b let a be set ; ::_thesis: ( a in F implies gh . b1 c= b1 ) assume A41: a in F ; ::_thesis: gh . b1 c= b1 percases ( a in (F \ {x}) \ {y} or a in {x,y} ) by A36, A41, XBOOLE_0:def_3; suppose a in (F \ {x}) \ {y} ; ::_thesis: gh . b1 c= b1 then ( not a in dom ((x,y) --> (({} TM),({} TM))) & g . a c= a ) by A28, A33, XBOOLE_0:3; hence gh . a c= a by FUNCT_4:11; ::_thesis: verum end; suppose a in {x,y} ; ::_thesis: gh . b1 c= b1 then ( a = x or a = y ) by TARSKI:def_2; hence gh . a c= a by A39, A40, XBOOLE_1:2; ::_thesis: verum end; end; end; let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b ) assume that A42: ( a in F & b in F ) and A43: a <> b ; ::_thesis: gh . a misses gh . b percases ( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or a in {x,y} or b in {x,y} ) by A36, A42, XBOOLE_0:def_3; supposeA44: ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) ; ::_thesis: gh . a misses gh . b then not a in dom ((x,y) --> (({} TM),({} TM))) by A33, XBOOLE_0:3; then A45: gh . a = g . a by FUNCT_4:11; ( not b in dom ((x,y) --> (({} TM),({} TM))) & g . a misses g . b ) by A29, A33, A43, A44, XBOOLE_0:3; hence gh . a misses gh . b by A45, FUNCT_4:11; ::_thesis: verum end; suppose ( a in {x,y} or b in {x,y} ) ; ::_thesis: gh . a misses gh . b then ( gh . a = {} TM or gh . b = {} TM ) by A39, A40, TARSKI:def_2; hence gh . a misses gh . b by XBOOLE_1:65; ::_thesis: verum end; end; end; supposeA46: (F \ {x}) \ {y} is not Cover of A ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) A47: (union ((F \ {x}) \ {y})) \/ (x \/ y) = (union ((F \ {x}) \ {y})) \/ (union {(x \/ y)}) by ZFMISC_1:25 .= union (((F \ {x}) \ {y}) \/ {(x \/ y)}) by ZFMISC_1:78 ; A48: ((F \ {x}) \ {y}) \/ {(x \/ y)} is open by A22, A24, TOPS_2:13; A49: union F = (union (F \ {x})) \/ (union {x}) by A19, ZFMISC_1:78 .= (union (F \ {x})) \/ x by ZFMISC_1:25 .= ((union ((F \ {x}) \ {y})) \/ (union {y})) \/ x by A23, ZFMISC_1:78 .= ((union ((F \ {x}) \ {y})) \/ y) \/ x by ZFMISC_1:25 .= (union ((F \ {x}) \ {y})) \/ (y \/ x) by XBOOLE_1:4 ; A c= union F by A9, SETFAM_1:def_11; then ((F \ {x}) \ {y}) \/ {(x \/ y)} is Cover of A by A47, A49, SETFAM_1:def_11; then consider g being Function of (((F \ {x}) \ {y}) \/ {(x \/ y)}),(bool the carrier of TM) such that A50: rng g is open and A51: rng g is Cover of A and A52: for a being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} holds g . a c= a and A53: for a, b being set st a in ((F \ {x}) \ {y}) \/ {(x \/ y)} & b in ((F \ {x}) \ {y}) \/ {(x \/ y)} & a <> b holds g . a misses g . b by A4, A5, A6, A7, A21, A48; A54: rng (g | ((F \ {x}) \ {y})) is open by A50, RELAT_1:70, TOPS_2:11; x \/ y in {(x \/ y)} by TARSKI:def_1; then A55: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def_3; then A56: g . (x \/ y) c= x \/ y by A52; A57: dom g = ((F \ {x}) \ {y}) \/ {(x \/ y)} by FUNCT_2:def_1; then A58: dom (g | ((F \ {x}) \ {y})) = (((F \ {x}) \ {y}) \/ {(x \/ y)}) /\ ((F \ {x}) \ {y}) by RELAT_1:61 .= (F \ {x}) \ {y} by XBOOLE_1:21 ; g . (x \/ y) in rng g by A55, A57, FUNCT_1:def_3; then reconsider gxy = g . (x \/ y) as open Subset of TM by A50, TOPS_2:def_1; set gxyA = gxy /\ A; gxy /\ A c= gxy by XBOOLE_1:17; then A59: gxy /\ A c= x \/ y by A56, XBOOLE_1:1; [#] (TM | A) = A by PRE_TOPC:def_5; then reconsider GxyA = gxy /\ A as Subset of (TM | A) by XBOOLE_1:17; A60: (TM | A) | GxyA = TM | (gxy /\ A) by METRIZTS:9; then A61: gxy /\ A is finite-ind by A6, TOPDIM_1:18; then A62: ind (gxy /\ A) = ind (TM | (gxy /\ A)) by TOPDIM_1:17; ind GxyA <= ind (TM | A) by A6, TOPDIM_1:19; then ind GxyA <= 0 by A6, A7, TOPDIM_1:17; then ind (gxy /\ A) <= 0 by A61, TOPDIM_1:21; then consider V1, V2 being open Subset of TM such that A63: ( V1 c= x & V2 c= y ) and A64: V1 misses V2 and A65: gxy /\ A c= V1 \/ V2 by A5, A59, A60, A61, A62, Lm10; reconsider gV1 = gxy /\ V1, gV2 = gxy /\ V2 as open Subset of TM ; set h = (x,y) --> (gV1,gV2); A66: dom ((x,y) --> (gV1,gV2)) = {x,y} by FUNCT_4:62; then A67: dom ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = ((F \ {x}) \ {y}) \/ {x,y} by A58, FUNCT_4:def_1; not x in F \ {x} by ZFMISC_1:56; then A68: not x in (F \ {x}) \ {y} by ZFMISC_1:56; A69: x in {x,y} by TARSKI:def_2; A70: ((F \ {x}) \ {y}) \/ {x,y} = ((F \ {x}) \ {y}) \/ ({y} \/ {x}) by ENUMSET1:1 .= (((F \ {x}) \ {y}) \/ {y}) \/ {x} by XBOOLE_1:4 .= F by A18, A19, ZFMISC_1:116 ; for A being Subset of TM st A in {gV1,gV2} holds A is open by TARSKI:def_2; then A71: {gV1,gV2} is open by TOPS_2:def_1; A72: y in {x,y} by TARSKI:def_2; not y in (F \ {x}) \ {y} by ZFMISC_1:56; then A73: (F \ {x}) \ {y} misses {x,y} by A68, ZFMISC_1:51; then A74: rng ((g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2))) = (rng (g | ((F \ {x}) \ {y}))) \/ (rng ((x,y) --> (gV1,gV2))) by A58, A66, NECKLACE:6; then reconsider gh = (g | ((F \ {x}) \ {y})) +* ((x,y) --> (gV1,gV2)) as Function of F,(bool the carrier of TM) by A67, A70, FUNCT_2:2; A75: (F \ {x}) \ {y} c= dom gh by A67, XBOOLE_1:7; take gh ; ::_thesis: ( rng gh is open & rng gh is Cover of A & ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) A76: x <> y by A18, ZFMISC_1:56; then rng ((x,y) --> (gV1,gV2)) = {gV1,gV2} by FUNCT_4:64; hence rng gh is open by A54, A71, A74, TOPS_2:13; ::_thesis: ( rng gh is Cover of A & ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) ((x,y) --> (gV1,gV2)) . x = gV1 by A76, FUNCT_4:63; then A77: gh . x = gV1 by A66, A69, FUNCT_4:13; ((x,y) --> (gV1,gV2)) . y = gV2 by FUNCT_4:63; then A78: gh . y = gV2 by A66, A72, FUNCT_4:13; A79: for a, b being set st a in (F \ {x}) \ {y} & b in {x,y} & a <> b holds gh . a misses gh . b proof x \/ y in {(x \/ y)} by TARSKI:def_1; then A80: x \/ y in ((F \ {x}) \ {y}) \/ {(x \/ y)} by XBOOLE_0:def_3; let a, b be set ; ::_thesis: ( a in (F \ {x}) \ {y} & b in {x,y} & a <> b implies gh . a misses gh . b ) assume that A81: a in (F \ {x}) \ {y} and A82: b in {x,y} and a <> b ; ::_thesis: gh . a misses gh . b ( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A81, FUNCT_1:47, XBOOLE_0:3; then A83: gh . a = g . a by FUNCT_4:11; A84: a <> x \/ y proof assume a = x \/ y ; ::_thesis: contradiction then A85: union F = union ((F \ {x}) \ {y}) by A49, A81, XBOOLE_1:12, ZFMISC_1:74; not A c= union ((F \ {x}) \ {y}) by A46, SETFAM_1:def_11; hence contradiction by A9, A85, SETFAM_1:def_11; ::_thesis: verum end; assume gh . a meets gh . b ; ::_thesis: contradiction then consider z being set such that A86: z in gh . a and A87: z in gh . b by XBOOLE_0:3; ( z in gV1 or z in gV2 ) by A78, A77, A82, A87, TARSKI:def_2; then z in gxy by XBOOLE_0:def_4; then g . (x \/ y) meets g . a by A83, A86, XBOOLE_0:3; hence contradiction by A53, A58, A80, A81, A84; ::_thesis: verum end; A88: {x,y} c= dom gh by A67, XBOOLE_1:7; then A89: gh . y in rng gh by A72, FUNCT_1:def_3; A90: gh . x in rng gh by A69, A88, FUNCT_1:def_3; A c= union (rng gh) proof let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in A or z in union (rng gh) ) assume A91: z in A ; ::_thesis: z in union (rng gh) A c= union (rng g) by A51, SETFAM_1:def_11; then consider G being set such that A92: z in G and A93: G in rng g by A91, TARSKI:def_4; consider Gx being set such that A94: Gx in ((F \ {x}) \ {y}) \/ {(x \/ y)} and A95: g . Gx = G by A57, A93, FUNCT_1:def_3; percases ( Gx in (F \ {x}) \ {y} or Gx in {(x \/ y)} ) by A94, XBOOLE_0:def_3; supposeA96: Gx in (F \ {x}) \ {y} ; ::_thesis: z in union (rng gh) then ( (g | ((F \ {x}) \ {y})) . Gx = G & not Gx in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A95, FUNCT_1:47, XBOOLE_0:3; then A97: gh . Gx = G by FUNCT_4:11; gh . Gx in rng gh by A75, A96, FUNCT_1:def_3; hence z in union (rng gh) by A92, A97, TARSKI:def_4; ::_thesis: verum end; suppose Gx in {(x \/ y)} ; ::_thesis: z in union (rng gh) then A98: z in gxy by A92, A95, TARSKI:def_1; then z in gxy /\ A by A91, XBOOLE_0:def_4; then ( z in V1 or z in V2 ) by A65, XBOOLE_0:def_3; then ( z in gV1 or z in gV2 ) by A98, XBOOLE_0:def_4; hence z in union (rng gh) by A78, A77, A90, A89, TARSKI:def_4; ::_thesis: verum end; end; end; hence rng gh is Cover of A by SETFAM_1:def_11; ::_thesis: ( ( for a being set st a in F holds gh . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b ) ) A99: ( gV1 c= V1 & gV2 c= V2 ) by XBOOLE_1:17; hereby ::_thesis: for a, b being set st a in F & b in F & a <> b holds gh . a misses gh . b let a be set ; ::_thesis: ( a in F implies gh . b1 c= b1 ) assume A100: a in F ; ::_thesis: gh . b1 c= b1 percases ( a in (F \ {x}) \ {y} or a in {x,y} ) by A70, A100, XBOOLE_0:def_3; supposeA101: a in (F \ {x}) \ {y} ; ::_thesis: gh . b1 c= b1 then A102: (g | ((F \ {x}) \ {y})) . a = g . a by A58, FUNCT_1:47; ( not a in dom ((x,y) --> (gV1,gV2)) & g . a c= a ) by A52, A58, A73, A101, XBOOLE_0:3; hence gh . a c= a by A102, FUNCT_4:11; ::_thesis: verum end; suppose a in {x,y} ; ::_thesis: gh . b1 c= b1 then ( a = x or a = y ) by TARSKI:def_2; hence gh . a c= a by A63, A78, A77, A99, XBOOLE_1:1; ::_thesis: verum end; end; end; let a, b be set ; ::_thesis: ( a in F & b in F & a <> b implies gh . a misses gh . b ) assume that A103: ( a in F & b in F ) and A104: a <> b ; ::_thesis: gh . a misses gh . b percases ( ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) or ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) or ( a in {x,y} & b in {x,y} ) ) by A70, A103, XBOOLE_0:def_3; supposeA105: ( a in (F \ {x}) \ {y} & b in (F \ {x}) \ {y} ) ; ::_thesis: gh . a misses gh . b then ( (g | ((F \ {x}) \ {y})) . a = g . a & not a in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, FUNCT_1:47, XBOOLE_0:3; then A106: gh . a = g . a by FUNCT_4:11; A107: ( (g | ((F \ {x}) \ {y})) . b = g . b & not b in dom ((x,y) --> (gV1,gV2)) ) by A58, A73, A105, FUNCT_1:47, XBOOLE_0:3; g . a misses g . b by A53, A58, A104, A105; hence gh . a misses gh . b by A106, A107, FUNCT_4:11; ::_thesis: verum end; suppose ( ( a in (F \ {x}) \ {y} & b in {x,y} ) or ( a in {x,y} & b in (F \ {x}) \ {y} ) ) ; ::_thesis: gh . a misses gh . b hence gh . a misses gh . b by A79, A104; ::_thesis: verum end; supposeA108: ( a in {x,y} & b in {x,y} ) ; ::_thesis: gh . a misses gh . b then ( a = x or a = y ) by TARSKI:def_2; then ( ( a = x & b = y ) or ( a = y & b = x ) ) by A104, A108, TARSKI:def_2; hence gh . a misses gh . b by A64, A78, A77, A99, XBOOLE_1:64; ::_thesis: verum end; end; end; end; end; end; end; end; end; A109: S1[ 0 ] proof let A be Subset of TM; ::_thesis: ( TM | A is second-countable & A is finite-ind & ind A <= 0 implies for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume that TM | A is second-countable and A is finite-ind and ind A <= 0 ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of A & card F <= 0 holds ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of A & card F <= 0 implies ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ) assume that F is open and A110: F is Cover of A and A111: card F <= 0 ; ::_thesis: ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) ( rng {} c= bool the carrier of TM & dom {} = F ) by A111, XBOOLE_1:2; then reconsider g = {} as Function of F,(bool the carrier of TM) by FUNCT_2:2; take g ; ::_thesis: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) F = {} by A111; hence ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) by A110; ::_thesis: verum end; for n being Nat holds S1[n] from NAT_1:sch_2(A109, A3); then S1[ card F] ; hence ex g being Function of F,(bool the carrier of TM) st ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) by A1, A2, TOPDIM_1:18; ::_thesis: verum end; theorem :: TOPDIM_2:23 for n being Nat for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds for F being finite Subset-Family of TM st F is open & F is Cover of TM holds ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) proof let n be Nat; ::_thesis: for TM being metrizable TopSpace st TM is second-countable & TM is finite-ind & ind TM <= n holds for F being finite Subset-Family of TM st F is open & F is Cover of TM holds ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) let TM be metrizable TopSpace; ::_thesis: ( TM is second-countable & TM is finite-ind & ind TM <= n implies for F being finite Subset-Family of TM st F is open & F is Cover of TM holds ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) ) assume that A1: ( TM is second-countable & TM is finite-ind ) and A2: ind TM <= n ; ::_thesis: for F being finite Subset-Family of TM st F is open & F is Cover of TM holds ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) reconsider I = n as Integer ; consider G being finite Subset-Family of TM such that A3: G is Cover of TM and A4: ( G is finite-ind & ind G <= 0 ) and A5: card G <= I + 1 and for a, b being Subset of TM st a in G & b in G & a meets b holds a = b by A1, A2, Th7; set cTM = the carrier of TM; let F be finite Subset-Family of TM; ::_thesis: ( F is open & F is Cover of TM implies ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) ) assume that A6: F is open and A7: F is Cover of TM ; ::_thesis: ex G being finite Subset-Family of TM st ( G is open & G is Cover of TM & G is_finer_than F & card G <= (card F) * (n + 1) & order G <= n ) card ((n + 1) * (card F)) = card (card ((n + 1) * (card F))) ; then A8: card ((n + 1) * (card F)) = (n + 1) * (card F) by CARD_1:40; defpred S1[ set , set ] means for A being Subset of TM st A = $1 holds ex g being Function of F,(bool the carrier of TM) st ( $2 = rng g & rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ); A9: for x being set st x in G holds ex y being set st ( y in bool (bool the carrier of TM) & S1[x,y] ) proof let x be set ; ::_thesis: ( x in G implies ex y being set st ( y in bool (bool the carrier of TM) & S1[x,y] ) ) assume A10: x in G ; ::_thesis: ex y being set st ( y in bool (bool the carrier of TM) & S1[x,y] ) then reconsider A = x as Subset of TM ; A11: TM | A is second-countable by A1; [#] TM c= union F by A7, SETFAM_1:def_11; then A c= union F by XBOOLE_1:1; then A12: F is Cover of A by SETFAM_1:def_11; ( A is finite-ind & ind A <= 0 ) by A4, A10, TOPDIM_1:11; then consider g being Function of F,(bool the carrier of TM) such that A13: ( rng g is open & rng g is Cover of A & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) by A6, A11, A12, Th22; take rng g ; ::_thesis: ( rng g in bool (bool the carrier of TM) & S1[x, rng g] ) thus ( rng g in bool (bool the carrier of TM) & S1[x, rng g] ) by A13; ::_thesis: verum end; consider GG being Function of G,(bool (bool the carrier of TM)) such that A14: for x being set st x in G holds S1[x,GG . x] from FUNCT_2:sch_1(A9); union (rng GG) c= union (bool (bool the carrier of TM)) by ZFMISC_1:77; then reconsider Ugg = Union GG as Subset-Family of TM ; A15: dom GG = G by FUNCT_2:def_1; A16: for x being set st x in dom GG holds card (GG . x) c= card F proof let x be set ; ::_thesis: ( x in dom GG implies card (GG . x) c= card F ) assume A17: x in dom GG ; ::_thesis: card (GG . x) c= card F then reconsider A = x as Subset of TM by A15; consider g being Function of F,(bool the carrier of TM) such that A18: GG . x = rng g and rng g is open and rng g is Cover of A and for a being set st a in F holds g . a c= a and for a, b being set st a in F & b in F & a <> b holds g . a misses g . b by A14, A17; dom g = F by FUNCT_2:def_1; hence card (GG . x) c= card F by A18, CARD_1:12; ::_thesis: verum end; card (dom GG) c= n + 1 by A5, A15, NAT_1:39; then A19: card Ugg c= (n + 1) *` (card F) by A16, CARD_2:86; card (card (n + 1)) = card (n + 1) ; then ( card (card F) = card F & card (n + 1) = n + 1 ) by CARD_1:40; then A20: (n + 1) *` (card F) = (n + 1) * (card F) by A8, CARD_2:39; then reconsider Ugg = Ugg as finite Subset-Family of TM by A19; take Ugg ; ::_thesis: ( Ugg is open & Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n ) thus Ugg is open ::_thesis: ( Ugg is Cover of TM & Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n ) proof let A be Subset of TM; :: according to TOPS_2:def_1 ::_thesis: ( not A in Ugg or A is open ) assume A in Ugg ; ::_thesis: A is open then consider Y being set such that A21: A in Y and A22: Y in rng GG by TARSKI:def_4; consider x being set such that A23: ( x in dom GG & Y = GG . x ) by A22, FUNCT_1:def_3; ex g being Function of F,(bool the carrier of TM) st ( Y = rng g & rng g is open & rng g is Cover of x & ( for a being set st a in F holds g . a c= a ) & ( for a, b being set st a in F & b in F & a <> b holds g . a misses g . b ) ) by A14, A15, A23; hence A is open by A21, TOPS_2:def_1; ::_thesis: verum end; [#] TM c= union Ugg proof A24: [#] TM c= union G by A3, SETFAM_1:def_11; let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in [#] TM or x in union Ugg ) assume A25: x in [#] TM ; ::_thesis: x in union Ugg consider A being set such that A26: x in A and A27: A in G by A24, A25, TARSKI:def_4; consider g being Function of F,(bool the carrier of TM) such that A28: GG . A = rng g and rng g is open and A29: rng g is Cover of A and for a being set st a in F holds g . a c= a and for a, b being set st a in F & b in F & a <> b holds g . a misses g . b by A14, A27; A c= union (rng g) by A29, SETFAM_1:def_11; then consider y being set such that A30: x in y and A31: y in rng g by A26, TARSKI:def_4; GG . A in rng GG by A15, A27, FUNCT_1:def_3; then y in Ugg by A28, A31, TARSKI:def_4; hence x in union Ugg by A30, TARSKI:def_4; ::_thesis: verum end; hence Ugg is Cover of TM by SETFAM_1:def_11; ::_thesis: ( Ugg is_finer_than F & card Ugg <= (card F) * (n + 1) & order Ugg <= n ) thus Ugg is_finer_than F ::_thesis: ( card Ugg <= (card F) * (n + 1) & order Ugg <= n ) proof let A be set ; :: according to SETFAM_1:def_2 ::_thesis: ( not A in Ugg or ex b1 being set st ( b1 in F & A c= b1 ) ) assume A in Ugg ; ::_thesis: ex b1 being set st ( b1 in F & A c= b1 ) then consider Y being set such that A32: A in Y and A33: Y in rng GG by TARSKI:def_4; consider x being set such that A34: ( x in dom GG & Y = GG . x ) by A33, FUNCT_1:def_3; consider g being Function of F,(bool the carrier of TM) such that A35: Y = rng g and rng g is open and rng g is Cover of x and A36: for a being set st a in F holds g . a c= a and for a, b being set st a in F & b in F & a <> b holds g . a misses g . b by A14, A15, A34; dom g = F by FUNCT_2:def_1; then ex z being set st ( z in F & g . z = A ) by A32, A35, FUNCT_1:def_3; hence ex b1 being set st ( b1 in F & A c= b1 ) by A36; ::_thesis: verum end; thus card Ugg <= (card F) * (n + 1) by A19, A20, NAT_1:39; ::_thesis: order Ugg <= n defpred S2[ set , set ] means $1 in GG . $2; now__::_thesis:_for_H_being_finite_Subset-Family_of_TM_st_H_c=_Ugg_&_card_H_>_n_+_1_holds_ meet_H_is_empty let H be finite Subset-Family of TM; ::_thesis: ( H c= Ugg & card H > n + 1 implies meet H is empty ) assume that A37: H c= Ugg and A38: card H > n + 1 ; ::_thesis: meet H is empty not H is empty by A38; then consider XX being set such that A39: XX in H by XBOOLE_0:def_1; A40: for x being set st x in H holds ex y being set st ( y in G & S2[x,y] ) proof let A be set ; ::_thesis: ( A in H implies ex y being set st ( y in G & S2[A,y] ) ) assume A in H ; ::_thesis: ex y being set st ( y in G & S2[A,y] ) then consider Y being set such that A41: A in Y and A42: Y in rng GG by A37, TARSKI:def_4; ex x being set st ( x in dom GG & Y = GG . x ) by A42, FUNCT_1:def_3; hence ex y being set st ( y in G & S2[A,y] ) by A41; ::_thesis: verum end; consider q being Function of H,G such that A43: for x being set st x in H holds S2[x,q . x] from FUNCT_2:sch_1(A40); ex y being set st ( y in G & S2[XX,y] ) by A40, A39; then A44: dom q = H by FUNCT_2:def_1; assume not meet H is empty ; ::_thesis: contradiction then consider x being set such that A45: x in meet H by XBOOLE_0:def_1; for x1, x2 being set st x1 in dom q & x2 in dom q & q . x1 = q . x2 holds x1 = x2 proof let x1, x2 be set ; ::_thesis: ( x1 in dom q & x2 in dom q & q . x1 = q . x2 implies x1 = x2 ) assume that A46: x1 in dom q and A47: x2 in dom q and A48: q . x1 = q . x2 ; ::_thesis: x1 = x2 ( x in x1 & x in x2 ) by A45, A46, A47, SETFAM_1:def_1; then A49: x1 meets x2 by XBOOLE_0:3; q . x1 in rng q by A46, FUNCT_1:def_3; then q . x1 in G ; then consider g being Function of F,(bool the carrier of TM) such that A50: GG . (q . x1) = rng g and rng g is open and rng g is Cover of q . x1 and for a being set st a in F holds g . a c= a and A51: for a, b being set st a in F & b in F & a <> b holds g . a misses g . b by A14; A52: dom g = F by FUNCT_2:def_1; x2 in GG . (q . x1) by A43, A47, A48; then A53: ex y2 being set st ( y2 in F & x2 = g . y2 ) by A50, A52, FUNCT_1:def_3; x1 in GG . (q . x1) by A43, A46; then ex y1 being set st ( y1 in F & x1 = g . y1 ) by A50, A52, FUNCT_1:def_3; hence x1 = x2 by A49, A51, A53; ::_thesis: verum end; then A54: q is one-to-one by FUNCT_1:def_4; rng q c= G ; then card H c= card G by A54, A44, CARD_1:10; then card H <= card G by NAT_1:39; hence contradiction by A5, A38, XXREAL_0:2; ::_thesis: verum end; hence order Ugg <= n by Th3; ::_thesis: verum end; theorem :: TOPDIM_2:24 for n being Nat 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 ) proof 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 set 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, XBOOLE_0:def_7 .= [#] 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, XBOOLE_0:def_10; ::_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, XBOOLE_0:def_10; ::_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 end;