let X, Y be TopSpace; :: thesis: for XV being SubSpace of X holds [:XV,Y:] is SubSpace of [:X,Y:]
let XV be SubSpace of X; :: thesis: [:XV,Y:] is SubSpace of [:X,Y:]
set S = [:XV,Y:];
set T = [:X,Y:];
A1:
the carrier of [:XV,Y:] = [:the carrier of XV,the carrier of Y:]
by BORSUK_1:def 5;
A2:
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:]
by BORSUK_1:def 5;
A3:
the carrier of XV c= the carrier of X
by BORSUK_1:35;
then A4:
[#] [:XV,Y:] c= [#] [:X,Y:]
by A1, A2, ZFMISC_1:119;
for P being Subset of [:XV,Y:] holds
( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) )
proof
let P be
Subset of
[:XV,Y:];
:: thesis: ( P in the topology of [:XV,Y:] iff ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) )
reconsider P' =
P as
Subset of
[:XV,Y:] ;
hereby :: thesis: ( ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) ) implies P in the topology of [:XV,Y:] )
assume
P in the
topology of
[:XV,Y:]
;
:: thesis: ex Q being Subset of [:X,Y:] st
( Q in the topology of [:X,Y:] & P = Q /\ ([#] [:XV,Y:]) )then
P' is
open
by PRE_TOPC:def 5;
then consider A being
Subset-Family of
[:XV,Y:] such that A5:
(
P' = union A & ( for
e being
set st
e in A holds
ex
X1 being
Subset of
XV ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open ) ) )
by BORSUK_1:45;
set AA =
{ [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A ) } ;
{ [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A ) } c= bool the
carrier of
[:X,Y:]
proof
let a be
set ;
:: according to TARSKI:def 3 :: thesis: ( not a in { [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A ) } or a in bool the carrier of [:X,Y:] )
assume
a in { [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A ) }
;
:: thesis: a in bool the carrier of [:X,Y:]
then consider Xx1 being
Subset of
X,
Yy2 being
Subset of
Y such that A6:
(
a = [:Xx1,Yy2:] & ex
Y1 being
Subset of
XV st
(
Y1 = Xx1 /\ ([#] XV) &
Xx1 is
open &
Yy2 is
open &
[:Y1,Yy2:] in A ) )
;
thus
a in bool the
carrier of
[:X,Y:]
by A6;
:: thesis: verum
end; then reconsider AA =
{ [:X1,Y2:] where X1 is Subset of X, Y2 is Subset of Y : ex Y1 being Subset of XV st
( Y1 = X1 /\ ([#] XV) & X1 is open & Y2 is open & [:Y1,Y2:] in A ) } as
Subset-Family of
[:X,Y:] ;
reconsider AA =
AA as
Subset-Family of
[:X,Y:] ;
AA c= the
topology of
[:X,Y:]
proof
let t be
set ;
:: according to TARSKI:def 3 :: thesis: ( not t in AA or t in the topology of [:X,Y:] )
assume
t in AA
;
:: thesis: t in the topology of [:X,Y:]
then consider Xx1 being
Subset of
X,
Yy2 being
Subset of
Y such that A7:
(
t = [:Xx1,Yy2:] & ex
Y1 being
Subset of
XV st
(
Y1 = Xx1 /\ ([#] XV) &
Xx1 is
open &
Yy2 is
open &
[:Y1,Yy2:] in A ) )
;
set A' =
{t};
{t} c= bool the
carrier of
[:X,Y:]
then reconsider A' =
{t} as
Subset-Family of
[:X,Y:] ;
A8:
t = union A'
by ZFMISC_1:31;
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 ) }
then
t in { (union As) where As is Subset-Family of [:X,Y:] : As 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 A8;
hence
t in the
topology of
[:X,Y:]
by BORSUK_1:def 5;
:: thesis: verum
end; then A10:
union AA in the
topology of
[:X,Y:]
by PRE_TOPC:def 1;
P = (union AA) /\ ([#] [:XV,Y:])
proof
thus
P c= (union AA) /\ ([#] [:XV,Y:])
:: according to XBOOLE_0:def 10 :: thesis: (union AA) /\ ([#] [:XV,Y:]) c= Pproof
let p be
set ;
:: according to TARSKI:def 3 :: thesis: ( not p in P or p in (union AA) /\ ([#] [:XV,Y:]) )
assume
p in P
;
:: thesis: p in (union AA) /\ ([#] [:XV,Y:])
then consider A1 being
set such that A11:
(
p in A1 &
A1 in A )
by A5, TARSKI:def 4;
reconsider A1 =
A1 as
Subset of
[:XV,Y:] by A11;
consider X2 being
Subset of
XV,
Y2 being
Subset of
Y such that A12:
(
A1 = [:X2,Y2:] &
X2 is
open &
Y2 is
open )
by A5, A11;
consider p1,
p2 being
set such that A13:
(
p1 in X2 &
p2 in Y2 &
p = [p1,p2] )
by A11, A12, ZFMISC_1:def 2;
X2 in the
topology of
XV
by A12, PRE_TOPC:def 5;
then consider Q1 being
Subset of
X such that A14:
(
Q1 in the
topology of
X &
X2 = Q1 /\ ([#] XV) )
by PRE_TOPC:def 9;
reconsider Q1 =
Q1 as
Subset of
X ;
set EX =
[:Q1,Y2:];
p1 in Q1
by A13, A14, XBOOLE_0:def 4;
then A15:
p in [:Q1,Y2:]
by A13, ZFMISC_1:106;
(
Q1 is
open &
[:X2,Y2:] in A )
by A11, A12, A14, PRE_TOPC:def 5;
then
[:Q1,Y2:] in { [:Xx1,Yy2:] where Xx1 is Subset of X, Yy2 is Subset of Y : ex Z1 being Subset of XV st
( Z1 = Xx1 /\ ([#] XV) & Xx1 is open & Yy2 is open & [:Z1,Yy2:] in A ) }
by A12, A14;
then
p in union AA
by A15, TARSKI:def 4;
hence
p in (union AA) /\ ([#] [:XV,Y:])
by A11, XBOOLE_0:def 4;
:: thesis: verum
end;
thus
(union AA) /\ ([#] [:XV,Y:]) c= P
:: thesis: verumproof
let h be
set ;
:: according to TARSKI:def 3 :: thesis: ( not h in (union AA) /\ ([#] [:XV,Y:]) or h in P )
assume A16:
h in (union AA) /\ ([#] [:XV,Y:])
;
:: thesis: h in P
then
(
h in union AA &
h in [#] [:XV,Y:] )
by XBOOLE_0:def 4;
then consider A2 being
set such that A17:
(
h in A2 &
A2 in AA )
by TARSKI:def 4;
consider Xx1 being
Subset of
X,
Yy2 being
Subset of
Y such that A18:
(
A2 = [:Xx1,Yy2:] & ex
Y1 being
Subset of
XV st
(
Y1 = Xx1 /\ ([#] XV) &
Xx1 is
open &
Yy2 is
open &
[:Y1,Yy2:] in A ) )
by A17;
consider p1,
p2 being
set such that A19:
(
p1 in Xx1 &
p2 in Yy2 &
h = [p1,p2] )
by A17, A18, ZFMISC_1:def 2;
consider Yy1 being
Subset of
XV such that A20:
(
Yy1 = Xx1 /\ ([#] XV) &
Xx1 is
open &
Yy2 is
open &
[:Yy1,Yy2:] in A )
by A18;
p1 in the
carrier of
XV
by A1, A16, A19, ZFMISC_1:106;
then
p1 in Xx1 /\ ([#] XV)
by A19, XBOOLE_0:def 4;
then
h in [:Yy1,Yy2:]
by A19, A20, ZFMISC_1:106;
hence
h in P
by A5, A20, TARSKI:def 4;
:: thesis: verum
end;
end; hence
ex
Q being
Subset of
[:X,Y:] st
(
Q in the
topology of
[:X,Y:] &
P = Q /\ ([#] [:XV,Y:]) )
by A10;
:: thesis: verum
end;
given Q being
Subset of
[:X,Y:] such that A21:
(
Q in the
topology of
[:X,Y:] &
P = Q /\ ([#] [:XV,Y:]) )
;
:: thesis: P in the topology of [:XV,Y:]
reconsider Q' =
Q as
Subset of
[:X,Y:] ;
Q' is
open
by A21, PRE_TOPC:def 5;
then consider A being
Subset-Family of
[:X,Y:] such that A22:
(
Q' = union A & ( for
e being
set st
e in A holds
ex
X1 being
Subset of
X ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open ) ) )
by BORSUK_1:45;
reconsider oS =
[#] [:XV,Y:] as
Subset of
[:X,Y:] by A1, A2, A3, ZFMISC_1:119;
reconsider A =
A as
Subset-Family of
[:X,Y:] ;
reconsider AA =
A | oS as
Subset-Family of
([:X,Y:] | oS) ;
reconsider AA =
AA as
Subset-Family of
[:XV,Y:] by PRE_TOPC:29;
reconsider AA =
AA as
Subset-Family of
[:XV,Y:] ;
union AA c= union A
by TOPS_2:44;
then A23:
union AA c= (union A) /\ oS
by XBOOLE_1:19;
(union A) /\ oS c= union AA
then A27:
P = union AA
by A21, A22, A23, XBOOLE_0:def 10;
for
e being
set st
e in AA holds
ex
X1 being
Subset of
XV ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
proof
let e be
set ;
:: thesis: ( e in AA implies ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open ) )
assume A28:
e in AA
;
:: thesis: ex X1 being Subset of XV ex Y1 being Subset of Y st
( e = [:X1,Y1:] & X1 is open & Y1 is open )
then reconsider e' =
e as
Subset of
([:X,Y:] | oS) ;
consider R being
Subset of
[:X,Y:] such that A29:
(
R in A &
R /\ oS = e' )
by A28, TOPS_2:def 3;
consider X1 being
Subset of
X,
Y1 being
Subset of
Y such that A30:
(
R = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A22, A29;
[#] [:XV,Y:] = [:([#] XV),([#] Y):]
by BORSUK_1:def 5;
then A31:
e' = [:(X1 /\ ([#] XV)),(Y1 /\ ([#] Y)):]
by A29, A30, ZFMISC_1:123;
reconsider D2 =
X1 /\ ([#] XV) as
Subset of
XV ;
X1 in the
topology of
X
by A30, PRE_TOPC:def 5;
then
D2 in the
topology of
XV
by PRE_TOPC:def 9;
then
D2 is
open
by PRE_TOPC:def 5;
hence
ex
X1 being
Subset of
XV ex
Y1 being
Subset of
Y st
(
e = [:X1,Y1:] &
X1 is
open &
Y1 is
open )
by A30, A31, TOPS_1:38;
:: thesis: verum
end;
then
P' is
open
by A27, BORSUK_1:45;
hence
P in the
topology of
[:XV,Y:]
by PRE_TOPC:def 5;
:: thesis: verum
end;
hence
[:XV,Y:] is SubSpace of [:X,Y:]
by A4, PRE_TOPC:def 9; :: thesis: verum