:: XTUPLE_0 semantic presentation
begin
definition
let x be set ;
attrx is pair means :Dfx: :: XTUPLE_0:def 1
ex x1, x2 being set st x = [x1,x2];
end;
:: deftheorem Dfx defines pair XTUPLE_0:def_1_:_
for x being set holds
( x is pair iff ex x1, x2 being set st x = [x1,x2] );
registration
let x1, x2 be set ;
cluster[x1,x2] -> pair ;
coherence
[x1,x2] is pair by Dfx;
end;
Lx4: for x, y1, y2 being set st {x} = {y1,y2} holds
x = y1
proof
let x, y1, y2 be set ; ::_thesis: ( {x} = {y1,y2} implies x = y1 )
assume {x} = {y1,y2} ; ::_thesis: x = y1
then y1 in {x} by TARSKI:def_2;
hence x = y1 by TARSKI:def_1; ::_thesis: verum
end;
Lx5: for x, y1, y2 being set st {x} = {y1,y2} holds
y1 = y2
proof
let x, y1, y2 be set ; ::_thesis: ( {x} = {y1,y2} implies y1 = y2 )
assume A1: {x} = {y1,y2} ; ::_thesis: y1 = y2
then x = y1 by Lx4;
hence y1 = y2 by A1, Lx4; ::_thesis: verum
end;
Lx6: for x1, x2, y1, y2 being set holds
( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 )
x1 in {x1,x2} by TARSKI:def_2;
hence ( not {x1,x2} = {y1,y2} or x1 = y1 or x1 = y2 ) by TARSKI:def_2; ::_thesis: verum
end;
theorem Th1: :: XTUPLE_0:1
for x1, x2, y1, y2 being set st [x1,x2] = [y1,y2] holds
( x1 = y1 & x2 = y2 )
proof
let x1, x2, y1, y2 be set ; ::_thesis: ( [x1,x2] = [y1,y2] implies ( x1 = y1 & x2 = y2 ) )
assume A1: [x1,x2] = [y1,y2] ; ::_thesis: ( x1 = y1 & x2 = y2 )
percases ( y1 <> y2 or y1 = y2 ) ;
supposeA3: y1 <> y2 ; ::_thesis: ( x1 = y1 & x2 = y2 )
then A4: {x1} <> {y1,y2} by Lx5;
then {x1} = {y1} by A1, Lx6;
then x1 in {y1} by TARSKI:def_1;
hence A5: x1 = y1 by TARSKI:def_1; ::_thesis: x2 = y2
{y1,y2} = {x1,x2} by A1, A4, Lx6;
hence x2 = y2 by A3, A5, Lx6; ::_thesis: verum
end;
supposeA6: y1 = y2 ; ::_thesis: ( x1 = y1 & x2 = y2 )
then {{x1,x2},{x1}} = {{y1},{y1}} by A1, ENUMSET1:29
.= {{y1}} by ENUMSET1:29 ;
then {y1} = {x1,x2} by Lx4;
hence ( x1 = y1 & x2 = y2 ) by A6, Lx4; ::_thesis: verum
end;
end;
end;
definition
let x be set ;
assume x is pair ;
then consider x1, x2 being set such that
A1: x = [x1,x2] by Dfx;
funcx `1 -> set means :Def1: :: XTUPLE_0:def 2
for y1, y2 being set st x = [y1,y2] holds
it = y1;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y1
proof
take x1 ; ::_thesis: for y1, y2 being set st x = [y1,y2] holds
x1 = y1
thus for y1, y2 being set st x = [y1,y2] holds
x1 = y1 by A1, Th1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y1 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y1 ) holds
b1 = b2
proof
let z1, z2 be set ; ::_thesis: ( ( for y1, y2 being set st x = [y1,y2] holds
z1 = y1 ) & ( for y1, y2 being set st x = [y1,y2] holds
z2 = y1 ) implies z1 = z2 )
assume that
A2: for y1, y2 being set st x = [y1,y2] holds
z1 = y1 and
A3: for y1, y2 being set st x = [y1,y2] holds
z2 = y1 ; ::_thesis: z1 = z2
thus z1 = x1 by A1, A2
.= z2 by A1, A3 ; ::_thesis: verum
end;
funcx `2 -> set means :Def2: :: XTUPLE_0:def 3
for y1, y2 being set st x = [y1,y2] holds
it = y2;
existence
ex b1 being set st
for y1, y2 being set st x = [y1,y2] holds
b1 = y2
proof
take x2 ; ::_thesis: for y1, y2 being set st x = [y1,y2] holds
x2 = y2
thus for y1, y2 being set st x = [y1,y2] holds
x2 = y2 by A1, Th1; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for y1, y2 being set st x = [y1,y2] holds
b1 = y2 ) & ( for y1, y2 being set st x = [y1,y2] holds
b2 = y2 ) holds
b1 = b2
proof
let z1, z2 be set ; ::_thesis: ( ( for y1, y2 being set st x = [y1,y2] holds
z1 = y2 ) & ( for y1, y2 being set st x = [y1,y2] holds
z2 = y2 ) implies z1 = z2 )
assume that
A4: for y1, y2 being set st x = [y1,y2] holds
z1 = y2 and
A5: for y1, y2 being set st x = [y1,y2] holds
z2 = y2 ; ::_thesis: z1 = z2
thus z1 = x2 by A1, A4
.= z2 by A1, A5 ; ::_thesis: verum
end;
end;
:: deftheorem Def1 defines `1 XTUPLE_0:def_2_:_
for x being set st x is pair holds
for b2 being set holds
( b2 = x `1 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y1 );
:: deftheorem Def2 defines `2 XTUPLE_0:def_3_:_
for x being set st x is pair holds
for b2 being set holds
( b2 = x `2 iff for y1, y2 being set st x = [y1,y2] holds
b2 = y2 );
registration
let x1, x2 be set ;
reduce[x1,x2] `1 to x1;
reducibility
[x1,x2] `1 = x1 by Def1;
reduce[x1,x2] `2 to x2;
reducibility
[x1,x2] `2 = x2 by Def2;
end;
registration
cluster pair for set ;
existence
ex b1 being set st b1 is pair
proof
take [ the set , the set ] ; ::_thesis: [ the set , the set ] is pair
take the set ; :: according to XTUPLE_0:def_1 ::_thesis: ex x2 being set st [ the set , the set ] = [ the set ,x2]
take the set ; ::_thesis: [ the set , the set ] = [ the set , the set ]
thus [ the set , the set ] = [ the set , the set ] ; ::_thesis: verum
end;
end;
registration
let x be pair set ;
reduce[(x `1),(x `2)] to x;
reducibility
[(x `1),(x `2)] = x
proof
consider x1, x2 being set such that
W: x = [x1,x2] by Dfx;
thus [(x `1),(x `2)] = [x1,(x `2)] by W, Def1
.= x by W, Def2 ; ::_thesis: verum
end;
end;
theorem :: XTUPLE_0:2
for a, b being pair set st a `1 = b `1 & a `2 = b `2 holds
a = b
proof
let a, b be pair set ; ::_thesis: ( a `1 = b `1 & a `2 = b `2 implies a = b )
assume Z: ( a `1 = b `1 & a `2 = b `2 ) ; ::_thesis: a = b
( a = [(a `1),(a `2)] & b = [(b `1),(b `2)] ) ;
hence a = b by Z; ::_thesis: verum
end;
begin
definition
let x1, x2, x3 be set ;
func[x1,x2,x3] -> set equals :: XTUPLE_0:def 4
[[x1,x2],x3];
coherence
[[x1,x2],x3] is set ;
end;
:: deftheorem defines [ XTUPLE_0:def_4_:_
for x1, x2, x3 being set holds [x1,x2,x3] = [[x1,x2],x3];
definition
let x be set ;
attrx is triple means :Dfy: :: XTUPLE_0:def 5
ex x1, x2, x3 being set st x = [x1,x2,x3];
end;
:: deftheorem Dfy defines triple XTUPLE_0:def_5_:_
for x being set holds
( x is triple iff ex x1, x2, x3 being set st x = [x1,x2,x3] );
registration
let x1, x2, x3 be set ;
cluster[x1,x2,x3] -> triple ;
coherence
[x1,x2,x3] is triple by Dfy;
end;
theorem Th3: :: XTUPLE_0:3
for x1, x2, x3, y1, y2, y3 being set st [x1,x2,x3] = [y1,y2,y3] holds
( x1 = y1 & x2 = y2 & x3 = y3 )
proof
let x1, x2, x3, y1, y2, y3 be set ; ::_thesis: ( [x1,x2,x3] = [y1,y2,y3] implies ( x1 = y1 & x2 = y2 & x3 = y3 ) )
assume A1: [x1,x2,x3] = [y1,y2,y3] ; ::_thesis: ( x1 = y1 & x2 = y2 & x3 = y3 )
then [x1,x2] = [y1,y2] by Th1;
hence ( x1 = y1 & x2 = y2 & x3 = y3 ) by A1, Th1; ::_thesis: verum
end;
registration
cluster triple for set ;
existence
ex b1 being set st b1 is triple
proof
take [ the set , the set , the set ] ; ::_thesis: [ the set , the set , the set ] is triple
take the set ; :: according to XTUPLE_0:def_5 ::_thesis: ex x2, x3 being set st [ the set , the set , the set ] = [ the set ,x2,x3]
take the set ; ::_thesis: ex x3 being set st [ the set , the set , the set ] = [ the set , the set ,x3]
take the set ; ::_thesis: [ the set , the set , the set ] = [ the set , the set , the set ]
thus [ the set , the set , the set ] = [ the set , the set , the set ] ; ::_thesis: verum
end;
cluster triple -> pair for set ;
coherence
for b1 being set st b1 is triple holds
b1 is pair
proof
let x be set ; ::_thesis: ( x is triple implies x is pair )
assume ex x1, x2, x3 being set st x = [x1,x2,x3] ; :: according to XTUPLE_0:def_5 ::_thesis: x is pair
hence x is pair ; ::_thesis: verum
end;
end;
definition
let x be set ;
funcx `1_3 -> set equals :: XTUPLE_0:def 6
(x `1) `1 ;
coherence
(x `1) `1 is set ;
funcx `2_3 -> set equals :: XTUPLE_0:def 7
(x `1) `2 ;
coherence
(x `1) `2 is set ;
end;
:: deftheorem defines `1_3 XTUPLE_0:def_6_:_
for x being set holds x `1_3 = (x `1) `1 ;
:: deftheorem defines `2_3 XTUPLE_0:def_7_:_
for x being set holds x `2_3 = (x `1) `2 ;
notation
let x be set ;
synonym x `3_3 for x `2 ;
end;
registration
let x1, x2, x3 be set ;
reduce[x1,x2,x3] `1_3 to x1;
reducibility
[x1,x2,x3] `1_3 = x1
proof
thus [x1,x2,x3] `1_3 = ([[x1,x2],x3] `1) `1
.= x1 ; ::_thesis: verum
end;
reduce[x1,x2,x3] `2_3 to x2;
reducibility
[x1,x2,x3] `2_3 = x2
proof
thus [x1,x2,x3] `2_3 = ([[x1,x2],x3] `1) `2
.= x2 ; ::_thesis: verum
end;
reduce[x1,x2,x3] `3_3 to x3;
reducibility
[x1,x2,x3] `3_3 = x3
proof
thus [x1,x2,x3] `3_3 = [[x1,x2],x3] `2
.= x3 ; ::_thesis: verum
end;
end;
registration
let x be triple set ;
reduce[(x `1_3),(x `2_3),(x `3_3)] to x;
reducibility
[(x `1_3),(x `2_3),(x `3_3)] = x
proof
consider x1, x2, x3 being set such that
W: x = [x1,x2,x3] by Dfy;
( [x1,x2,x3] `1_3 = x1 & [x1,x2,x3] `2_3 = x2 & [x1,x2,x3] `3_3 = x3 ) ;
hence [(x `1_3),(x `2_3),(x `3_3)] = x by W; ::_thesis: verum
end;
end;
theorem :: XTUPLE_0:4
for a, b being triple set st a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 holds
a = b
proof
let a, b be triple set ; ::_thesis: ( a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 implies a = b )
assume Z: ( a `1_3 = b `1_3 & a `2_3 = b `2_3 & a `3_3 = b `3_3 ) ; ::_thesis: a = b
( a = [(a `1_3),(a `2_3),(a `3_3)] & b = [(b `1_3),(b `2_3),(b `3_3)] ) ;
hence a = b by Z; ::_thesis: verum
end;
begin
definition
let x1, x2, x3, x4 be set ;
func[x1,x2,x3,x4] -> set equals :: XTUPLE_0:def 8
[[x1,x2,x3],x4];
coherence
[[x1,x2,x3],x4] is set ;
end;
:: deftheorem defines [ XTUPLE_0:def_8_:_
for x1, x2, x3, x4 being set holds [x1,x2,x3,x4] = [[x1,x2,x3],x4];
definition
let x be set ;
attrx is quadruple means :Dfz: :: XTUPLE_0:def 9
ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4];
end;
:: deftheorem Dfz defines quadruple XTUPLE_0:def_9_:_
for x being set holds
( x is quadruple iff ex x1, x2, x3, x4 being set st x = [x1,x2,x3,x4] );
registration
let x1, x2, x3, x4 be set ;
cluster[x1,x2,x3,x4] -> quadruple ;
coherence
[x1,x2,x3,x4] is quadruple by Dfz;
end;
theorem :: XTUPLE_0:5
for x1, x2, x3, x4, y1, y2, y3, y4 being set st [x1,x2,x3,x4] = [y1,y2,y3,y4] holds
( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
proof
let x1, x2, x3, x4, y1, y2, y3, y4 be set ; ::_thesis: ( [x1,x2,x3,x4] = [y1,y2,y3,y4] implies ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) )
assume A1: [x1,x2,x3,x4] = [y1,y2,y3,y4] ; ::_thesis: ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 )
then [x1,x2,x3] = [y1,y2,y3] by Th1;
hence ( x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 ) by A1, Th3, Th1; ::_thesis: verum
end;
registration
cluster quadruple for set ;
existence
ex b1 being set st b1 is quadruple
proof
take [ the set , the set , the set , the set ] ; ::_thesis: [ the set , the set , the set , the set ] is quadruple
take the set ; :: according to XTUPLE_0:def_9 ::_thesis: ex x2, x3, x4 being set st [ the set , the set , the set , the set ] = [ the set ,x2,x3,x4]
take the set ; ::_thesis: ex x3, x4 being set st [ the set , the set , the set , the set ] = [ the set , the set ,x3,x4]
take the set ; ::_thesis: ex x4 being set st [ the set , the set , the set , the set ] = [ the set , the set , the set ,x4]
take the set ; ::_thesis: [ the set , the set , the set , the set ] = [ the set , the set , the set , the set ]
thus [ the set , the set , the set , the set ] = [ the set , the set , the set , the set ] ; ::_thesis: verum
end;
cluster quadruple -> triple for set ;
coherence
for b1 being set st b1 is quadruple holds
b1 is triple
proof
let x be set ; ::_thesis: ( x is quadruple implies x is triple )
given x1, x2, x3, x4 being set such that G: x = [x1,x2,x3,x4] ; :: according to XTUPLE_0:def_9 ::_thesis: x is triple
x = [[x1,x2],x3,x4] by G;
hence x is triple ; ::_thesis: verum
end;
end;
definition
let x be set ;
funcx `1_4 -> set equals :: XTUPLE_0:def 10
((x `1) `1) `1 ;
coherence
((x `1) `1) `1 is set ;
funcx `2_4 -> set equals :: XTUPLE_0:def 11
((x `1) `1) `2 ;
coherence
((x `1) `1) `2 is set ;
end;
:: deftheorem defines `1_4 XTUPLE_0:def_10_:_
for x being set holds x `1_4 = ((x `1) `1) `1 ;
:: deftheorem defines `2_4 XTUPLE_0:def_11_:_
for x being set holds x `2_4 = ((x `1) `1) `2 ;
notation
let x be set ;
synonym x `3_4 for x `2_3 ;
synonym x `4_4 for x `2 ;
end;
registration
let x1, x2, x3, x4 be set ;
reduce[x1,x2,x3,x4] `1_4 to x1;
reducibility
[x1,x2,x3,x4] `1_4 = x1
proof
thus [x1,x2,x3,x4] `1_4 = (([[x1,x2,x3],x4] `1) `1) `1
.= [x1,x2,x3] `1_3
.= x1 ; ::_thesis: verum
end;
reduce[x1,x2,x3,x4] `2_4 to x2;
reducibility
[x1,x2,x3,x4] `2_4 = x2
proof
thus [x1,x2,x3,x4] `2_4 = (([[x1,x2,x3],x4] `1) `1) `2
.= [x1,x2,x3] `2_3
.= x2 ; ::_thesis: verum
end;
reduce[x1,x2,x3,x4] `3_4 to x3;
reducibility
[x1,x2,x3,x4] `3_4 = x3
proof
thus [x1,x2,x3,x4] `3_4 = ([[x1,x2,x3],x4] `1) `2
.= x3 ; ::_thesis: verum
end;
reduce[x1,x2,x3,x4] `4_4 to x4;
reducibility
[x1,x2,x3,x4] `4_4 = x4
proof
thus [x1,x2,x3,x4] `4_4 = [[x1,x2,x3],x4] `2
.= x4 ; ::_thesis: verum
end;
end;
registration
let x be quadruple set ;
reduce[(x `1_4),(x `2_4),(x `3_4),(x `4_4)] to x;
reducibility
[(x `1_4),(x `2_4),(x `3_4),(x `4_4)] = x
proof
consider x1, x2, x3, x4 being set such that
W: x = [x1,x2,x3,x4] by Dfz;
( [x1,x2,x3,x4] `1_4 = x1 & [x1,x2,x3,x4] `2_4 = x2 & [x1,x2,x3,x4] `3_4 = x3 & [x1,x2,x3,x4] `4_4 = x4 ) ;
hence [(x `1_4),(x `2_4),(x `3_4),(x `4_4)] = x by W; ::_thesis: verum
end;
end;
theorem Pre1: :: XTUPLE_0:6
for x, y, X being set st [x,y] in X holds
x in union (union X)
proof
let x, y, X be set ; ::_thesis: ( [x,y] in X implies x in union (union X) )
assume A1: [x,y] in X ; ::_thesis: x in union (union X)
{x} in [x,y] by TARSKI:def_2;
then A2: {x} in union X by A1, TARSKI:def_4;
x in {x} by TARSKI:def_1;
hence x in union (union X) by A2, TARSKI:def_4; ::_thesis: verum
end;
theorem Pre2: :: XTUPLE_0:7
for x, y, X being set st [x,y] in X holds
y in union (union X)
proof
let x, y, X be set ; ::_thesis: ( [x,y] in X implies y in union (union X) )
assume A1: [x,y] in X ; ::_thesis: y in union (union X)
{x,y} in [x,y] by TARSKI:def_2;
then A2: {x,y} in union X by A1, TARSKI:def_4;
y in {x,y} by TARSKI:def_2;
hence y in union (union X) by A2, TARSKI:def_4; ::_thesis: verum
end;
definition
let X be set ;
func proj1 X -> set means :Def4: :: XTUPLE_0:def 12
for x being set holds
( x in it iff ex y being set st [x,y] in X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [x,y] in X )
proof
defpred S1[ set ] means ex y being set st [$1,y] in X;
consider Y being set such that
A0: for x being set holds
( x in Y iff ( x in union (union X) & S1[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: for x being set holds
( x in Y iff ex y being set st [x,y] in X )
let x be set ; ::_thesis: ( x in Y iff ex y being set st [x,y] in X )
thus ( x in Y implies ex y being set st [x,y] in X ) by A0; ::_thesis: ( ex y being set st [x,y] in X implies x in Y )
given y being set such that A1: [x,y] in X ; ::_thesis: x in Y
x in union (union X) by A1, Pre1;
hence x in Y by A1, A0; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [x,y] in X ) ) & ( for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) ) holds
b1 = b2
proof
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff ex y being set st [x,y] in X ) ) & ( for x being set holds
( x in X2 iff ex y being set st [x,y] in X ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ex y being set st [x,y] in X ) and
A3: for x being set holds
( x in X2 iff ex y being set st [x,y] in X ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_set_holds_
(_x_in_X1_iff_x_in_X2_)
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
( x in X1 iff ex y being set st [x,y] in X ) by A2;
hence ( x in X1 iff x in X2 ) by A3; ::_thesis: verum
end;
hence X1 = X2 by TARSKI:1; ::_thesis: verum
end;
func proj2 X -> set means :Def5: :: XTUPLE_0:def 13
for x being set holds
( x in it iff ex y being set st [y,x] in X );
existence
ex b1 being set st
for x being set holds
( x in b1 iff ex y being set st [y,x] in X )
proof
defpred S1[ set ] means ex y being set st [y,$1] in X;
consider Y being set such that
A0: for x being set holds
( x in Y iff ( x in union (union X) & S1[x] ) ) from XBOOLE_0:sch_1();
take Y ; ::_thesis: for x being set holds
( x in Y iff ex y being set st [y,x] in X )
let x be set ; ::_thesis: ( x in Y iff ex y being set st [y,x] in X )
thus ( x in Y implies ex y being set st [y,x] in X ) by A0; ::_thesis: ( ex y being set st [y,x] in X implies x in Y )
given y being set such that A1: [y,x] in X ; ::_thesis: x in Y
x in union (union X) by A1, Pre2;
hence x in Y by A1, A0; ::_thesis: verum
end;
uniqueness
for b1, b2 being set st ( for x being set holds
( x in b1 iff ex y being set st [y,x] in X ) ) & ( for x being set holds
( x in b2 iff ex y being set st [y,x] in X ) ) holds
b1 = b2
proof
let X1, X2 be set ; ::_thesis: ( ( for x being set holds
( x in X1 iff ex y being set st [y,x] in X ) ) & ( for x being set holds
( x in X2 iff ex y being set st [y,x] in X ) ) implies X1 = X2 )
assume that
A2: for x being set holds
( x in X1 iff ex y being set st [y,x] in X ) and
A3: for x being set holds
( x in X2 iff ex y being set st [y,x] in X ) ; ::_thesis: X1 = X2
now__::_thesis:_for_x_being_set_holds_
(_x_in_X1_iff_x_in_X2_)
let x be set ; ::_thesis: ( x in X1 iff x in X2 )
( x in X1 iff ex y being set st [y,x] in X ) by A2;
hence ( x in X1 iff x in X2 ) by A3; ::_thesis: verum
end;
hence X1 = X2 by TARSKI:1; ::_thesis: verum
end;
end;
:: deftheorem Def4 defines proj1 XTUPLE_0:def_12_:_
for X, b2 being set holds
( b2 = proj1 X iff for x being set holds
( x in b2 iff ex y being set st [x,y] in X ) );
:: deftheorem Def5 defines proj2 XTUPLE_0:def_13_:_
for X, b2 being set holds
( b2 = proj2 X iff for x being set holds
( x in b2 iff ex y being set st [y,x] in X ) );
theorem Th10: :: XTUPLE_0:8
for X, Y being set st X c= Y holds
proj1 X c= proj1 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj1 X c= proj1 Y )
assume A1: X c= Y ; ::_thesis: proj1 X c= proj1 Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 X or x in proj1 Y )
assume x in proj1 X ; ::_thesis: x in proj1 Y
then consider y being set such that
A2: [x,y] in X by Def4;
[x,y] in Y by A1, A2, TARSKI:def_3;
hence x in proj1 Y by Def4; ::_thesis: verum
end;
theorem Th11: :: XTUPLE_0:9
for X, Y being set st X c= Y holds
proj2 X c= proj2 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj2 X c= proj2 Y )
assume A1: X c= Y ; ::_thesis: proj2 X c= proj2 Y
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj2 X or x in proj2 Y )
assume x in proj2 X ; ::_thesis: x in proj2 Y
then consider y being set such that
A2: [y,x] in X by Def5;
[y,x] in Y by A1, A2, TARSKI:def_3;
hence x in proj2 Y by Def5; ::_thesis: verum
end;
definition
let X be set ;
func proj1_3 X -> set equals :: XTUPLE_0:def 14
proj1 (proj1 X);
coherence
proj1 (proj1 X) is set ;
func proj2_3 X -> set equals :: XTUPLE_0:def 15
proj2 (proj1 X);
coherence
proj2 (proj1 X) is set ;
end;
:: deftheorem defines proj1_3 XTUPLE_0:def_14_:_
for X being set holds proj1_3 X = proj1 (proj1 X);
:: deftheorem defines proj2_3 XTUPLE_0:def_15_:_
for X being set holds proj2_3 X = proj2 (proj1 X);
notation
let X be set ;
synonym proj3_3 X for proj2 X;
end;
theorem Th12: :: XTUPLE_0:10
for X, Y being set st X c= Y holds
proj1_3 X c= proj1_3 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj1_3 X c= proj1_3 Y )
assume X c= Y ; ::_thesis: proj1_3 X c= proj1_3 Y
then proj1 X c= proj1 Y by Th10;
hence proj1_3 X c= proj1_3 Y by Th10; ::_thesis: verum
end;
theorem Th13: :: XTUPLE_0:11
for X, Y being set st X c= Y holds
proj2_3 X c= proj2_3 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj2_3 X c= proj2_3 Y )
assume X c= Y ; ::_thesis: proj2_3 X c= proj2_3 Y
then proj1 X c= proj1 Y by Th10;
hence proj2_3 X c= proj2_3 Y by Th11; ::_thesis: verum
end;
theorem Th14: :: XTUPLE_0:12
for x, X being set st x in proj1_3 X holds
ex y, z being set st [x,y,z] in X
proof
let x, X be set ; ::_thesis: ( x in proj1_3 X implies ex y, z being set st [x,y,z] in X )
assume x in proj1_3 X ; ::_thesis: ex y, z being set st [x,y,z] in X
then consider y being set such that
W1: [x,y] in proj1 X by Def4;
consider z being set such that
W2: [[x,y],z] in X by W1, Def4;
take y ; ::_thesis: ex z being set st [x,y,z] in X
take z ; ::_thesis: [x,y,z] in X
thus [x,y,z] in X by W2; ::_thesis: verum
end;
theorem Th14a: :: XTUPLE_0:13
for x, y, z, X being set st [x,y,z] in X holds
x in proj1_3 X
proof
let x, y, z, X be set ; ::_thesis: ( [x,y,z] in X implies x in proj1_3 X )
assume [x,y,z] in X ; ::_thesis: x in proj1_3 X
then [x,y] in proj1 X by Def4;
hence x in proj1_3 X by Def4; ::_thesis: verum
end;
theorem Th15: :: XTUPLE_0:14
for x, X being set st x in proj2_3 X holds
ex y, z being set st [y,x,z] in X
proof
let x, X be set ; ::_thesis: ( x in proj2_3 X implies ex y, z being set st [y,x,z] in X )
assume x in proj2_3 X ; ::_thesis: ex y, z being set st [y,x,z] in X
then consider y being set such that
W1: [y,x] in proj1 X by Def5;
consider z being set such that
W2: [[y,x],z] in X by W1, Def4;
take y ; ::_thesis: ex z being set st [y,x,z] in X
take z ; ::_thesis: [y,x,z] in X
thus [y,x,z] in X by W2; ::_thesis: verum
end;
theorem Th15a: :: XTUPLE_0:15
for x, y, z, X being set st [x,y,z] in X holds
y in proj2_3 X
proof
let x, y, z, X be set ; ::_thesis: ( [x,y,z] in X implies y in proj2_3 X )
assume [x,y,z] in X ; ::_thesis: y in proj2_3 X
then [x,y] in proj1 X by Def4;
hence y in proj2_3 X by Def5; ::_thesis: verum
end;
definition
let X be set ;
func proj1_4 X -> set equals :: XTUPLE_0:def 16
proj1 (proj1_3 X);
coherence
proj1 (proj1_3 X) is set ;
func proj2_4 X -> set equals :: XTUPLE_0:def 17
proj2 (proj1_3 X);
coherence
proj2 (proj1_3 X) is set ;
end;
:: deftheorem defines proj1_4 XTUPLE_0:def_16_:_
for X being set holds proj1_4 X = proj1 (proj1_3 X);
:: deftheorem defines proj2_4 XTUPLE_0:def_17_:_
for X being set holds proj2_4 X = proj2 (proj1_3 X);
notation
let X be set ;
synonym proj3_4 X for proj2_3 X;
synonym proj4_4 X for proj2 X;
end;
theorem Th17: :: XTUPLE_0:16
for X, Y being set st X c= Y holds
proj1_4 X c= proj1_4 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj1_4 X c= proj1_4 Y )
assume X c= Y ; ::_thesis: proj1_4 X c= proj1_4 Y
then proj1_3 X c= proj1_3 Y by Th12;
hence proj1_4 X c= proj1_4 Y by Th10; ::_thesis: verum
end;
theorem Th18: :: XTUPLE_0:17
for X, Y being set st X c= Y holds
proj2_4 X c= proj2_4 Y
proof
let X, Y be set ; ::_thesis: ( X c= Y implies proj2_4 X c= proj2_4 Y )
assume X c= Y ; ::_thesis: proj2_4 X c= proj2_4 Y
then proj1_3 X c= proj1_3 Y by Th12;
hence proj2_4 X c= proj2_4 Y by Th11; ::_thesis: verum
end;
theorem Th19: :: XTUPLE_0:18
for x, X being set st x in proj1_4 X holds
ex x1, x2, x3 being set st [x,x1,x2,x3] in X
proof
let x, X be set ; ::_thesis: ( x in proj1_4 X implies ex x1, x2, x3 being set st [x,x1,x2,x3] in X )
assume x in proj1_4 X ; ::_thesis: ex x1, x2, x3 being set st [x,x1,x2,x3] in X
then consider x1 being set such that
W1: [x,x1] in proj1_3 X by Def4;
consider x2 being set such that
W2: [[x,x1],x2] in proj1 X by W1, Def4;
consider x3 being set such that
W3: [[[x,x1],x2],x3] in X by W2, Def4;
take x1 ; ::_thesis: ex x2, x3 being set st [x,x1,x2,x3] in X
take x2 ; ::_thesis: ex x3 being set st [x,x1,x2,x3] in X
take x3 ; ::_thesis: [x,x1,x2,x3] in X
thus [x,x1,x2,x3] in X by W3; ::_thesis: verum
end;
theorem Th19a: :: XTUPLE_0:19
for x, x1, x2, x3, X being set st [x,x1,x2,x3] in X holds
x in proj1_4 X
proof
let x, x1, x2, x3, X be set ; ::_thesis: ( [x,x1,x2,x3] in X implies x in proj1_4 X )
assume [x,x1,x2,x3] in X ; ::_thesis: x in proj1_4 X
then [[x,x1],x2,x3] in X ;
then [x,x1] in proj1_3 X by Th14a;
hence x in proj1_4 X by Def4; ::_thesis: verum
end;
theorem Th20: :: XTUPLE_0:20
for x, X being set st x in proj2_4 X holds
ex x1, x2, x3 being set st [x1,x,x2,x3] in X
proof
let x, X be set ; ::_thesis: ( x in proj2_4 X implies ex x1, x2, x3 being set st [x1,x,x2,x3] in X )
assume x in proj2_4 X ; ::_thesis: ex x1, x2, x3 being set st [x1,x,x2,x3] in X
then consider x1 being set such that
W1: [x1,x] in proj1_3 X by Def5;
consider x2 being set such that
W2: [[x1,x],x2] in proj1 X by W1, Def4;
consider x3 being set such that
W3: [[[x1,x],x2],x3] in X by W2, Def4;
take x1 ; ::_thesis: ex x2, x3 being set st [x1,x,x2,x3] in X
take x2 ; ::_thesis: ex x3 being set st [x1,x,x2,x3] in X
take x3 ; ::_thesis: [x1,x,x2,x3] in X
thus [x1,x,x2,x3] in X by W3; ::_thesis: verum
end;
theorem Th20a: :: XTUPLE_0:21
for x1, x, x2, x3, X being set st [x1,x,x2,x3] in X holds
x in proj2_4 X
proof
let x1, x, x2, x3, X be set ; ::_thesis: ( [x1,x,x2,x3] in X implies x in proj2_4 X )
assume [x1,x,x2,x3] in X ; ::_thesis: x in proj2_4 X
then [[x1,x],x2,x3] in X ;
then [x1,x] in proj1_3 X by Th14a;
hence x in proj2_4 X by Def5; ::_thesis: verum
end;
theorem :: XTUPLE_0:22
for a, b being quadruple set st a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 holds
a = b
proof
let a, b be quadruple set ; ::_thesis: ( a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 implies a = b )
assume Z: ( a `1_4 = b `1_4 & a `2_4 = b `2_4 & a `3_4 = b `3_4 & a `4_4 = b `4_4 ) ; ::_thesis: a = b
( a = [(a `1_4),(a `2_4),(a `3_4),(a `4_4)] & b = [(b `1_4),(b `2_4),(b `3_4),(b `4_4)] ) ;
hence a = b by Z; ::_thesis: verum
end;
begin
registration
let X be empty set ;
cluster proj1 X -> empty ;
coherence
proj1 X is empty
proof
assume not proj1 X is empty ; ::_thesis: contradiction
then consider x being set such that
W: x in proj1 X by XBOOLE_0:def_1;
ex y being set st [x,y] in X by W, Def4;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let X be empty set ;
cluster proj2 X -> empty ;
coherence
proj2 X is empty
proof
assume not proj2 X is empty ; ::_thesis: contradiction
then consider x being set such that
W: x in proj2 X by XBOOLE_0:def_1;
ex y being set st [y,x] in X by W, Def5;
hence contradiction ; ::_thesis: verum
end;
end;
registration
let X be empty set ;
cluster proj1_3 X -> empty ;
coherence
proj1_3 X is empty ;
end;
registration
let X be empty set ;
cluster proj2_3 X -> empty ;
coherence
proj2_3 X is empty ;
end;
registration
let X be empty set ;
cluster proj1_4 X -> empty ;
coherence
proj1_4 X is empty ;
end;
registration
let X be empty set ;
cluster proj2_4 X -> empty ;
coherence
proj2_4 X is empty ;
end;
theorem Th22: :: XTUPLE_0:23
for X, Y being set holds proj1 (X \/ Y) = (proj1 X) \/ (proj1 Y)
proof
let X, Y be set ; ::_thesis: proj1 (X \/ Y) = (proj1 X) \/ (proj1 Y)
thus proj1 (X \/ Y) c= (proj1 X) \/ (proj1 Y) :: according to XBOOLE_0:def_10 ::_thesis: (proj1 X) \/ (proj1 Y) c= proj1 (X \/ Y)
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in proj1 (X \/ Y) or x in (proj1 X) \/ (proj1 Y) )
assume x in proj1 (X \/ Y) ; ::_thesis: x in (proj1 X) \/ (proj1 Y)
then consider y being set such that
A1: [x,y] in X \/ Y by Def4;
( [x,y] in X or [x,y] in Y ) by A1, XBOOLE_0:def_3;
then ( x in proj1 X or x in proj1 Y ) by Def4;
hence x in (proj1 X) \/ (proj1 Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
A3: proj1 Y c= proj1 (X \/ Y) by Th10, XBOOLE_1:7;
proj1 X c= proj1 (X \/ Y) by Th10, XBOOLE_1:7;
hence (proj1 X) \/ (proj1 Y) c= proj1 (X \/ Y) by A3, XBOOLE_1:8; ::_thesis: verum
end;
theorem :: XTUPLE_0:24
for X, Y being set holds proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y)
proof
let X, Y be set ; ::_thesis: proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y)
( proj1 (X /\ Y) c= proj1 X & proj1 (X /\ Y) c= proj1 Y ) by Th10, XBOOLE_1:17;
hence proj1 (X /\ Y) c= (proj1 X) /\ (proj1 Y) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th24: :: XTUPLE_0:25
for X, Y being set holds (proj1 X) \ (proj1 Y) c= proj1 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj1 X) \ (proj1 Y) c= proj1 (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1 X) \ (proj1 Y) or x in proj1 (X \ Y) )
assume A1: x in (proj1 X) \ (proj1 Y) ; ::_thesis: x in proj1 (X \ Y)
then x in proj1 X by XBOOLE_0:def_5;
then consider y being set such that
A2: [x,y] in X by Def4;
not x in proj1 Y by A1, XBOOLE_0:def_5;
then not [x,y] in Y by Def4;
then [x,y] in X \ Y by A2, XBOOLE_0:def_5;
hence x in proj1 (X \ Y) by Def4; ::_thesis: verum
end;
theorem :: XTUPLE_0:26
for X, Y being set holds (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y)
( (proj1 X) \ (proj1 Y) c= proj1 (X \ Y) & (proj1 Y) \ (proj1 X) c= proj1 (Y \ X) ) by Th24;
then (proj1 X) \+\ (proj1 Y) c= (proj1 (X \ Y)) \/ (proj1 (Y \ X)) by XBOOLE_1:13;
hence (proj1 X) \+\ (proj1 Y) c= proj1 (X \+\ Y) by Th22; ::_thesis: verum
end;
theorem Th26: :: XTUPLE_0:27
for X, Y being set holds proj2 (X \/ Y) = (proj2 X) \/ (proj2 Y)
proof
let X, Y be set ; ::_thesis: proj2 (X \/ Y) = (proj2 X) \/ (proj2 Y)
thus proj2 (X \/ Y) c= (proj2 X) \/ (proj2 Y) :: according to XBOOLE_0:def_10 ::_thesis: (proj2 X) \/ (proj2 Y) c= proj2 (X \/ Y)
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 (X \/ Y) or y in (proj2 X) \/ (proj2 Y) )
assume y in proj2 (X \/ Y) ; ::_thesis: y in (proj2 X) \/ (proj2 Y)
then consider x being set such that
A1: [x,y] in X \/ Y by Def5;
( [x,y] in X or [x,y] in Y ) by A1, XBOOLE_0:def_3;
then ( y in proj2 X or y in proj2 Y ) by Def5;
hence y in (proj2 X) \/ (proj2 Y) by XBOOLE_0:def_3; ::_thesis: verum
end;
A3: proj2 Y c= proj2 (X \/ Y) by Th11, XBOOLE_1:7;
proj2 X c= proj2 (X \/ Y) by Th11, XBOOLE_1:7;
hence (proj2 X) \/ (proj2 Y) c= proj2 (X \/ Y) by A3, XBOOLE_1:8; ::_thesis: verum
end;
theorem :: XTUPLE_0:28
for X, Y being set holds proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y)
proof
let X, Y be set ; ::_thesis: proj2 (X /\ Y) c= (proj2 X) /\ (proj2 Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in proj2 (X /\ Y) or y in (proj2 X) /\ (proj2 Y) )
assume y in proj2 (X /\ Y) ; ::_thesis: y in (proj2 X) /\ (proj2 Y)
then consider x being set such that
A3: [x,y] in X /\ Y by Def5;
[x,y] in Y by A3, XBOOLE_0:def_4;
then A4: y in proj2 Y by Def5;
[x,y] in X by A3, XBOOLE_0:def_4;
then y in proj2 X by Def5;
hence y in (proj2 X) /\ (proj2 Y) by A4, XBOOLE_0:def_4; ::_thesis: verum
end;
theorem Th28: :: XTUPLE_0:29
for X, Y being set holds (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj2 X) \ (proj2 Y) c= proj2 (X \ Y)
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in (proj2 X) \ (proj2 Y) or y in proj2 (X \ Y) )
assume A3: y in (proj2 X) \ (proj2 Y) ; ::_thesis: y in proj2 (X \ Y)
then y in proj2 X by XBOOLE_0:def_5;
then consider x being set such that
A4: [x,y] in X by Def5;
not y in proj2 Y by A3, XBOOLE_0:def_5;
then not [x,y] in Y by Def5;
then [x,y] in X \ Y by A4, XBOOLE_0:def_5;
hence y in proj2 (X \ Y) by Def5; ::_thesis: verum
end;
theorem :: XTUPLE_0:30
for X, Y being set holds (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y)
( (proj2 X) \ (proj2 Y) c= proj2 (X \ Y) & (proj2 Y) \ (proj2 X) c= proj2 (Y \ X) ) by Th28;
then (proj2 X) \+\ (proj2 Y) c= (proj2 (X \ Y)) \/ (proj2 (Y \ X)) by XBOOLE_1:13;
hence (proj2 X) \+\ (proj2 Y) c= proj2 (X \+\ Y) by Th26; ::_thesis: verum
end;
theorem Th30: :: XTUPLE_0:31
for X, Y being set holds proj1_3 (X \/ Y) = (proj1_3 X) \/ (proj1_3 Y)
proof
let X, Y be set ; ::_thesis: proj1_3 (X \/ Y) = (proj1_3 X) \/ (proj1_3 Y)
thus proj1_3 (X \/ Y) = proj1 ((proj1 X) \/ (proj1 Y)) by Th22
.= (proj1_3 X) \/ (proj1_3 Y) by Th22 ; ::_thesis: verum
end;
theorem :: XTUPLE_0:32
for X, Y being set holds proj1_3 (X /\ Y) c= (proj1_3 X) /\ (proj1_3 Y)
proof
let X, Y be set ; ::_thesis: proj1_3 (X /\ Y) c= (proj1_3 X) /\ (proj1_3 Y)
( proj1_3 (X /\ Y) c= proj1_3 X & proj1_3 (X /\ Y) c= proj1_3 Y ) by Th12, XBOOLE_1:17;
hence proj1_3 (X /\ Y) c= (proj1_3 X) /\ (proj1_3 Y) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th32: :: XTUPLE_0:33
for X, Y being set holds (proj1_3 X) \ (proj1_3 Y) c= proj1_3 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj1_3 X) \ (proj1_3 Y) c= proj1_3 (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1_3 X) \ (proj1_3 Y) or x in proj1_3 (X \ Y) )
assume A1: x in (proj1_3 X) \ (proj1_3 Y) ; ::_thesis: x in proj1_3 (X \ Y)
then x in proj1_3 X by XBOOLE_0:def_5;
then consider y, z being set such that
A2: [x,y,z] in X by Th14;
not x in proj1_3 Y by A1, XBOOLE_0:def_5;
then not [x,y,z] in Y by Th14a;
then [x,y,z] in X \ Y by A2, XBOOLE_0:def_5;
hence x in proj1_3 (X \ Y) by Th14a; ::_thesis: verum
end;
theorem :: XTUPLE_0:34
for X, Y being set holds (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y)
( (proj1_3 X) \ (proj1_3 Y) c= proj1_3 (X \ Y) & (proj1_3 Y) \ (proj1_3 X) c= proj1_3 (Y \ X) ) by Th32;
then (proj1_3 X) \+\ (proj1_3 Y) c= (proj1_3 (X \ Y)) \/ (proj1_3 (Y \ X)) by XBOOLE_1:13;
hence (proj1_3 X) \+\ (proj1_3 Y) c= proj1_3 (X \+\ Y) by Th30; ::_thesis: verum
end;
theorem Th34: :: XTUPLE_0:35
for X, Y being set holds proj2_3 (X \/ Y) = (proj2_3 X) \/ (proj2_3 Y)
proof
let X, Y be set ; ::_thesis: proj2_3 (X \/ Y) = (proj2_3 X) \/ (proj2_3 Y)
thus proj2_3 (X \/ Y) = proj2 ((proj1 X) \/ (proj1 Y)) by Th22
.= (proj2_3 X) \/ (proj2_3 Y) by Th26 ; ::_thesis: verum
end;
theorem :: XTUPLE_0:36
for X, Y being set holds proj2_3 (X /\ Y) c= (proj2_3 X) /\ (proj2_3 Y)
proof
let X, Y be set ; ::_thesis: proj2_3 (X /\ Y) c= (proj2_3 X) /\ (proj2_3 Y)
( proj2_3 (X /\ Y) c= proj2_3 X & proj2_3 (X /\ Y) c= proj2_3 Y ) by Th13, XBOOLE_1:17;
hence proj2_3 (X /\ Y) c= (proj2_3 X) /\ (proj2_3 Y) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th36: :: XTUPLE_0:37
for X, Y being set holds (proj2_3 X) \ (proj2_3 Y) c= proj2_3 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj2_3 X) \ (proj2_3 Y) c= proj2_3 (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2_3 X) \ (proj2_3 Y) or x in proj2_3 (X \ Y) )
assume A1: x in (proj2_3 X) \ (proj2_3 Y) ; ::_thesis: x in proj2_3 (X \ Y)
then x in proj2_3 X by XBOOLE_0:def_5;
then consider y, z being set such that
A2: [y,x,z] in X by Th15;
not x in proj2_3 Y by A1, XBOOLE_0:def_5;
then not [y,x,z] in Y by Th15a;
then [y,x,z] in X \ Y by A2, XBOOLE_0:def_5;
hence x in proj2_3 (X \ Y) by Th15a; ::_thesis: verum
end;
theorem :: XTUPLE_0:38
for X, Y being set holds (proj2_3 X) \+\ (proj2_3 Y) c= proj2_3 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj2_3 X) \+\ (proj2_3 Y) c= proj2_3 (X \+\ Y)
( (proj2_3 X) \ (proj2_3 Y) c= proj2_3 (X \ Y) & (proj2_3 Y) \ (proj2_3 X) c= proj2_3 (Y \ X) ) by Th36;
then (proj2_3 X) \+\ (proj2_3 Y) c= (proj2_3 (X \ Y)) \/ (proj2_3 (Y \ X)) by XBOOLE_1:13;
hence (proj2_3 X) \+\ (proj2_3 Y) c= proj2_3 (X \+\ Y) by Th34; ::_thesis: verum
end;
theorem Th38: :: XTUPLE_0:39
for X, Y being set holds proj1_4 (X \/ Y) = (proj1_4 X) \/ (proj1_4 Y)
proof
let X, Y be set ; ::_thesis: proj1_4 (X \/ Y) = (proj1_4 X) \/ (proj1_4 Y)
thus proj1_4 (X \/ Y) = proj1 ((proj1_3 X) \/ (proj1_3 Y)) by Th30
.= (proj1_4 X) \/ (proj1_4 Y) by Th22 ; ::_thesis: verum
end;
theorem :: XTUPLE_0:40
for X, Y being set holds proj1_4 (X /\ Y) c= (proj1_4 X) /\ (proj1_4 Y)
proof
let X, Y be set ; ::_thesis: proj1_4 (X /\ Y) c= (proj1_4 X) /\ (proj1_4 Y)
( proj1_4 (X /\ Y) c= proj1_4 X & proj1_4 (X /\ Y) c= proj1_4 Y ) by Th17, XBOOLE_1:17;
hence proj1_4 (X /\ Y) c= (proj1_4 X) /\ (proj1_4 Y) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th32: :: XTUPLE_0:41
for X, Y being set holds (proj1_4 X) \ (proj1_4 Y) c= proj1_4 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj1_4 X) \ (proj1_4 Y) c= proj1_4 (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj1_4 X) \ (proj1_4 Y) or x in proj1_4 (X \ Y) )
assume A1: x in (proj1_4 X) \ (proj1_4 Y) ; ::_thesis: x in proj1_4 (X \ Y)
then x in proj1_4 X by XBOOLE_0:def_5;
then consider x1, x2, x3 being set such that
A2: [x,x1,x2,x3] in X by Th19;
not x in proj1_4 Y by A1, XBOOLE_0:def_5;
then not [x,x1,x2,x3] in Y by Th19a;
then [x,x1,x2,x3] in X \ Y by A2, XBOOLE_0:def_5;
hence x in proj1_4 (X \ Y) by Th19a; ::_thesis: verum
end;
theorem :: XTUPLE_0:42
for X, Y being set holds (proj1_4 X) \+\ (proj1_4 Y) c= proj1_4 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj1_4 X) \+\ (proj1_4 Y) c= proj1_4 (X \+\ Y)
( (proj1_4 X) \ (proj1_4 Y) c= proj1_4 (X \ Y) & (proj1_4 Y) \ (proj1_4 X) c= proj1_4 (Y \ X) ) by Th32;
then (proj1_4 X) \+\ (proj1_4 Y) c= (proj1_4 (X \ Y)) \/ (proj1_4 (Y \ X)) by XBOOLE_1:13;
hence (proj1_4 X) \+\ (proj1_4 Y) c= proj1_4 (X \+\ Y) by Th38; ::_thesis: verum
end;
theorem Th34: :: XTUPLE_0:43
for X, Y being set holds proj2_4 (X \/ Y) = (proj2_4 X) \/ (proj2_4 Y)
proof
let X, Y be set ; ::_thesis: proj2_4 (X \/ Y) = (proj2_4 X) \/ (proj2_4 Y)
thus proj2_4 (X \/ Y) = proj2 ((proj1_3 X) \/ (proj1_3 Y)) by Th30
.= (proj2_4 X) \/ (proj2_4 Y) by Th26 ; ::_thesis: verum
end;
theorem :: XTUPLE_0:44
for X, Y being set holds proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y)
proof
let X, Y be set ; ::_thesis: proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y)
( proj2_4 (X /\ Y) c= proj2_4 X & proj2_4 (X /\ Y) c= proj2_4 Y ) by Th18, XBOOLE_1:17;
hence proj2_4 (X /\ Y) c= (proj2_4 X) /\ (proj2_4 Y) by XBOOLE_1:19; ::_thesis: verum
end;
theorem Th36: :: XTUPLE_0:45
for X, Y being set holds (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y)
proof
let X, Y be set ; ::_thesis: (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y)
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in (proj2_4 X) \ (proj2_4 Y) or x in proj2_4 (X \ Y) )
assume A1: x in (proj2_4 X) \ (proj2_4 Y) ; ::_thesis: x in proj2_4 (X \ Y)
then x in proj2_4 X by XBOOLE_0:def_5;
then consider x1, x2, x3 being set such that
A2: [x1,x,x2,x3] in X by Th20;
not x in proj2_4 Y by A1, XBOOLE_0:def_5;
then not [x1,x,x2,x3] in Y by Th20a;
then [x1,x,x2,x3] in X \ Y by A2, XBOOLE_0:def_5;
hence x in proj2_4 (X \ Y) by Th20a; ::_thesis: verum
end;
theorem :: XTUPLE_0:46
for X, Y being set holds (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y)
proof
let X, Y be set ; ::_thesis: (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y)
( (proj2_4 X) \ (proj2_4 Y) c= proj2_4 (X \ Y) & (proj2_4 Y) \ (proj2_4 X) c= proj2_4 (Y \ X) ) by Th36;
then (proj2_4 X) \+\ (proj2_4 Y) c= (proj2_4 (X \ Y)) \/ (proj2_4 (Y \ X)) by XBOOLE_1:13;
hence (proj2_4 X) \+\ (proj2_4 Y) c= proj2_4 (X \+\ Y) by Th34; ::_thesis: verum
end;