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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) } }
;
:: thesis: 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:]
;
:: thesis: 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 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:80;
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
by ZFMISC_1:31;
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;
:: thesis: ( ( 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 #)
:: thesis: 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 #);
:: thesis: ( 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 #) )
assume A3:
a c= the
topology of
TopStruct(#
[:the carrier of X,the carrier of Y:],
t #)
;
:: thesis: 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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) ) }
;
:: thesis: 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:]
;
:: thesis: 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:] ;
A4:
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 ) }
union A = union a
proof
thus
union A c= union a
:: according to XBOOLE_0:def 10 :: thesis: union a c= union Aproof
let e1,
e2 be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [e1,e2] in union A or [e1,e2] in union a )
assume
[e1,e2] in union A
;
:: thesis: [e1,e2] in union a
then consider u being
set such that A5:
(
[e1,e2] in u &
u in A )
by TARSKI:def 4;
consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A6:
u = [:X1,Y1:]
and
(
X1 in the
topology of
X &
Y1 in the
topology of
Y )
and A7:
ex
x being
set st
(
x in a &
[:X1,Y1:] c= x )
by A5;
thus
[e1,e2] in union a
by A5, A6, A7, TARSKI:def 4;
:: thesis: verum
end;
let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( not e in union a or e in union A )
assume
e in union a
;
:: thesis: e in union A
then consider u being
set such that A8:
(
e in u &
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 &
x in B )
by A8, 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, A11;
then consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A12:
(
x = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y )
;
[:X1,Y1:] c= u
by A9, A11, A12, ZFMISC_1:92;
then
x in A
by A8, A12;
hence
e in union A
by A11, TARSKI:def 4;
:: thesis: verum
end;
hence
union a in the
topology of
TopStruct(#
[:the carrier of X,the carrier of Y:],
t #)
by A4;
:: thesis: verum
end; let a,
b be
Subset of
TopStruct(#
[:the carrier of X,the carrier of Y:],
t #);
:: thesis: ( 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 #) )assume that A13:
a in the
topology of
TopStruct(#
[:the carrier of X,the carrier of Y:],
t #)
and A14:
b in the
topology of
TopStruct(#
[:the carrier of X,the carrier of Y:],
t #)
;
:: thesis: 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 A15:
a = union A
and A16:
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 A13;
consider B being
Subset-Family of
[:the carrier of X,the carrier of Y:] such that A17:
b = union B
and A18:
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 A14;
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
set ;
:: according to TARSKI:def 3 :: thesis: ( 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 ) }
;
:: thesis: 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:]
;
:: thesis: 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:] ;
A19:
a /\ b = union C
proof
thus
a /\ b c= union C
:: according to XBOOLE_0:def 10 :: thesis: union C c= a /\ bproof
let e be
set ;
:: according to TARSKI:def 3 :: thesis: ( not e in a /\ b or e in union C )
assume
e in a /\ b
;
:: thesis: e in union C
then A20:
(
e in a &
e in b )
by XBOOLE_0:def 4;
then consider u1 being
set such that A21:
(
e in u1 &
u1 in A )
by A15, TARSKI:def 4;
consider u2 being
set such that A22:
(
e in u2 &
u2 in B )
by A17, A20, TARSKI:def 4;
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 A16, A21;
then consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A23:
(
u1 = [:X1,Y1:] &
X1 in the
topology of
X &
Y1 in the
topology of
Y )
;
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 A18, A22;
then consider X2 being
Subset of
X,
Y2 being
Subset of
Y such that A24:
(
u2 = [:X2,Y2:] &
X2 in the
topology of
X &
Y2 in the
topology of
Y )
;
A25:
(
X1 /\ X2 in the
topology of
X &
Y1 /\ Y2 in the
topology of
Y )
by A23, A24, PRE_TOPC:def 1;
(
u1 c= a &
u2 c= b )
by A15, A17, A21, A22, ZFMISC_1:92;
then
[:X1,Y1:] /\ [:X2,Y2:] c= a /\ b
by A23, A24, XBOOLE_1:27;
then
[:(X1 /\ X2),(Y1 /\ Y2):] c= a /\ b
by ZFMISC_1:123;
then A26:
[:(X1 /\ X2),(Y1 /\ Y2):] in C
by A25;
e in [:(X1 /\ X2),(Y1 /\ Y2):]
by A21, A22, A23, A24, ZFMISC_1:137;
hence
e in union C
by A26, TARSKI:def 4;
:: thesis: verum
end;
let e1,
e2 be
set ;
:: according to RELAT_1:def 3 :: thesis: ( not [e1,e2] in union C or [e1,e2] in a /\ b )
assume
[e1,e2] in union C
;
:: thesis: [e1,e2] in a /\ b
then consider u being
set such that A27:
(
[e1,e2] in u &
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 A27;
hence
[e1,e2] in a /\ b
by A27;
:: thesis: 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 A19;
:: thesis: 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
; :: thesis: ( 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 ) } } )
; :: thesis: verum