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 5
;
A2:
the carrier of [:X,Y:] = [: the carrier of X, the carrier of Y:]
by Def2;
assume A3:
[:X1,Y1:] c= union H
; SETFAM_1:def 11 ( ( 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:4;
let e be
object ;
TARSKI:def 3,
SETFAM_1:def 11 ( 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:87;
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:87;
then A8:
[x,y] in dom (pr1 ( the carrier of X, the carrier of Y))
by FUNCT_3:def 4;
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 4
;
e = (pr1 ( the carrier of X, the carrier of Y)) . (
x,
y)
by FUNCT_3:def 4;
then A10:
e in (pr1 ( the carrier of X, the carrier of Y)) .: A
by A6, A8, FUNCT_1:def 6;
(.: (pr1 ( the carrier of X, the carrier of Y))) . A = (pr1 ( the carrier of X, the carrier of Y)) .: A
by A2, A7, EQREL_1:47;
then
(pr1 ( the carrier of X, the carrier of Y)) .: A in (Pr1 (X,Y)) .: H
by A2, A7, A9, FUNCT_1:def 6;
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:4;
let e be object ; TARSKI:def 3,SETFAM_1:def 11 ( 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:87;
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:87;
then A15:
[x,y] in dom (pr2 ( the carrier of X, the carrier of Y))
by FUNCT_3:def 5;
e = (pr2 ( the carrier of X, the carrier of Y)) . (x,y)
by FUNCT_3:def 5;
then A16:
e in (pr2 ( the carrier of X, the carrier of Y)) .: A
by A13, A15, FUNCT_1:def 6;
(.: (pr2 ( the carrier of X, the carrier of Y))) . A = (pr2 ( the carrier of X, the carrier of Y)) .: A
by A2, A14, EQREL_1:48;
then
(pr2 ( the carrier of X, the carrier of Y)) .: A in (Pr2 (X,Y)) .: H
by A2, A14, A1, FUNCT_1:def 6;
hence
e in union ((Pr2 (X,Y)) .: H)
by A16, TARSKI:def 4; verum