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 S_{1}[ object , object ] 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 object st x in NAT holds

ex y being object st

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

A4: for x being object st x in NAT holds

S_{1}[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 )

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

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

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 S

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 object st x in NAT holds

ex y being object st

( y in bool (bool the carrier of T) & S

proof

consider f being SetSequence of (bool the carrier of T) such that
let x be object ; :: thesis: ( x in NAT implies ex y being object st

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

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

( y in bool (bool the carrier of T) & S_{1}[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) & S_{1}[x,y] )

thus ( y in bool (bool the carrier of T) & S_{1}[x,y] )
by A3; :: thesis: verum

end;( y in bool (bool the carrier of T) & S

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

( y in bool (bool the carrier of T) & S

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) & S

thus ( y in bool (bool the carrier of T) & S

A4: for x being object st x in NAT holds

S

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

for A being Subset of T st A in F holds
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 Nat such that

A5: A in f . n by PROB_1:12;

n in NAT by ORDINAL1:def 12;

then f . n is closed by A4;

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

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

then consider n being Nat such that

A5: A in f . n by PROB_1:12;

n in NAT by ORDINAL1:def 12;

then f . n is closed by A4;

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

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

proof

hence
( F is finite-ind & ind F <= n )
by TOPDIM_1:11; :: thesis: ( F is countable & Union g = union F )
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 Nat such that

A6: A in f . i by PROB_1:12;

i in NAT by ORDINAL1:def 12;

then 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;assume A in F ; :: thesis: ( A is finite-ind & ind A <= n )

then consider i being Nat such that

A6: A in f . i by PROB_1:12;

i in NAT by ORDINAL1:def 12;

then 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

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

thus
union F c= Union g
:: thesis: verum
let x be object ; :: 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 Nat such that

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

i in NAT by ORDINAL1:def 12;

then 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;assume x in Union g ; :: thesis: x in union F

then consider i being Nat such that

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

i in NAT by ORDINAL1:def 12;

then 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

proof

let x be object ; :: 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 Nat such that

A15: y in f . i by A14, PROB_1:12;

i in NAT by ORDINAL1:def 12;

then 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;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 Nat such that

A15: y in f . i by A14, PROB_1:12;

i in NAT by ORDINAL1:def 12;

then 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