let X, Y be set ; for X1 being Subset of X
for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let X1 be Subset of X; for Y1 being Subset of Y st [:X1,Y1:] <> {} holds
( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
let Y1 be Subset of Y; ( [:X1,Y1:] <> {} implies ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 ) )
assume A1:
[:X1,Y1:] <> {}
; ( (pr1 (X,Y)) .: [:X1,Y1:] = X1 & (pr2 (X,Y)) .: [:X1,Y1:] = Y1 )
then A2:
X1 <> {}
;
A3:
Y1 <> {}
by A1;
A4:
X <> {}
by A2;
now for x being object holds
( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )set y = the
Element of
Y1;
let x be
object ;
( ( x in (pr1 (X,Y)) .: [:X1,Y1:] implies x in X1 ) & ( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] ) )thus
(
x in (pr1 (X,Y)) .: [:X1,Y1:] implies
x in X1 )
( x in X1 implies x in (pr1 (X,Y)) .: [:X1,Y1:] )proof
assume
x in (pr1 (X,Y)) .: [:X1,Y1:]
;
x in X1
then consider u being
object such that A5:
u in [:X,Y:]
and A6:
(
u in [:X1,Y1:] &
x = (pr1 (X,Y)) . u )
by FUNCT_2:64;
A7:
u `2 in Y
by A5, MCART_1:10;
(
u `1 in X1 &
x = (pr1 (X,Y)) . (
(u `1),
(u `2)) )
by A6, MCART_1:10, MCART_1:21;
hence
x in X1
by A7, FUNCT_3:def 4;
verum
end; assume A8:
x in X1
;
x in (pr1 (X,Y)) .: [:X1,Y1:]
the
Element of
Y1 in Y
by A3, TARSKI:def 3;
then A9:
x = (pr1 (X,Y)) . (
x, the
Element of
Y1)
by A8, FUNCT_3:def 4;
[x, the Element of Y1] in [:X1,Y1:]
by A3, A8, ZFMISC_1:87;
hence
x in (pr1 (X,Y)) .: [:X1,Y1:]
by A4, A9, FUNCT_2:35;
verum end;
hence
(pr1 (X,Y)) .: [:X1,Y1:] = X1
by TARSKI:2; (pr2 (X,Y)) .: [:X1,Y1:] = Y1
A10:
Y <> {}
by A3;
now for y being object holds
( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )set x = the
Element of
X1;
let y be
object ;
( ( y in (pr2 (X,Y)) .: [:X1,Y1:] implies y in Y1 ) & ( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] ) )thus
(
y in (pr2 (X,Y)) .: [:X1,Y1:] implies
y in Y1 )
( y in Y1 implies y in (pr2 (X,Y)) .: [:X1,Y1:] )proof
assume
y in (pr2 (X,Y)) .: [:X1,Y1:]
;
y in Y1
then consider u being
object such that A11:
u in [:X,Y:]
and A12:
(
u in [:X1,Y1:] &
y = (pr2 (X,Y)) . u )
by FUNCT_2:64;
A13:
u `1 in X
by A11, MCART_1:10;
(
u `2 in Y1 &
y = (pr2 (X,Y)) . (
(u `1),
(u `2)) )
by A12, MCART_1:10, MCART_1:21;
hence
y in Y1
by A13, FUNCT_3:def 5;
verum
end; assume A14:
y in Y1
;
y in (pr2 (X,Y)) .: [:X1,Y1:]
the
Element of
X1 in X
by A2, TARSKI:def 3;
then A15:
y = (pr2 (X,Y)) . ( the
Element of
X1,
y)
by A14, FUNCT_3:def 5;
[ the Element of X1,y] in [:X1,Y1:]
by A2, A14, ZFMISC_1:87;
hence
y in (pr2 (X,Y)) .: [:X1,Y1:]
by A10, A15, FUNCT_2:35;
verum end;
hence
(pr2 (X,Y)) .: [:X1,Y1:] = Y1
by TARSKI:2; verum