let S, T be antisymmetric with_suprema RelStr ; 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:]; ( 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 TARSKI:def 3,
XBOOLE_0:def 10 proj2 (X "\/" Y) = (proj2 X) "\/" (proj2 Y)
hereby for a being object st a in (proj1 X) "\/" (proj1 Y) holds
a in proj1 (X "\/" Y)
let a be
object ;
( a in proj1 (X "\/" Y) implies a in (proj1 X) "\/" (proj1 Y) )assume
a in proj1 (X "\/" Y)
;
a in (proj1 X) "\/" (proj1 Y)then consider b being
object such that A4:
[a,b] in X "\/" Y
by XTUPLE_0:def 12;
consider x,
y being
Element of
[:S,T:] such that A5:
[a,b] = x "\/" y
and A6:
x in X
and A7:
y in Y
by A2, A4;
x = [(x `1),(x `2)]
by A1, MCART_1:21;
then A8:
x `1 in proj1 X
by A6, XTUPLE_0:def 12;
y = [(y `1),(y `2)]
by A1, MCART_1:21;
then A9:
y `1 in proj1 Y
by A7, XTUPLE_0:def 12;
a =
[a,b] `1
.=
(x `1) "\/" (y `1)
by A5, Th14
;
hence
a in (proj1 X) "\/" (proj1 Y)
by A8, A9, YELLOW_4:10;
verum
end; let a be
object ;
( a in (proj1 X) "\/" (proj1 Y) implies a in proj1 (X "\/" Y) )assume
a in (proj1 X) "\/" (proj1 Y)
;
a in proj1 (X "\/" Y)then consider x,
y being
Element of
S such that A10:
a = x "\/" y
and A11:
x in proj1 X
and A12:
y in proj1 Y
by A3;
consider x2 being
object such that A13:
[x,x2] in X
by A11, XTUPLE_0:def 12;
consider y2 being
object such that A14:
[y,y2] in Y
by A12, XTUPLE_0:def 12;
reconsider x2 =
x2,
y2 =
y2 as
Element of
T by A1, A13, A14, ZFMISC_1:87;
[x,x2] "\/" [y,y2] = [a,(x2 "\/" y2)]
by A10, Th16;
then
[a,(x2 "\/" y2)] in X "\/" Y
by A13, A14, YELLOW_4:10;
hence
a in proj1 (X "\/" Y)
by XTUPLE_0:def 12;
verum
hereby TARSKI:def 3,
XBOOLE_0:def 10 (proj2 X) "\/" (proj2 Y) c= proj2 (X "\/" Y)
let b be
object ;
( b in proj2 (X "\/" Y) implies b in (proj2 X) "\/" (proj2 Y) )assume
b in proj2 (X "\/" Y)
;
b in (proj2 X) "\/" (proj2 Y)then consider a being
object such that A15:
[a,b] in X "\/" Y
by XTUPLE_0:def 13;
consider x,
y being
Element of
[:S,T:] such that A16:
[a,b] = x "\/" y
and A17:
x in X
and A18:
y in Y
by A2, A15;
x = [(x `1),(x `2)]
by A1, MCART_1:21;
then A19:
x `2 in proj2 X
by A17, XTUPLE_0:def 13;
y = [(y `1),(y `2)]
by A1, MCART_1:21;
then A20:
y `2 in proj2 Y
by A18, XTUPLE_0:def 13;
b =
[a,b] `2
.=
(x `2) "\/" (y `2)
by A16, Th14
;
hence
b in (proj2 X) "\/" (proj2 Y)
by A19, A20, YELLOW_4:10;
verum
end;
let b be object ; TARSKI:def 3 ( not b in (proj2 X) "\/" (proj2 Y) or b in proj2 (X "\/" Y) )
A21:
(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;
assume
b in (proj2 X) "\/" (proj2 Y)
; b in proj2 (X "\/" Y)
then consider x, y being Element of T such that
A22:
b = x "\/" y
and
A23:
x in proj2 X
and
A24:
y in proj2 Y
by A21;
consider x1 being object such that
A25:
[x1,x] in X
by A23, XTUPLE_0:def 13;
consider y1 being object such that
A26:
[y1,y] in Y
by A24, XTUPLE_0:def 13;
reconsider x1 = x1, y1 = y1 as Element of S by A1, A25, A26, ZFMISC_1:87;
[x1,x] "\/" [y1,y] = [(x1 "\/" y1),b]
by A22, Th16;
then
[(x1 "\/" y1),b] in X "\/" Y
by A25, A26, YELLOW_4:10;
hence
b in proj2 (X "\/" Y)
by XTUPLE_0:def 13; verum