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 & P in FinMeetCl (product_prebasis J) holds
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 & P in FinMeetCl (product_prebasis J) holds
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 & P in FinMeetCl (product_prebasis J) holds
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 & 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)) ) )
assume A1:
( i <> j & P in FinMeetCl (product_prebasis J) )
; 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)) )
then consider X being Subset-Family of (product (Carrier J)), f being I -valued one-to-one Function such that
A2:
( X c= product_prebasis J & X is finite & P = Intersect X & dom f = X )
and
A3:
P = product ((Carrier J) +* (product_basis_selector (J,f)))
by Lm3;
set F = (Carrier J) +* (product_basis_selector (J,f));
( i in I & j in I )
;
then A4:
( i in dom (Carrier J) & j in dom (Carrier J) )
by PARTFUN1:def 2;
rng f c= I
;
then
rng f c= {i,j}
by A1, Th8;
per cases then
( rng f = {} or rng f = {i} or rng f = {j} or rng f = {i,j} )
by ZFMISC_1:36;
suppose
rng f = {}
;
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)) )then
product_basis_selector (
J,
f)
= {}
;
then A5:
P =
product ((i,j) --> (((Carrier J) . i),((Carrier J) . j)))
by A1, A3, Th9
.=
product ((i,j) --> (([#] (J . i)),((Carrier J) . j)))
by PENCIL_3:7
.=
product ((i,j) --> (([#] (J . i)),([#] (J . j))))
by PENCIL_3:7
;
thus
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 A5;
verum end; suppose A6:
rng f = {i}
;
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)) )then A7:
dom f = {((f ") . i)}
by Th1;
A8:
i in rng f
by A6, TARSKI:def 1;
A9:
(f ") . i in X
by A2, A7, TARSKI:def 1;
then reconsider V0 =
(f ") . i as
Subset of
(product (Carrier J)) ;
reconsider V =
(proj (J,i)) .: V0 as
Subset of
(J . i) ;
take
V
;
ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )take
[#] (J . j)
;
( V is open & [#] (J . j) is open & P = product ((i,j) --> (V,([#] (J . j)))) )
(
V0 is
empty or not
V0 is
empty )
;
hence
(
V is
open &
[#] (J . j) is
open )
by A2, A9, Th58;
P = product ((i,j) --> (V,([#] (J . j)))) product_basis_selector (
J,
f) =
{i} --> ((product_basis_selector (J,f)) . i)
by A6, Th7
.=
{i} --> ((proj (J,i)) .: ((f ") . i))
by A8, Th54
.=
i .--> V
by FUNCOP_1:def 9
;
then (Carrier J) +* (product_basis_selector (J,f)) =
(Carrier J) +* (
i,
V)
by A4, FUNCT_7:def 3
.=
(
i,
j)
--> (
V,
((Carrier J) . j))
by A1, Th34
.=
(
i,
j)
--> (
V,
([#] (J . j)))
by PENCIL_3:7
;
hence
P = product ((i,j) --> (V,([#] (J . j))))
by A3;
verum end; suppose A10:
rng f = {j}
;
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)) )then A11:
dom f = {((f ") . j)}
by Th1;
A12:
j in rng f
by A10, TARSKI:def 1;
A13:
(f ") . j in X
by A2, A11, TARSKI:def 1;
then reconsider W0 =
(f ") . j as
Subset of
(product (Carrier J)) ;
reconsider W =
(proj (J,j)) .: W0 as
Subset of
(J . j) ;
take
[#] (J . i)
;
ex W being Subset of (J . j) st
( [#] (J . i) is open & W is open & P = product ((i,j) --> (([#] (J . i)),W)) )take
W
;
( [#] (J . i) is open & W is open & P = product ((i,j) --> (([#] (J . i)),W)) )thus
[#] (J . i) is
open
;
( W is open & P = product ((i,j) --> (([#] (J . i)),W)) )
(
W0 is
empty or not
W0 is
empty )
;
hence
W is
open
by A2, A13, Th58;
P = product ((i,j) --> (([#] (J . i)),W)) product_basis_selector (
J,
f) =
{j} --> ((product_basis_selector (J,f)) . j)
by A10, Th7
.=
{j} --> ((proj (J,j)) .: ((f ") . j))
by A12, Th54
.=
j .--> W
by FUNCOP_1:def 9
;
then (Carrier J) +* (product_basis_selector (J,f)) =
(Carrier J) +* (
j,
W)
by A4, FUNCT_7:def 3
.=
(
i,
j)
--> (
((Carrier J) . i),
W)
by A1, Th34
.=
(
i,
j)
--> (
([#] (J . i)),
W)
by PENCIL_3:7
;
hence
P = product ((i,j) --> (([#] (J . i)),W))
by A3;
verum end; suppose A14:
rng f = {i,j}
;
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)) )then A15:
dom f = {((f ") . i),((f ") . j)}
by Th2;
A16:
(
i in rng f &
j in rng f )
by A14, TARSKI:def 2;
A17:
(
(f ") . i in X &
(f ") . j in X )
by A2, A15, TARSKI:def 2;
then reconsider V0 =
(f ") . i as
Subset of
(product (Carrier J)) ;
reconsider V =
(proj (J,i)) .: V0 as
Subset of
(J . i) ;
reconsider W0 =
(f ") . j as
Subset of
(product (Carrier J)) by A17;
reconsider W =
(proj (J,j)) .: W0 as
Subset of
(J . j) ;
take
V
;
ex W being Subset of (J . j) st
( V is open & W is open & P = product ((i,j) --> (V,W)) )take
W
;
( V is open & W is open & P = product ((i,j) --> (V,W)) )
(
V0 is
empty or not
V0 is
empty )
;
hence
V is
open
by A2, A17, Th58;
( W is open & P = product ((i,j) --> (V,W)) )
(
W0 is
empty or not
W0 is
empty )
;
hence
W is
open
by A2, A17, Th58;
P = product ((i,j) --> (V,W))
rng f = I
by A1, A14, Th8;
then A18:
product_basis_selector (
J,
f) =
(
i,
j)
--> (
((product_basis_selector (J,f)) . i),
((product_basis_selector (J,f)) . j))
by A1, Th9
.=
(
i,
j)
--> (
((product_basis_selector (J,f)) . i),
((proj (J,j)) .: ((f ") . j)))
by A16, Th54
.=
(
i,
j)
--> (
V,
W)
by A16, Th54
;
dom (Carrier J) =
I
by PARTFUN1:def 2
.=
{i,j}
by A1, Th8
;
then
dom (Carrier J) = dom (product_basis_selector (J,f))
by A14, PARTFUN1:def 2;
hence
P = product ((i,j) --> (V,W))
by A3, A18, FUNCT_4:19;
verum end;