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