let X be set ; for B being non-empty ManySortedSet of X st rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds
x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ) holds
ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )
let B be non-empty ManySortedSet of X; ( rng B c= bool (bool X) & ( for x, U being set st x in X & U in B . x holds
x in U ) & ( for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U ) ) & ( for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 ) ) implies ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) ) )
assume A1:
rng B c= bool (bool X)
; ( ex x, U being set st
( x in X & U in B . x & not x in U ) or ex x, y, U being set st
( x in U & U in B . y & y in X & ( for V being set holds
( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) ) )
Union B c= union (bool (bool X))
by A1, ZFMISC_1:77;
then reconsider P = Union B as Subset-Family of X by ZFMISC_1:81;
A2:
dom B = X
by PARTFUN1:def 2;
assume A3:
for x, U being set st x in X & U in B . x holds
x in U
; ( ex x, y, U being set st
( x in U & U in B . y & y in X & ( for V being set holds
( not V in B . x or not V c= U ) ) ) or ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) ) )
assume A4:
for x, y, U being set st x in U & U in B . y & y in X holds
ex V being set st
( V in B . x & V c= U )
; ( ex x, U1, U2 being set st
( x in X & U1 in B . x & U2 in B . x & ( for U being set holds
( not U in B . x or not U c= U1 /\ U2 ) ) ) or ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) ) )
assume A5:
for x, U1, U2 being set st x in X & U1 in B . x & U2 in B . x holds
ex U being set st
( U in B . x & U c= U1 /\ U2 )
; ex P being Subset-Family of X st
( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )
A6:
P is point-filtered
proof
let x,
U1,
U2 be
set ;
TOPGEN_3:def 1 ( U1 in P & U2 in P & x in U1 /\ U2 implies ex U being Subset of X st
( U in P & x in U & U c= U1 /\ U2 ) )
assume that A7:
U1 in P
and A8:
U2 in P
and A9:
x in U1 /\ U2
;
ex U being Subset of X st
( U in P & x in U & U c= U1 /\ U2 )
A10:
x in U2
by A9, XBOOLE_0:def 4;
ex
y2 being
object st
(
y2 in X &
U2 in B . y2 )
by A2, A8, CARD_5:2;
then consider V2 being
set such that A11:
V2 in B . x
and A12:
V2 c= U2
by A10, A4;
A13:
x in U1
by A9, XBOOLE_0:def 4;
ex
y1 being
object st
(
y1 in X &
U1 in B . y1 )
by A7, A2, CARD_5:2;
then consider V1 being
set such that A14:
V1 in B . x
and A15:
V1 c= U1
by A13, A4;
A16:
x in X
by A2, A14, FUNCT_1:def 2;
then consider U being
set such that A17:
U in B . x
and A18:
U c= V1 /\ V2
by A5, A14, A11;
U in P
by A2, A16, A17, CARD_5:2;
then reconsider U =
U as
Subset of
X ;
take
U
;
( U in P & x in U & U c= U1 /\ U2 )
thus
U in P
by A2, A16, A17, CARD_5:2;
( x in U & U c= U1 /\ U2 )
thus
x in U
by A3, A16, A17;
U c= U1 /\ U2
V1 /\ V2 c= U1 /\ U2
by A15, A12, XBOOLE_1:27;
hence
U c= U1 /\ U2
by A18;
verum
end;
take
P
; ( P = Union B & ( for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) ) )
thus
P = Union B
; for T being TopStruct st the carrier of T = X & the topology of T = UniCl P holds
( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) )
let T be TopStruct ; ( the carrier of T = X & the topology of T = UniCl P implies ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) ) )
assume that
A19:
the carrier of T = X
and
A20:
the topology of T = UniCl P
; ( T is TopSpace & ( for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9 ) )
then
P is covering
by Th1;
hence
T is TopSpace
by A19, A20, A6, Th2; for T9 being non empty TopSpace st T9 = T holds
B is Neighborhood_System of T9
let T9 be non empty TopSpace; ( T9 = T implies B is Neighborhood_System of T9 )
assume A23:
T9 = T
; B is Neighborhood_System of T9
then reconsider B9 = B as ManySortedSet of T9 by A19;
B9 is Neighborhood_System of T9
proof
let x be
Point of
T9;
TOPGEN_2:def 3 B9 . x is Element of bool (bool the carrier of T9)
A24:
B9 . x in rng B
by A2, A19, A23, FUNCT_1:def 3;
then reconsider Bx =
B9 . x as
Subset-Family of
T9 by A1, A19, A23;
Bx is
Basis of
x
proof
A25:
P c= UniCl P
by CANTOR_1:1;
Bx c= P
by A24, ZFMISC_1:74;
then
Bx c= the
topology of
T9
by A25, A20, A23;
then A26:
Bx is
open
by TOPS_2:64;
Bx is
x -quasi_basis
proof
for
a being
set st
a in Bx holds
x in a
by A3, A19, A23;
hence
x in Intersect Bx
by SETFAM_1:43;
YELLOW_8:def 1 for b1 being Element of bool the carrier of T9 holds
( not b1 is open or not x in b1 or ex b2 being Element of bool the carrier of T9 st
( b2 in Bx & b2 c= b1 ) )
let A be
Subset of
T9;
( not A is open or not x in A or ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A ) )
assume
A in the
topology of
T9
;
PRE_TOPC:def 2 ( not x in A or ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A ) )
then consider Y being
Subset-Family of
T9 such that A27:
Y c= P
and A28:
A = union Y
by A19, A20, A23, CANTOR_1:def 1;
assume
x in A
;
ex b1 being Element of bool the carrier of T9 st
( b1 in Bx & b1 c= A )
then consider a being
set such that A29:
x in a
and A30:
a in Y
by A28, TARSKI:def 4;
ex
b being
object st
(
b in dom B &
a in B . b )
by A27, A30, CARD_5:2;
then A31:
ex
V being
set st
(
V in B . x &
V c= a )
by A4, A29;
a c= A
by A28, A30, ZFMISC_1:74;
hence
ex
b1 being
Element of
bool the
carrier of
T9 st
(
b1 in Bx &
b1 c= A )
by A31, XBOOLE_1:1;
verum
end;
hence
Bx is
Basis of
x
by A26;
verum
end;
hence
B9 . x is
Element of
bool (bool the carrier of T9)
;
verum
end;
hence
B is Neighborhood_System of T9
; verum