let X be set ; :: thesis: for B being Subset-Family of X st B is point-filtered & B is covering holds
for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T )
let B be Subset-Family of X; :: thesis: ( B is point-filtered & B is covering implies for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T ) )
assume A1: ( B is point-filtered & B is covering ) ; :: thesis: for T being TopStruct st the carrier of T = X & the topology of T = UniCl B holds
( T is TopSpace & B is Basis of T )
let T be TopStruct ; :: thesis: ( the carrier of T = X & the topology of T = UniCl B implies ( T is TopSpace & B is Basis of T ) )
assume that
A2: the carrier of T = X and
A3: the topology of T = UniCl B ; :: thesis: ( T is TopSpace & B is Basis of T )
T is TopSpace-like
proof
union B in UniCl B by CANTOR_1:def 1;
hence the carrier of T in the topology of T by A1, A2, A3, ABIAN:4; :: according to PRE_TOPC:def 1 :: thesis: ( ( for b1 being Element of bool (bool the carrier of T) holds
( not b1 c= the topology of T or union b1 in the topology of T ) ) & ( for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T ) ) )
hereby :: thesis: for b1, b2 being Element of bool the carrier of T holds
( not b1 in the topology of T or not b2 in the topology of T or b1 /\ b2 in the topology of T )
let a be Subset-Family of T; :: thesis: ( a c= the topology of T implies union a in the topology of T )
assume a c= the topology of T ; :: thesis: union a in the topology of T
then union a in UniCl the topology of T by CANTOR_1:def 1;
hence union a in the topology of T by A2, A3, YELLOW_9:15; :: thesis: verum
end;
let a, b be Subset of T; :: thesis: ( not a in the topology of T or not b in the topology of T or a /\ b in the topology of T )
set Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } ;
{ c where c is Subset of T : ( c in B & c c= a /\ b ) } c= bool X
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } or x in bool X )
assume x in { c where c is Subset of T : ( c in B & c c= a /\ b ) } ; :: thesis: x in bool X
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in bool X ; :: thesis: verum
end;
then reconsider Bc = { c where c is Subset of T : ( c in B & c c= a /\ b ) } as Subset-Family of T by A2;
assume a in the topology of T ; :: thesis: ( not b in the topology of T or a /\ b in the topology of T )
then consider Ba being Subset-Family of T such that
A4: Ba c= B and
A5: a = union Ba by A2, A3, CANTOR_1:def 1;
assume b in the topology of T ; :: thesis: a /\ b in the topology of T
then consider Bb being Subset-Family of T such that
A6: Bb c= B and
A7: b = union Bb by A2, A3, CANTOR_1:def 1;
A8: union Bc = a /\ b
proof
Bc c= bool (a /\ b)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Bc or x in bool (a /\ b) )
assume x in Bc ; :: thesis: x in bool (a /\ b)
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in bool (a /\ b) ; :: thesis: verum
end;
then union Bc c= union (bool (a /\ b)) by ZFMISC_1:77;
hence union Bc c= a /\ b by ZFMISC_1:81; :: according to XBOOLE_0:def 10 :: thesis: a /\ b c= union Bc
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a /\ b or x in union Bc )
assume A9: x in a /\ b ; :: thesis: x in union Bc
then x in a by XBOOLE_0:def 4;
then consider U1 being set such that
A10: x in U1 and
A11: U1 in Ba by A5, TARSKI:def 4;
x in b by A9, XBOOLE_0:def 4;
then consider U2 being set such that
A12: x in U2 and
A13: U2 in Bb by A7, TARSKI:def 4;
A14: U2 c= b by A7, A13, ZFMISC_1:74;
x in U1 /\ U2 by A10, A12, XBOOLE_0:def 4;
then consider U being Subset of X such that
A15: U in B and
A16: x in U and
A17: U c= U1 /\ U2 by A4, A11, A6, A13, A1;
U1 c= a by A5, A11, ZFMISC_1:74;
then U1 /\ U2 c= a /\ b by A14, XBOOLE_1:27;
then U c= a /\ b by A17;
then U in Bc by A2, A15;
hence x in union Bc by A16, TARSKI:def 4; :: thesis: verum
end;
Bc c= B
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in Bc or x in B )
assume x in Bc ; :: thesis: x in B
then ex c being Subset of T st
( x = c & c in B & c c= a /\ b ) ;
hence x in B ; :: thesis: verum
end;
hence a /\ b in the topology of T by A8, A2, A3, CANTOR_1:def 1; :: thesis: verum
end;
hence T is TopSpace ; :: thesis: B is Basis of T
reconsider B9 = B as Subset-Family of T by A2;
B9 c= the topology of T by A3, CANTOR_1:1;
hence B is Basis of T by A2, A3, CANTOR_1:def 2, TOPS_2:64; :: thesis: verum