let X, Y be non empty TopSpace; :: thesis: for H being Subset-Family of [:X,Y:]
for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 ) )
let H be Subset-Family of [:X,Y:]; :: thesis: for X1 being Subset of X
for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 ) )
let X1 be Subset of X; :: thesis: for Y1 being Subset of Y st H is Cover of [:X1,Y1:] holds
( ( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 ) )
let Y1 be Subset of Y; :: thesis: ( H is Cover of [:X1,Y1:] implies ( ( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 ) ) )
A1:
the carrier of [:X,Y:] = [:the carrier of X,the carrier of Y:]
by Def5;
assume A2:
[:X1,Y1:] c= union H
; :: according to SETFAM_1:def 12 :: thesis: ( ( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 ) & ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 ) )
thus
( Y1 <> {} implies (Pr1 X,Y) .: H is Cover of X1 )
:: thesis: ( X1 <> {} implies (Pr2 X,Y) .: H is Cover of Y1 )proof
assume
Y1 <> {}
;
:: thesis: (Pr1 X,Y) .: H is Cover of X1
then consider y being
Point of
Y such that A3:
y in Y1
by SUBSET_1:10;
let e be
set ;
:: according to TARSKI:def 3,
SETFAM_1:def 12 :: thesis: ( not e in X1 or e in union ((Pr1 X,Y) .: H) )
assume A4:
e in X1
;
:: thesis: e in union ((Pr1 X,Y) .: H)
then reconsider x =
e as
Point of
X ;
[x,y] in [:X1,Y1:]
by A3, A4, ZFMISC_1:106;
then consider A being
set such that A5:
(
[x,y] in A &
A in H )
by A2, TARSKI:def 4;
A6:
dom (.: (pr1 the carrier of X,the carrier of Y)) =
bool (dom (pr1 the carrier of X,the carrier of Y))
by FUNCT_3:def 1
.=
bool [:the carrier of X,the carrier of Y:]
by FUNCT_3:def 5
;
(.: (pr1 the carrier of X,the carrier of Y)) . A = (pr1 the carrier of X,the carrier of Y) .: A
by A1, A5, Th9;
then A7:
(pr1 the carrier of X,the carrier of Y) .: A in (Pr1 X,Y) .: H
by A1, A5, A6, FUNCT_1:def 12;
[x,y] in [:the carrier of X,the carrier of Y:]
by ZFMISC_1:106;
then A8:
[x,y] in dom (pr1 the carrier of X,the carrier of Y)
by FUNCT_3:def 5;
e = (pr1 the carrier of X,the carrier of Y) . x,
y
by FUNCT_3:def 5;
then
e in (pr1 the carrier of X,the carrier of Y) .: A
by A5, A8, FUNCT_1:def 12;
hence
e in union ((Pr1 X,Y) .: H)
by A7, TARSKI:def 4;
:: thesis: verum
end;
assume
X1 <> {}
; :: thesis: (Pr2 X,Y) .: H is Cover of Y1
then consider x being Point of X such that
A9:
x in X1
by SUBSET_1:10;
let e be set ; :: according to TARSKI:def 3,SETFAM_1:def 12 :: thesis: ( not e in Y1 or e in union ((Pr2 X,Y) .: H) )
assume A10:
e in Y1
; :: thesis: e in union ((Pr2 X,Y) .: H)
then reconsider y = e as Point of Y ;
[x,y] in [:X1,Y1:]
by A9, A10, ZFMISC_1:106;
then consider A being set such that
A11:
( [x,y] in A & A in H )
by A2, TARSKI:def 4;
A12: dom (.: (pr2 the carrier of X,the carrier of Y)) =
bool (dom (pr2 the carrier of X,the carrier of Y))
by FUNCT_3:def 1
.=
bool [:the carrier of X,the carrier of Y:]
by FUNCT_3:def 6
;
(.: (pr2 the carrier of X,the carrier of Y)) . A = (pr2 the carrier of X,the carrier of Y) .: A
by A1, A11, Th10;
then A13:
(pr2 the carrier of X,the carrier of Y) .: A in (Pr2 X,Y) .: H
by A1, A11, A12, FUNCT_1:def 12;
[x,y] in [:the carrier of X,the carrier of Y:]
by ZFMISC_1:106;
then A14:
[x,y] in dom (pr2 the carrier of X,the carrier of Y)
by FUNCT_3:def 6;
e = (pr2 the carrier of X,the carrier of Y) . x,y
by FUNCT_3:def 6;
then
e in (pr2 the carrier of X,the carrier of Y) .: A
by A11, A14, FUNCT_1:def 12;
hence
e in union ((Pr2 X,Y) .: H)
by A13, TARSKI:def 4; :: thesis: verum