let S, T be antisymmetric with_suprema RelStr ; :: thesis: for X, Y being Subset of [:S,T:] holds
( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )
let X, Y be Subset of [:S,T:]; :: thesis: ( proj1 (X "\/" Y) = (proj1 X) "\/" (proj1 Y) & proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y) )
A1:
the carrier of [:S,T:] = [:the carrier of S,the carrier of T:]
by YELLOW_3:def 2;
A2:
X "\/" Y = { (x "\/" y) where x, y is Element of [:S,T:] : ( x in X & y in Y ) }
by YELLOW_4:def 3;
A3:
(proj1 X) "\/" (proj1 Y) = { (x "\/" y) where x, y is Element of S : ( x in proj1 X & y in proj1 Y ) }
by YELLOW_4:def 3;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y)
hereby :: thesis: for a being set st a in (proj1 X) "\/" (proj1 Y) holds
a in proj1 (X "\/" Y)
let a be
set ;
:: thesis: ( a in proj1 (X "\/" Y) implies a in (proj1 X) "\/" (proj1 Y) )assume
a in proj1 (X "\/" Y)
;
:: thesis: a in (proj1 X) "\/" (proj1 Y)then consider b being
set such that A4:
[a,b] in X "\/" Y
by RELAT_1:def 4;
consider x,
y being
Element of
[:S,T:] such that A5:
[a,b] = x "\/" y
and A6:
(
x in X &
y in Y )
by A2, A4;
A7:
a =
[a,b] `1
by MCART_1:7
.=
(x `1 ) "\/" (y `1 )
by A5, Th14
;
(
x = [(x `1 ),(x `2 )] &
y = [(y `1 ),(y `2 )] )
by A1, MCART_1:23;
then
(
x `1 in proj1 X &
y `1 in proj1 Y )
by A6, FUNCT_5:4;
hence
a in (proj1 X) "\/" (proj1 Y)
by A7, YELLOW_4:10;
:: thesis: verum
end; let a be
set ;
:: thesis: ( a in (proj1 X) "\/" (proj1 Y) implies a in proj1 (X "\/" Y) )assume
a in (proj1 X) "\/" (proj1 Y)
;
:: thesis: a in proj1 (X "\/" Y)then consider x,
y being
Element of
S such that A8:
(
a = x "\/" y &
x in proj1 X &
y in proj1 Y )
by A3;
consider x2 being
set such that A9:
[x,x2] in X
by A8, RELAT_1:def 4;
consider y2 being
set such that A10:
[y,y2] in Y
by A8, RELAT_1:def 4;
reconsider x2 =
x2,
y2 =
y2 as
Element of
T by A1, A9, A10, ZFMISC_1:106;
[x,x2] "\/" [y,y2] = [a,(x2 "\/" y2)]
by A8, Th16;
then
[a,(x2 "\/" y2)] in X "\/" Y
by A9, A10, YELLOW_4:10;
hence
a in proj1 (X "\/" Y)
by RELAT_1:def 4;
:: thesis: verum
A11:
(proj2 X) "\/" (proj2 Y) = { (x "\/" y) where x, y is Element of T : ( x in proj2 X & y in proj2 Y ) }
by YELLOW_4:def 3;
hereby :: according to TARSKI:def 3,
XBOOLE_0:def 10 :: thesis: (proj2 X) "\/" (proj2 Y) c= proj2 (X "\/" Y)
let b be
set ;
:: thesis: ( b in proj2 (X "\/" Y) implies b in (proj2 X) "\/" (proj2 Y) )assume
b in proj2 (X "\/" Y)
;
:: thesis: b in (proj2 X) "\/" (proj2 Y)then consider a being
set such that A12:
[a,b] in X "\/" Y
by RELAT_1:def 5;
consider x,
y being
Element of
[:S,T:] such that A13:
[a,b] = x "\/" y
and A14:
(
x in X &
y in Y )
by A2, A12;
A15:
b =
[a,b] `2
by MCART_1:7
.=
(x `2 ) "\/" (y `2 )
by A13, Th14
;
(
x = [(x `1 ),(x `2 )] &
y = [(y `1 ),(y `2 )] )
by A1, MCART_1:23;
then
(
x `2 in proj2 X &
y `2 in proj2 Y )
by A14, FUNCT_5:4;
hence
b in (proj2 X) "\/" (proj2 Y)
by A15, YELLOW_4:10;
:: thesis: verum
end;
let b be set ; :: according to TARSKI:def 3 :: thesis: ( not b in (proj2 X) "\/" (proj2 Y) or b in proj2 (X "\/" Y) )
assume
b in (proj2 X) "\/" (proj2 Y)
; :: thesis: b in proj2 (X "\/" Y)
then consider x, y being Element of T such that
A16:
( b = x "\/" y & x in proj2 X & y in proj2 Y )
by A11;
consider x1 being set such that
A17:
[x1,x] in X
by A16, RELAT_1:def 5;
consider y1 being set such that
A18:
[y1,y] in Y
by A16, RELAT_1:def 5;
reconsider x1 = x1, y1 = y1 as Element of S by A1, A17, A18, ZFMISC_1:106;
[x1,x] "\/" [y1,y] = [(x1 "\/" y1),b]
by A16, Th16;
then
[(x1 "\/" y1),b] in X "\/" Y
by A17, A18, YELLOW_4:10;
hence
b in proj2 (X "\/" Y)
by RELAT_1:def 5; :: thesis: verum