set TOP = the topology of TM;
set cTM = the carrier of TM;
let Am be Subset of TM; :: thesis: ( Am is open implies Am is F_sigma )
assume A1: Am is open ; :: thesis: Am is F_sigma
per cases ( TM is empty or not TM is empty ) ;
suppose A2: TM is empty ; :: thesis: Am is F_sigma
reconsider E = {} as empty Subset-Family of TM by TOPGEN_4:18;
Am = union E by A2, ZFMISC_1:2;
hence Am is F_sigma by TOPGEN_4:def 6; :: thesis: verum
end;
suppose A3: not TM is empty ; :: thesis: Am is F_sigma
per cases ( Am = [#] TM or Am <> [#] TM ) ;
suppose A4: Am <> [#] TM ; :: thesis: Am is F_sigma
consider metr being Function of [:the carrier of TM,the carrier of TM:],REAL such that
A5: metr is_metric_of the carrier of TM and
A6: Family_open_set (SpaceMetr the carrier of TM,metr) = the topology of TM by PCOMPS_1:def 9;
reconsider Tm = SpaceMetr the carrier of TM,metr as non empty MetrSpace by A3, A5, PCOMPS_1:40;
set TTm = TopSpaceMetr Tm;
Am in the topology of (TopSpaceMetr Tm) by A1, A6, PRE_TOPC:def 5;
then reconsider a = Am as open Subset of (TopSpaceMetr Tm) by PRE_TOPC:def 5;
({} (TopSpaceMetr Tm)) ` = [#] (TopSpaceMetr Tm) ;
then reconsider A9 = a ` as non empty closed Subset of (TopSpaceMetr Tm) by A3, A4, A5, PCOMPS_2:8;
defpred S1[ set , set ] means for n being Nat st n = TM holds
c2 = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } ;
A7: for x being set st x in NAT holds
ex y being set st
( y in the topology of TM & S1[x,y] )
proof
let x be set ; :: thesis: ( x in NAT implies ex y being set st
( y in the topology of TM & S1[x,y] ) )
assume x in NAT ; :: thesis: ex y being set st
( y in the topology of TM & S1[x,y] )
then reconsider n = x as Element of NAT ;
reconsider BallA = { p where p is Point of (TopSpaceMetr Tm) : (dist_min A9) . p < 1 / (2 |^ n) } as open Subset of (TopSpaceMetr Tm) by Lm4;
take BallA ; :: thesis: ( BallA in the topology of TM & S1[x,BallA] )
thus ( BallA in the topology of TM & S1[x,BallA] ) by A6, PRE_TOPC:def 5; :: thesis: verum
end;
consider p being Function of NAT ,the topology of TM such that
A8: for x being set st x in NAT holds
S1[x,p . x] from FUNCT_2:sch 1(A7);
 the topology of TM is open by CANTOR_1:3;
then reconsider RNG = rng p as open Subset-Family of TM by TOPS_2:18, XBOOLE_1:1;
set Crng = COMPLEMENT RNG;
A9: dom p = NAT by FUNCT_2:def 1;
A10: [#] TM = [#] (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:8;
A11: union (COMPLEMENT RNG) = Am
proof
hereby :: according to TARSKI:def 3,XBOOLE_0:def 10 :: thesis: Am c= union (COMPLEMENT RNG)
let x be set ; :: thesis: ( x in union (COMPLEMENT RNG) implies x in Am )
assume A12: x in union (COMPLEMENT RNG) ; :: thesis: x in Am
then consider y being set such that
A13: x in y and
A14: y in COMPLEMENT RNG by TARSKI:def 4;
reconsider Y = y as Subset of TM by A14;
Y ` in RNG by A14, SETFAM_1:def 8;
then consider n being set such that
A15: n in dom p and
A16: p . n = Y ` by FUNCT_1:def 5;
reconsider n = n as Element of NAT by A15;
assume not x in Am ; :: thesis: contradiction
then x in A9 by A10, A12, XBOOLE_0:def 5;
then A17: ( 2 |^ n > 0 & (dist_min A9) . x = 0 ) by HAUSDORF:5, PREPOWER:13;
Y ` = { q where q is Point of (TopSpaceMetr Tm) : (dist_min A9) . q < 1 / (2 |^ n) } by A8, A16;
then x in Y ` by A10, A12, A17;
hence contradiction by A13, XBOOLE_0:def 5; :: thesis: verum
end;
let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Am or x in union (COMPLEMENT RNG) )
assume A18: x in Am ; :: thesis: x in union (COMPLEMENT RNG)
then reconsider q = x as Point of (TopSpaceMetr Tm) by A3, A5, PCOMPS_2:8;
( Cl A9 = A9 & not q in A9 ) by A18, PRE_TOPC:52, XBOOLE_0:def 5;
then A19: (dist_min A9) . q <> 0 by HAUSDORF:10;
(dist_min A9) . q >= 0 by JORDAN1K:9;
then consider n being Element of NAT such that
A20: 1 / (2 |^ n) <= (dist_min A9) . q by A19, PREPOWER:106;
p . n in RNG by A9, FUNCT_1:def 5;
then reconsider pn = p . n as Subset of TM ;
A21: pn = { s where s is Point of (TopSpaceMetr Tm) : (dist_min A9) . s < 1 / (2 |^ n) } by A8;
for s being Point of (TopSpaceMetr Tm) st s = q holds
not 1 / (2 |^ n) > (dist_min A9) . s by A20;
then not q in pn by A21;
then A22: q in pn ` by A18, XBOOLE_0:def 5;
(pn ` ) ` in RNG by A9, FUNCT_1:def 5;
then pn ` in COMPLEMENT RNG by SETFAM_1:def 8;
hence x in union (COMPLEMENT RNG) by A22, TARSKI:def 4; :: thesis: verum
end;
( COMPLEMENT RNG is closed & RNG is countable ) by A9, CARD_3:127, TOPS_2:17;
hence Am is F_sigma by A11, TOPGEN_4:def 6; :: thesis: verum
end;
end;
end;
end;