let I be 2 -element set ; for J being non-Empty TopSpace-yielding ManySortedSet of I
for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
let J be non-Empty TopSpace-yielding ManySortedSet of I; for i, j being Element of I
for P being Subset of (product (Carrier J)) st i <> j holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
let i, j be Element of I; for P being Subset of (product (Carrier J)) st i <> j holds
( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
let P be Subset of (product (Carrier J)); ( i <> j implies ( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) ) )
assume A1:
i <> j
; ( P in FinMeetCl (product_prebasis J) iff ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
hence
( P in FinMeetCl (product_prebasis J) implies ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) )
by Lm9; ( ex V being Subset of (J . i) ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) ) implies P in FinMeetCl (product_prebasis J) )
given V being Subset of (J . i), W being Subset of (J . j) such that A2:
( V is open & W is open & P = product ((i,j) --> (V,W)) )
; P in FinMeetCl (product_prebasis J)
ex Y being Subset-Family of (product (Carrier J)) st
( Y c= product_prebasis J & Y is finite & P = Intersect Y )
proof
set V0 =
product ((Carrier J) +* (i,V));
set W0 =
product ((Carrier J) +* (j,W));
set Y =
{(product ((Carrier J) +* (i,V))),(product ((Carrier J) +* (j,W)))};
A3:
dom (Carrier J) = I
by PARTFUN1:def 2;
(
(Carrier J) . i = [#] (J . i) &
(Carrier J) . j = [#] (J . j) )
by PENCIL_3:7;
then a4:
(
(Carrier J) . i = the
carrier of
(J . i) &
(Carrier J) . j = the
carrier of
(J . j) )
by STRUCT_0:def 3;
A5:
(
product ((Carrier J) +* (i,V)) c= product (Carrier J) &
product ((Carrier J) +* (j,W)) c= product (Carrier J) )
by a4, A3, Th39;
then reconsider Y =
{(product ((Carrier J) +* (i,V))),(product ((Carrier J) +* (j,W)))} as
Subset-Family of
(product (Carrier J)) by ZFMISC_1:32;
take
Y
;
( Y c= product_prebasis J & Y is finite & P = Intersect Y )
A6:
(
product ((Carrier J) +* (i,V)) = product ((i,j) --> (V,((Carrier J) . j))) &
product ((Carrier J) +* (j,W)) = product ((i,j) --> (((Carrier J) . i),W)) )
by A1, Th34;
then
(
product ((Carrier J) +* (i,V)) = product ((i,j) --> (V,([#] (J . j)))) &
product ((Carrier J) +* (j,W)) = product ((i,j) --> (([#] (J . i)),W)) )
by PENCIL_3:7;
then
(
product ((Carrier J) +* (i,V)) in product_prebasis J &
product ((Carrier J) +* (j,W)) in product_prebasis J )
by A1, A2, A5, Th69;
hence
(
Y c= product_prebasis J &
Y is
finite )
by ZFMISC_1:32;
P = Intersect Y
(
P c= product ((Carrier J) +* (i,V)) &
P c= product ((Carrier J) +* (j,W)) )
by A2, a4, A6, Th28;
then A7:
P c= (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W)))
by XBOOLE_1:19;
(product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) c= P
proof
let x be
object ;
TARSKI:def 3 ( not x in (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W))) or x in P )
assume
x in (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W)))
;
x in P
then A8:
(
x in product ((Carrier J) +* (i,V)) &
x in product ((Carrier J) +* (j,W)) )
by XBOOLE_0:def 4;
then consider g being
Function such that A9:
(
g = x &
dom g = dom ((i,j) --> (V,((Carrier J) . j))) )
and A10:
for
y being
object st
y in dom ((i,j) --> (V,((Carrier J) . j))) holds
g . y in ((i,j) --> (V,((Carrier J) . j))) . y
by A6, CARD_3:def 5;
A12:
dom g =
{i,j}
by A9, FUNCT_4:62
.=
dom ((i,j) --> (V,W))
by FUNCT_4:62
;
for
y being
object st
y in dom ((i,j) --> (V,W)) holds
g . y in ((i,j) --> (V,W)) . y
proof
let y be
object ;
( y in dom ((i,j) --> (V,W)) implies g . y in ((i,j) --> (V,W)) . y )
assume
y in dom ((i,j) --> (V,W))
;
g . y in ((i,j) --> (V,W)) . y
then A13:
y in {i,j}
by FUNCT_4:62;
per cases then
( y = i or y = j )
by TARSKI:def 2;
suppose A14:
y = i
;
g . y in ((i,j) --> (V,W)) . ythen A15:
((i,j) --> (V,((Carrier J) . j))) . y =
V
by A1, FUNCT_4:63
.=
((i,j) --> (V,W)) . y
by A1, A14, FUNCT_4:63
;
y in dom ((i,j) --> (V,((Carrier J) . j)))
by A13, FUNCT_4:62;
hence
g . y in ((i,j) --> (V,W)) . y
by A10, A15;
verum end; suppose A16:
y = j
;
g . y in ((i,j) --> (V,W)) . ythen A17:
((i,j) --> (((Carrier J) . i),W)) . y =
W
by FUNCT_4:63
.=
((i,j) --> (V,W)) . y
by A16, FUNCT_4:63
;
y in dom ((i,j) --> (((Carrier J) . i),W))
by A13, FUNCT_4:62;
hence
g . y in ((i,j) --> (V,W)) . y
by A6, A8, A9, CARD_3:9, A17;
verum end;
end;
hence
x in P
by A2, A9, A12, CARD_3:9;
verum
end;
then
P = (product ((Carrier J) +* (i,V))) /\ (product ((Carrier J) +* (j,W)))
by A7, XBOOLE_0:def 10;
then
P = meet Y
by SETFAM_1:11;
hence
P = Intersect Y
by SETFAM_1:def 9;
verum
end;
hence
P in FinMeetCl (product_prebasis J)
by CANTOR_1:def 3; verum