set t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } ;
{ (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be
object ;
TARSKI:def 3 ( not e in { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } or e in bool [: the carrier of X, the carrier of Y:] )
assume
e in { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } }
;
e in bool [: the carrier of X, the carrier of Y:]
then
ex
A being
Subset-Family of
[: the carrier of X, the carrier of Y:] st
(
e = union A &
A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } )
;
hence
e in bool [: the carrier of X, the carrier of Y:]
;
verum
end;
then reconsider t = { (union A) where A is Subset-Family of [: the carrier of X, the carrier of Y:] : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } as Subset-Family of [: the carrier of X, the carrier of Y:] ;
set T = TopStruct(# [: the carrier of X, the carrier of Y:],t #);
now ( the carrier of TopStruct(# [: the carrier of X, the carrier of Y:],t #) in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & ( for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) )reconsider A =
{[: the carrier of X, the carrier of Y:]} as
Subset-Family of
[: the carrier of X, the carrier of Y:] by ZFMISC_1:68;
reconsider A =
A as
Subset-Family of
[: the carrier of X, the carrier of Y:] ;
A1:
A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
the
carrier of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
= union A
;
hence
the
carrier of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
by A1;
( ( for a being Subset-Family of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) & ( for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) ) )thus
for
a being
Subset-Family of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #) st
a c= the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #) holds
union a in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
for a, b being Subset of TopStruct(# [: the carrier of X, the carrier of Y:],t #) st a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) holds
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)proof
let a be
Subset-Family of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #);
( a c= the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )
set A =
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } ;
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be
object ;
TARSKI:def 3 ( not e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } or e in bool [: the carrier of X, the carrier of Y:] )
assume
e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) }
;
e in bool [: the carrier of X, the carrier of Y:]
then
ex
X1 being
Subset of
X ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y & ex
x being
set st
(
x in a &
[:X1,Y1:] c= x ) )
;
hence
e in bool [: the carrier of X, the carrier of Y:]
;
verum
end;
then reconsider A =
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & ex x being set st
( x in a & [:X1,Y1:] c= x ) ) } as
Subset-Family of
[: the carrier of X, the carrier of Y:] ;
assume A3:
a c= the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
;
union a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)
A4:
union A = union a
proof
thus
union A c= union a
XBOOLE_0:def 10 union a c= union Aproof
let e1,
e2 be
object ;
RELAT_1:def 3 ( not [e1,e2] in union A or [e1,e2] in union a )
assume
[e1,e2] in union A
;
[e1,e2] in union a
then consider u being
set such that A5:
[e1,e2] in u
and A6:
u in A
by TARSKI:def 4;
ex
X1 being
Subset of
X ex
Y1 being
Subset of
Y st
(
u = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y & ex
x being
set st
(
x in a &
[:X1,Y1:] c= x ) )
by A6;
hence
[e1,e2] in union a
by A5, TARSKI:def 4;
verum
end;
let e be
object ;
TARSKI:def 3 ( not e in union a or e in union A )
assume
e in union a
;
e in union A
then consider u being
set such that A7:
e in u
and A8:
u in a
by TARSKI:def 4;
u in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
by A3, A8;
then consider B being
Subset-Family of
[: the carrier of X, the carrier of Y:] such that A9:
u = union B
and A10:
B c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
;
consider x being
set such that A11:
e in x
and A12:
x in B
by A7, A9, TARSKI:def 4;
x in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
by A10, A12;
then consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A13:
x = [:X1,Y1:]
and A14:
(
X1 in the
topology of
X &
Y1 in the
topology of
Y )
;
[:X1,Y1:] c= u
by A9, A12, A13, ZFMISC_1:74;
then
x in A
by A8, A13, A14;
hence
e in union A
by A11, TARSKI:def 4;
verum
end;
A c= { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) }
hence
union a in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
by A4;
verum
end; let a,
b be
Subset of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #);
( a in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) & b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) implies a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #) )set C =
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } ;
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } c= bool [: the carrier of X, the carrier of Y:]
proof
let e be
object ;
TARSKI:def 3 ( not e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } or e in bool [: the carrier of X, the carrier of Y:] )
assume
e in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) }
;
e in bool [: the carrier of X, the carrier of Y:]
then
ex
X1 being
Subset of
X ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y &
[:X1,Y1:] c= a /\ b )
;
hence
e in bool [: the carrier of X, the carrier of Y:]
;
verum
end; then reconsider C =
{ [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y & [:X1,Y1:] c= a /\ b ) } as
Subset-Family of
[: the carrier of X, the carrier of Y:] ;
assume that A15:
a in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
and A16:
b in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
;
a /\ b in the topology of TopStruct(# [: the carrier of X, the carrier of Y:],t #)consider A being
Subset-Family of
[: the carrier of X, the carrier of Y:] such that A17:
a = union A
and A18:
A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
by A15;
consider B being
Subset-Family of
[: the carrier of X, the carrier of Y:] such that A19:
b = union B
and A20:
B c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
by A16;
A21:
a /\ b = union C
proof
thus
a /\ b c= union C
XBOOLE_0:def 10 union C c= a /\ bproof
let e be
object ;
TARSKI:def 3 ( not e in a /\ b or e in union C )
assume A22:
e in a /\ b
;
e in union C
then
e in a
by XBOOLE_0:def 4;
then consider u1 being
set such that A23:
e in u1
and A24:
u1 in A
by A17, TARSKI:def 4;
A25:
u1 in { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
by A18, A24;
e in b
by A22, XBOOLE_0:def 4;
then consider u2 being
set such that A26:
e in u2
and A27:
u2 in B
by A19, TARSKI:def 4;
A28:
u2 in { [:X2,Y2:] where X2 is Subset of X, Y2 is Subset of Y : ( X2 in the topology of X & Y2 in the topology of Y ) }
by A20, A27;
A29:
u2 c= b
by A19, A27, ZFMISC_1:74;
consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A30:
u1 = [:X1,Y1:]
and A31:
(
X1 in the
topology of
X &
Y1 in the
topology of
Y )
by A25;
consider X2 being
Subset of
X,
Y2 being
Subset of
Y such that A32:
u2 = [:X2,Y2:]
and A33:
(
X2 in the
topology of
X &
Y2 in the
topology of
Y )
by A28;
u1 c= a
by A17, A24, ZFMISC_1:74;
then
[:X1,Y1:] /\ [:X2,Y2:] c= a /\ b
by A30, A32, A29, XBOOLE_1:27;
then A34:
[:(X1 /\ X2),(Y1 /\ Y2):] c= a /\ b
by ZFMISC_1:100;
(
X1 /\ X2 in the
topology of
X &
Y1 /\ Y2 in the
topology of
Y )
by A31, A33, PRE_TOPC:def 1;
then A35:
[:(X1 /\ X2),(Y1 /\ Y2):] in C
by A34;
e in [:(X1 /\ X2),(Y1 /\ Y2):]
by A23, A26, A30, A32, ZFMISC_1:113;
hence
e in union C
by A35, TARSKI:def 4;
verum
end;
let e1,
e2 be
object ;
RELAT_1:def 3 ( not [e1,e2] in union C or [e1,e2] in a /\ b )
assume
[e1,e2] in union C
;
[e1,e2] in a /\ b
then consider u being
set such that A36:
[e1,e2] in u
and A37:
u in C
by TARSKI:def 4;
ex
X1 being
Subset of
X ex
Y1 being
Subset of
Y st
(
u = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y &
[:X1,Y1:] c= a /\ b )
by A37;
hence
[e1,e2] in a /\ b
by A36;
verum
end;
C c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) }
hence
a /\ b in the
topology of
TopStruct(#
[: the carrier of X, the carrier of Y:],
t #)
by A21;
verum end;
then reconsider T = TopStruct(# [: the carrier of X, the carrier of Y:],t #) as strict TopSpace by PRE_TOPC:def 1;
take
T
; ( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T = { (union A) where A is Subset-Family of T : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } )
thus
( the carrier of T = [: the carrier of X, the carrier of Y:] & the topology of T = { (union A) where A is Subset-Family of T : A c= { [:X1,Y1:] where X1 is Subset of X, Y1 is Subset of Y : ( X1 in the topology of X & Y1 in the topology of Y ) } } )
; verum