let M be non empty set ; :: thesis: for J being non-Empty TopStruct-yielding ManySortedSet of M
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 TopStruct-yielding ManySortedSet of M; :: 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 object 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
reconsider G9 = G as Subset of (J . i) ;
( [#] (J . i) <> {} & proj (J,i) is continuous ) by WAYBEL18:5;
then A8: (proj (J,i)) " G9 is open by A6, TOPS_2:43;
A9: for z being object st z in dom ((Carrier J) +* (i,G)) holds
f . z in ((Carrier J) +* (i,G)) . z
proof
let z be object ; :: thesis: ( z in dom ((Carrier J) +* (i,G)) implies f . z in ((Carrier J) +* (i,G)) . z )
assume z in dom ((Carrier J) +* (i,G)) ; :: thesis: f . z in ((Carrier J) +* (i,G)) . z
then A10: z in dom (Carrier J) by FUNCT_7:30;
per cases ( z = i or z <> i ) ;
suppose z = i ; :: thesis: f . z in ((Carrier J) +* (i,G)) . z
hence f . z in ((Carrier J) +* (i,G)) . z by A2, A7, A10, FUNCT_7:31; :: thesis: verum
end;
suppose z <> i ; :: thesis: f . z in ((Carrier J) +* (i,G)) . z
then ((Carrier J) +* (i,G)) . z = (Carrier J) . z by FUNCT_7:32;
hence f . z in ((Carrier J) +* (i,G)) . z by A4, A10; :: thesis: verum
end;
end;
end;
A11: product ((Carrier J) +* (i,G9)) = (proj (J,i)) " G9 by WAYBEL18:4;
dom f = dom ((Carrier J) +* (i,G)) by A3, FUNCT_7:30;
then x in product ((Carrier J) +* (i,G)) by A2, A9, CARD_3:def 5;
then {y} meets (proj (J,i)) " G9 by A1, A8, A11, PRE_TOPC:def 7;
then y in product ((Carrier J) +* (i,G)) by A11, ZFMISC_1:50;
then consider g being Function such that
A12: y = g and
dom g = dom ((Carrier J) +* (i,G)) and
A13: for z being object st z in dom ((Carrier J) +* (i,G)) holds
g . z in ((Carrier J) +* (i,G)) . z by CARD_3:def 5;
A14: i in dom (Carrier J) by A5, PARTFUN1:def 2;
then i in dom ((Carrier J) +* (i,G)) by FUNCT_7:30;
then g . i in ((Carrier J) +* (i,G)) . i by A13;
then g . i in G by A14, FUNCT_7:31;
hence {(y . i)} meets G by A12, ZFMISC_1:48; :: thesis: verum
end;
hence x . i in Cl {(y . i)} by PRE_TOPC:def 7; :: thesis: verum
end;
reconsider K = product_prebasis J as prebasis of (product J) by WAYBEL18:def 3;
assume A15: for i being Element of M holds x . i in Cl {(y . i)} ; :: thesis: x in Cl {y}
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
A16: Z c= K and
A17: x in Intersect Z ; :: thesis: Intersect Z meets {y}
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 )
y in the carrier of (product J) ;
then y in product (Carrier J) by WAYBEL18:def 3;
then consider g being Function such that
A18: y = g and
A19: dom g = dom (Carrier J) and
A20: for z being object st z in dom (Carrier J) holds
g . z in (Carrier J) . z by CARD_3:def 5;
assume A21: Y in Z ; :: thesis: y in Y
then Y in K by A16;
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 in Y by A17, A21, SETFAM_1:43;
then A26: ex f being Function st
( x = f & dom f = dom ((Carrier J) +* (i,V)) & ( for z being object st z in dom ((Carrier J) +* (i,V)) holds
f . z in ((Carrier J) +* (i,V)) . z ) ) by A25, CARD_3:def 5;
x . i in Cl {(y . i)} by A15;
then A27: ( x . i in V implies {(y . i)} meets V ) by A23, A24, PRE_TOPC:def 7;
A28: for z being object st z in dom ((Carrier J) +* (i,V)) holds
g . z in ((Carrier J) +* (i,V)) . z
proof
let z be object ; :: thesis: ( z in dom ((Carrier J) +* (i,V)) implies g . z in ((Carrier J) +* (i,V)) . z )
assume A29: z in dom ((Carrier J) +* (i,V)) ; :: thesis: g . z in ((Carrier J) +* (i,V)) . z
then A30: z in dom (Carrier J) by FUNCT_7:30;
per cases ( z = i or z <> i ) ;
suppose A31: z = i ; :: thesis: g . z in ((Carrier J) +* (i,V)) . z
then ((Carrier J) +* (i,V)) . z = V by A30, FUNCT_7:31;
hence g . z in ((Carrier J) +* (i,V)) . z by A27, A26, A18, A29, A31, ZFMISC_1:50; :: thesis: verum
end;
suppose z <> i ; :: thesis: g . z in ((Carrier J) +* (i,V)) . z
then ((Carrier J) +* (i,V)) . z = (Carrier J) . z by FUNCT_7:32;
hence g . z in ((Carrier J) +* (i,V)) . z by A20, A30; :: thesis: verum
end;
end;
end;
dom g = dom ((Carrier J) +* (i,V)) by A19, FUNCT_7:30;
hence y in Y by A25, A18, A28, CARD_3:def 5; :: thesis: verum
end;
then ( y in {y} & y in Intersect Z ) by SETFAM_1:43, TARSKI:def 1;
hence Intersect Z meets {y} by XBOOLE_0:3; :: thesis: verum
end;
hence x in Cl {y} by YELLOW_9:38; :: thesis: verum