let I be non empty set ; :: thesis: { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } is prebasis of product (I --> Sierpinski_Space )
set IS = I --> Sierpinski_Space ;
set pB = { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } ;
set P = product_prebasis (I --> Sierpinski_Space );
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } c= bool the carrier of (product (I --> Sierpinski_Space ))
then reconsider B = { (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } as Subset-Family of (product (I --> Sierpinski_Space )) ;
reconsider B = B as Subset-Family of (product (I --> Sierpinski_Space )) ;
A12:
B c= product_prebasis (I --> Sierpinski_Space )
A17:
product_prebasis (I --> Sierpinski_Space ) is prebasis of product (I --> Sierpinski_Space )
by Def3;
then A18:
product_prebasis (I --> Sierpinski_Space ) c= the topology of (product (I --> Sierpinski_Space ))
by CANTOR_1:def 5;
reconsider P = product_prebasis (I --> Sierpinski_Space ) as Subset-Family of (product (I --> Sierpinski_Space )) by Def3;
reconsider P = P as Subset-Family of (product (I --> Sierpinski_Space )) ;
FinMeetCl P is Basis of product (I --> Sierpinski_Space )
by A17, YELLOW_9:23;
then reconsider F = (FinMeetCl P) \ {{} } as Basis of product (I --> Sierpinski_Space ) by Th3;
A19:
F c= FinMeetCl B
proof
let x be
set ;
:: according to TARSKI:def 3 :: thesis: ( not x in F or x in FinMeetCl B )
assume A20:
x in F
;
:: thesis: x in FinMeetCl B
then reconsider y =
x as
Subset of
(product (I --> Sierpinski_Space )) ;
A21:
not
x in {{} }
by A20, XBOOLE_0:def 5;
x in FinMeetCl P
by A20, XBOOLE_0:def 5;
then consider Y1 being
Subset-Family of
(product (I --> Sierpinski_Space )) such that A22:
Y1 c= P
and A23:
Y1 is
finite
and A24:
y = Intersect Y1
by CANTOR_1:def 4;
A25:
the
carrier of
(product (I --> Sierpinski_Space )) = product (Carrier (I --> Sierpinski_Space ))
by Def3;
reconsider Y2 =
Y1 /\ B as
Subset-Family of
(product (I --> Sierpinski_Space )) ;
A26:
Y2 c= B
by XBOOLE_1:17;
A27:
Y2 is
finite
by A23, FINSET_1:13, XBOOLE_1:17;
A28:
Intersect Y1 c= Intersect Y2
by SETFAM_1:59, XBOOLE_1:17;
Intersect Y2 c= Intersect Y1
proof
let z be
set ;
:: according to TARSKI:def 3 :: thesis: ( not z in Intersect Y2 or z in Intersect Y1 )
assume A29:
z in Intersect Y2
;
:: thesis: z in Intersect Y1
then A30:
z in product (Carrier (I --> Sierpinski_Space ))
by A25;
for
Y being
set st
Y in Y1 holds
z in Y
proof
let Y be
set ;
:: thesis: ( Y in Y1 implies z in Y )
assume A31:
Y in Y1
;
:: thesis: z in Y
then reconsider Y' =
Y as
Subset of
(product (Carrier (I --> Sierpinski_Space ))) by Def3;
consider i being
set ,
S being
TopStruct ,
V being
Subset of
S such that A32:
i in I
and A33:
V is
open
and A34:
S = (I --> Sierpinski_Space ) . i
and A35:
Y' = product ((Carrier (I --> Sierpinski_Space )) +* i,V)
by A22, A31, Def2;
consider RR being
1-sorted such that A36:
RR = (I --> Sierpinski_Space ) . i
and A37:
(Carrier (I --> Sierpinski_Space )) . i = the
carrier of
RR
by A32, PRALG_1:def 13;
A38:
i in dom (Carrier (I --> Sierpinski_Space ))
by A32, PARTFUN1:def 4;
reconsider V' =
V as
Subset of
Sierpinski_Space by A32, A34, FUNCOP_1:13;
V in the
topology of
S
by A33, PRE_TOPC:def 5;
then
V' in the
topology of
Sierpinski_Space
by A32, A34, FUNCOP_1:13;
then A39:
V' in {{} ,{1},{0 ,1}}
by Def9;
A40:
V' <> {}
proof
assume A41:
V' = {}
;
:: thesis: contradiction
A42:
((Carrier (I --> Sierpinski_Space )) +* i,{} ) . i = {}
by A38, FUNCT_7:33;
i in dom ((Carrier (I --> Sierpinski_Space )) +* i,{} )
by A38, FUNCT_7:32;
then
{} in rng ((Carrier (I --> Sierpinski_Space )) +* i,{} )
by A42, FUNCT_1:def 5;
then
Y' = {}
by A35, A41, CARD_3:37;
then
y = {}
by A24, A31, MSSUBFAM:3;
hence
contradiction
by A21, TARSKI:def 1;
:: thesis: verum
end;
reconsider i' =
i as
Element of
I by A32;
end;
hence
z in Intersect Y1
by A29, SETFAM_1:58;
:: thesis: verum
end;
then
y = Intersect Y2
by A24, A28, XBOOLE_0:def 10;
hence
x in FinMeetCl B
by A26, A27, CANTOR_1:def 4;
:: thesis: verum
end;
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } c= the topology of (product (I --> Sierpinski_Space ))
by A12, A18, XBOOLE_1:1;
hence
{ (product ((Carrier (I --> Sierpinski_Space )) +* i,{1})) where i is Element of I : verum } is prebasis of product (I --> Sierpinski_Space )
by A19, CANTOR_1:def 5; :: thesis: verum