let M be non empty set ; :: thesis: for J being non-Empty TopSpace-yielding ManySortedSet of
for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let J be non-Empty TopSpace-yielding ManySortedSet of ; :: thesis: for x, y being Point of (product J) holds
( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
let x, y be Point of (product J); :: thesis: ( x in Cl {y} iff for i being Element of M holds x . i in Cl {(y . i)} )
hereby :: thesis: ( ( for i being Element of M holds x . i in Cl {(y . i)} ) implies x in Cl {y} )
assume A1:
x in Cl {y}
;
:: thesis: for i being Element of M holds x . i in Cl {(y . i)}let i be
Element of
M;
:: thesis: x . i in Cl {(y . i)}
x in the
carrier of
(product J)
;
then
x in product (Carrier J)
by WAYBEL18:def 3;
then consider f being
Function such that A2:
x = f
and A3:
dom f = dom (Carrier J)
and A4:
for
z being
set st
z in dom (Carrier J) holds
f . z in (Carrier J) . z
by CARD_3:def 5;
A5:
i in M
;
for
G being
Subset of
(J . i) st
G is
open &
x . i in G holds
{(y . i)} meets G
proof
let G be
Subset of
(J . i);
:: thesis: ( G is open & x . i in G implies {(y . i)} meets G )
assume that A6:
G is
open
and A7:
x . i in G
;
:: thesis: {(y . i)} meets G
A8:
dom f = dom ((Carrier J) +* i,G)
by A3, FUNCT_7:32;
for
z being
set st
z in dom ((Carrier J) +* i,G) holds
f . z in ((Carrier J) +* i,G) . z
then A10:
x in product ((Carrier J) +* i,G)
by A2, A8, CARD_3:def 5;
reconsider G' =
G as
Subset of
(J . i) ;
A11:
[#] (J . i) <> {}
;
proj J,
i is
continuous
by WAYBEL18:6;
then A12:
(proj J,i) " G' is
open
by A6, A11, TOPS_2:55;
A13:
product ((Carrier J) +* i,G') = (proj J,i) " G'
by WAYBEL18:5;
then
{y} meets (proj J,i) " G'
by A1, A10, A12, PRE_TOPC:def 13;
then
y in product ((Carrier J) +* i,G)
by A13, ZFMISC_1:56;
then consider g being
Function such that A14:
y = g
and
dom g = dom ((Carrier J) +* i,G)
and A15:
for
z being
set st
z in dom ((Carrier J) +* i,G) holds
g . z in ((Carrier J) +* i,G) . z
by CARD_3:def 5;
A16:
i in dom (Carrier J)
by A5, PARTFUN1:def 4;
then
i in dom ((Carrier J) +* i,G)
by FUNCT_7:32;
then
g . i in ((Carrier J) +* i,G) . i
by A15;
then
g . i in G
by A16, FUNCT_7:33;
hence
{(y . i)} meets G
by A14, ZFMISC_1:54;
:: thesis: verum
end; hence
x . i in Cl {(y . i)}
by PRE_TOPC:def 13;
:: thesis: verum
end;
assume A17:
for i being Element of M holds x . i in Cl {(y . i)}
; :: thesis: x in Cl {y}
reconsider K = product_prebasis J as prebasis of product J by WAYBEL18:def 3;
for Z being finite Subset-Family of (product J) st Z c= K & x in Intersect Z holds
Intersect Z meets {y}
proof
let Z be
finite Subset-Family of
(product J);
:: thesis: ( Z c= K & x in Intersect Z implies Intersect Z meets {y} )
assume that A18:
Z c= K
and A19:
x in Intersect Z
;
:: thesis: Intersect Z meets {y}
A20:
y in {y}
by TARSKI:def 1;
for
Y being
set st
Y in Z holds
y in Y
proof
let Y be
set ;
:: thesis: ( Y in Z implies y in Y )
assume A21:
Y in Z
;
:: thesis: y in Y
then
Y in K
by A18;
then consider i being
set ,
W being
TopStruct ,
V being
Subset of
W such that A22:
i in M
and A23:
V is
open
and A24:
W = J . i
and A25:
Y = product ((Carrier J) +* i,V)
by WAYBEL18:def 2;
reconsider i =
i as
Element of
M by A22;
reconsider V =
V as
Subset of
(J . i) by A24;
x . i in Cl {(y . i)}
by A17;
then A26:
(
x . i in V implies
{(y . i)} meets V )
by A23, A24, PRE_TOPC:def 13;
x in Y
by A19, A21, SETFAM_1:58;
then consider f being
Function such that A27:
x = f
and
dom f = dom ((Carrier J) +* i,V)
and A28:
for
z being
set st
z in dom ((Carrier J) +* i,V) holds
f . z in ((Carrier J) +* i,V) . z
by A25, CARD_3:def 5;
y in the
carrier of
(product J)
;
then
y in product (Carrier J)
by WAYBEL18:def 3;
then consider g being
Function such that A29:
y = g
and A30:
dom g = dom (Carrier J)
and A31:
for
z being
set st
z in dom (Carrier J) holds
g . z in (Carrier J) . z
by CARD_3:def 5;
A32:
dom g = dom ((Carrier J) +* i,V)
by A30, FUNCT_7:32;
for
z being
set st
z in dom ((Carrier J) +* i,V) holds
g . z in ((Carrier J) +* i,V) . z
hence
y in Y
by A25, A29, A32, CARD_3:def 5;
:: thesis: verum
end;
then
y in Intersect Z
by SETFAM_1:58;
hence
Intersect Z meets {y}
by A20, XBOOLE_0:3;
:: thesis: verum
end;
hence
x in Cl {y}
by YELLOW_9:38; :: thesis: verum