let T be non empty TopSpace; :: thesis: for B being ManySortedSet of T st ( for x being Element of T holds B . x is Basis of x ) holds
Union B is Basis of T
let B be ManySortedSet of T; :: thesis: ( ( for x being Element of T holds B . x is Basis of x ) implies Union B is Basis of T )
assume A1: for x being Element of T holds B . x is Basis of x ; :: thesis: Union B is Basis of T
Union B c= bool the carrier of T
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in Union B or a in bool the carrier of T )
assume a in Union B ; :: thesis: a in bool the carrier of T
then consider b being object such that
A2: b in dom B and
A3: a in B . b by CARD_5:2;
reconsider b = b as Point of T by A2;
B . b is Basis of b by A1;
hence a in bool the carrier of T by A3; :: thesis: verum
end;
then reconsider W = Union B as Subset-Family of T ;
A4: dom B = the carrier of T by PARTFUN1:def 2;
A5: now :: thesis: for A being Subset of T st A is open holds
for p being Point of T st p in A holds
ex a being Subset of T st
( a in W & p in a & a c= A )
let A be Subset of T; :: thesis: ( A is open implies for p being Point of T st p in A holds
ex a being Subset of T st
( a in W & p in a & a c= A ) )
assume A6: A is open ; :: thesis: for p being Point of T st p in A holds
ex a being Subset of T st
( a in W & p in a & a c= A )
let p be Point of T; :: thesis: ( p in A implies ex a being Subset of T st
( a in W & p in a & a c= A ) )
assume A7: p in A ; :: thesis: ex a being Subset of T st
( a in W & p in a & a c= A )
A8: B . p is Basis of p by A1;
then consider a being Subset of T such that
A9: a in B . p and
A10: a c= A by A6, A7, YELLOW_8:def 1;
take a = a; :: thesis: ( a in W & p in a & a c= A )
thus a in W by A4, A9, CARD_5:2; :: thesis: ( p in a & a c= A )
thus p in a by A8, A9, YELLOW_8:12; :: thesis: a c= A
thus a c= A by A10; :: thesis: verum
end;
W c= the topology of T
proof
let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in W or a in the topology of T )
assume a in W ; :: thesis: a in the topology of T
then consider b being object such that
A11: b in dom B and
A12: a in B . b by CARD_5:2;
reconsider b = b as Point of T by A11;
B . b is Basis of b by A1;
then B . b c= the topology of T by TOPS_2:64;
hence a in the topology of T by A12; :: thesis: verum
end;
hence Union B is Basis of T by A5, YELLOW_9:32; :: thesis: verum