:: Tuples, Projections and Cartesian Products
:: by Andrzej Trybulec
::
:: Received March 30, 1989
:: Copyright (c) 1990-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies XBOOLE_0, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, MCART_1,
XTUPLE_0, RECDEF_2, FACIRC_1;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1,
FUNCT_1;
constructors TARSKI, ENUMSET1, XTUPLE_0, SUBSET_1, FUNCT_1;
registrations RELAT_1, XTUPLE_0, SUBSET_1;
requirements SUBSET, BOOLE;
definitions TARSKI, XBOOLE_0;
equalities TARSKI, XBOOLE_0, RELAT_1, XTUPLE_0;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ENUMSET1, FUNCT_1, RELAT_1, XTUPLE_0,
XREGULAR;
schemes FUNCT_1;
begin
reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for object,
X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,
Z,Z1,Z2,Z3,Z4,Z5 for set;
reserve p for pair object;
::
:: Ordered pairs
::
:: Now we introduce the projections of ordered pairs (functions that assign
:: to an ordered pair its first and its second element). The definitions
:: are permissive, function are defined for an arbitrary object. If it is not
:: an ordered pair, they are of course meaningless.
::$CT 8
theorem
X <> {} implies ex v st v in X & not ex x,y st (x in X or y in X) & v
= [x,y]
proof
assume X <> {};
then consider Y such that
A1: Y in X and
A2: not ex Y1 st Y1 in Y & not Y1 misses X by XREGULAR:2;
take v = Y;
thus v in X by A1;
given x,y such that
A3: x in X or y in X and
A4: v = [x,y];
A5: { x,y } in Y by A4,TARSKI:def 2;
x in { x,y } & y in { x,y } by TARSKI:def 2;
hence contradiction by A2,A5,A3,XBOOLE_0:3;
end;
:: Now we prove theorems describing relationships between projections
:: of ordered pairs and Cartesian products of two sets.
theorem Th4:
z in [:X,Y:] implies z`1 in X & z`2 in Y
proof
assume z in [:X,Y:];
then consider x,y being object such that
A1: x in X & y in Y & z=[x,y] by ZFMISC_1:def 2;
thus thesis by A1;
end;
::$CT
theorem
z in [:{x},Y:] implies z`1=x & z`2 in Y
proof
assume
A1: z in [:{x},Y:];
then z`1 in {x} by Th4;
hence thesis by A1,Th4,TARSKI:def 1;
end;
theorem
z in [:X,{y}:] implies z`1 in X & z`2 = y
proof
assume
A1: z in [:X,{y}:];
then z`2 in {y} by Th4;
hence thesis by A1,Th4,TARSKI:def 1;
end;
theorem
z in [:{x},{y}:] implies z`1 = x & z`2 = y
proof
assume z in [:{x},{y}:];
then z`1 in {x} & z`2 in {y} by Th4;
hence thesis by TARSKI:def 1;
end;
theorem
z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y
proof
assume
A1: z in [:{x1,x2},Y:];
then z`1 in {x1,x2} by Th4;
hence thesis by A1,Th4,TARSKI:def 2;
end;
theorem
z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2)
proof
assume
A1: z in [:X,{y1,y2}:];
then z`2 in {y1,y2} by Th4;
hence thesis by A1,Th4,TARSKI:def 2;
end;
theorem
z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y
proof
assume z in [:{x1,x2},{y}:];
then z`1 in {x1,x2} & z`2 in {y} by Th4;
hence thesis by TARSKI:def 1,def 2;
end;
theorem
z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2)
proof
assume z in [:{x},{y1,y2}:];
then z`1 in {x} & z`2 in {y1,y2} by Th4;
hence thesis by TARSKI:def 1,def 2;
end;
theorem
z in [:{x1,x2},{y1,y2}:] implies (z`1 = x1 or z`1 = x2) & (z`2 = y1 or
z`2 = y2)
proof
assume z in [:{x1,x2},{y1,y2}:];
then z`1 in {x1,x2} & z`2 in {y1,y2} by Th4;
hence thesis by TARSKI:def 2;
end;
theorem Th14:
(ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2
proof
given y,z such that
A1: x = [y,z];
now
assume y = x;
then {{y,z},{y}} in {y} by A1,TARSKI:def 1;
hence contradiction by TARSKI:def 2;
end;
hence x <> x`1 by A1;
now
assume z = x;
then {{y,z},{y}} in {y,z} by A1,TARSKI:def 2;
hence contradiction by TARSKI:def 2;
end;
hence thesis by A1;
end;
:: Some of theorems proved above may be simplified , if we state them
:: for elements of Cartesian product rather than for arbitrary objects.
reserve R for Relation;
theorem Th15:
x in R implies x = [x`1,x`2]
proof
assume x in R;
then ex x1,x2 being object st x=[x1,x2] by RELAT_1:def 1;
hence thesis;
end;
Lm1: X1 <> {} & X2 <> {} implies
for x being Element of [:X1,X2:]
ex xx1 being Element of X1, xx2 being Element of X2 st x = [xx1,xx2]
proof
assume
A1: X1 <> {} & X2 <> {};
let x be Element of [:X1,X2:];
reconsider xx2 = x`2 as Element of X2 by A1,Th4;
reconsider xx1 = x`1 as Element of X1 by A1,Th4;
take xx1,xx2;
thus thesis by A1,Th15;
end;
registration
let X1,X2 be non empty set;
cluster -> pair for Element of [:X1,X2:];
coherence
proof let x be Element of [:X1,X2:];
ex xx1 being Element of X1, xx2 being Element of X2
st x = [xx1,xx2] by Lm1;
hence thesis;
end;
end;
theorem
X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x
= [x`1,x`2] by Th15;
theorem Th17:
[:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]}
proof
thus [:{x1,x2},{y1,y2}:] = [:{x1},{y1,y2}:] \/ [:{x2},{y1,y2}:] by
ZFMISC_1:109
.= {[x1,y1],[x1,y2]} \/ [:{x2},{y1,y2}:] by ZFMISC_1:30
.= {[x1,y1],[x1,y2]} \/ {[x2,y1],[x2,y2]} by ZFMISC_1:30
.= {[x1,y1],[x1,y2],[x2,y1],[x2,y2]} by ENUMSET1:5;
end;
theorem Th18:
X <> {} & Y <> {} implies for x being Element of [:X,Y:] holds x
<> x`1 & x <> x`2
proof
assume
A1: X <> {} & Y <> {};
let x be Element of [:X,Y:];
x = [x`1,x`2] by A1,Th15;
hence thesis by Th14;
end;
::
:: Triples
::
::$CT
theorem Th19:
X <> {} implies ex v st v in X & not ex x,y,z st (x in X or y in
X) & v = [x,y,z]
proof
assume X <> {};
then consider Y such that
A1: Y in X and
A2: not ex Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y & not Y1 misses X
by XREGULAR:4;
take v = Y;
thus v in X by A1;
given x,y,z such that
A3: x in X or y in X and
A4: v = [x,y,z];
set Y1 = { x,y }, Y2 = { Y1,{x} }, Y3 = { Y2,z };
A5: x in Y1 & y in Y1 by TARSKI:def 2;
A6: Y3 in Y by A4,TARSKI:def 2;
Y1 in Y2 & Y2 in Y3 by TARSKI:def 2;
hence contradiction by A2,A5,A6,A3,XBOOLE_0:3;
end;
::
:: Quadruples
::
::$CT 3
theorem Th20:
X <> {} implies ex v st v in X & not ex x1,x2,x3,x4 st (x1 in X
or x2 in X) & v = [x1,x2,x3,x4]
proof
assume X <> {};
then consider Y such that
A1: Y in X and
A2: for Y1,Y2,Y3,Y4,Y5 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5
in Y holds Y1 misses X by XREGULAR:6;
take v = Y;
thus v in X by A1;
given x1,x2,x3,x4 such that
A3: x1 in X or x2 in X and
A4: v = [x1,x2,x3,x4];
set Y1 = { x1,x2 }, Y2 = { Y1,{x1} }, Y3 = { Y2,x3 }, Y4 = { Y3, {Y2}}, Y5 =
{ Y4,x4 };
A5: Y3 in Y4 & Y4 in Y5 by TARSKI:def 2;
A6: Y5 in Y by A4,TARSKI:def 2;
A7: x1 in Y1 & x2 in Y1 by TARSKI:def 2;
Y1 in Y2 & Y2 in Y3 by TARSKI:def 2;
hence contradiction by A2,A7,A5,A6,A3,XBOOLE_0:3;
end;
::
:: Cartesian products of three sets
::
theorem Th21:
X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {}
proof
A1: X1 <> {} & X2 <> {} iff [:X1,X2:] <> {} by ZFMISC_1:90;
[:[:X1,X2:],X3:] = [:X1,X2,X3:] by ZFMISC_1:def 3;
hence thesis by A1,ZFMISC_1:90;
end;
reserve xx1 for Element of X1,
xx2 for Element of X2,
xx3 for Element of X3;
theorem Th22:
X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:]
implies X1=Y1 & X2=Y2 & X3=Y3)
proof
A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
assume
A2: X1<>{} & X2<>{};
assume
A3: X3<>{};
assume [:X1,X2,X3:] = [:Y1,Y2,Y3:];
then
A4: [:[:X1,X2:],X3:] = [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:def 3;
then [:X1,X2:] = [:Y1,Y2:] by A2,A3,ZFMISC_1:110;
hence thesis by A2,A3,A4,ZFMISC_1:110;
end;
theorem
[:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 &
X3=Y3
proof
assume
A1: [:X1,X2,X3:]<>{};
then
A2: X3<>{} by Th21;
X1<>{} & X2<>{} by A1,Th21;
hence thesis by A2,Th22;
end;
theorem
[:X,X,X:] = [:Y,Y,Y:] implies X = Y
proof
assume [:X,X,X:] = [:Y,Y,Y:];
then X<>{} or Y<>{} implies thesis by Th22;
hence thesis;
end;
Lm2: X1 <> {} & X2 <> {} & X3 <> {} implies
for x being Element of [:X1,X2,X3:]
ex xx1,xx2,xx3 st x = [xx1,xx2,xx3]
proof
assume that
A1: X1 <> {} & X2 <> {} and
A2: X3 <> {};
let x be Element of [:X1,X2,X3:];
reconsider x9=x as Element of [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
consider x12 being (Element of [:X1,X2:]), xx3 such that
A3: x9 = [x12,xx3] by A1,A2,Lm1;
consider xx1,xx2 such that
A4: x12 = [xx1,xx2] by A1,Lm1;
take xx1,xx2,xx3;
thus thesis by A3,A4;
end;
theorem Th25:
[:{x1},{x2},{x3}:] = { [x1,x2,x3] }
proof
thus [:{x1},{x2},{x3}:] = [:[:{x1},{x2}:],{x3}:] by ZFMISC_1:def 3
.= [:{[x1,x2]},{x3}:] by ZFMISC_1:29
.= { [x1,x2,x3] } by ZFMISC_1:29;
end;
theorem
[:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] }
proof
thus [:{x1,y1},{x2},{x3}:] = [:[:{x1,y1},{x2}:],{x3}:] by ZFMISC_1:def 3
.= [:{[x1,x2],[y1,x2]},{x3}:] by ZFMISC_1:30
.= { [x1,x2,x3],[y1,x2,x3] } by ZFMISC_1:30;
end;
theorem
[:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] }
proof
thus [:{x1},{x2,y2},{x3}:] = [:[:{x1},{x2,y2}:],{x3}:] by ZFMISC_1:def 3
.= [:{[x1,x2],[x1,y2]},{x3}:] by ZFMISC_1:30
.= { [x1,x2,x3],[x1,y2,x3] } by ZFMISC_1:30;
end;
theorem
[:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] }
proof
thus [:{x1},{x2},{x3,y3}:] = [:[:{x1},{x2}:],{x3,y3}:] by ZFMISC_1:def 3
.= [:{[x1,x2]},{x3,y3}:] by ZFMISC_1:29
.= { [x1,x2,x3],[x1,x2,y3] } by ZFMISC_1:30;
end;
theorem
[:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,
x3] }
proof
thus [:{x1,y1},{x2,y2},{x3}:] = [:[:{x1,y1},{x2,y2}:],{x3}:] by
ZFMISC_1:def 3
.= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3}:] by Th17
.= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3}:] by ENUMSET1:5
.= [:{[x1,x2],[x1,y2]},{x3}:] \/ [:{[y1,x2],[y1,y2]},{x3}:] by ZFMISC_1:97
.= { [[x1,x2],x3],[[x1,y2],x3]} \/ [:{[y1,x2],[y1,y2]},{x3}:] by
ZFMISC_1:30
.= { [[x1,x2],x3],[[x1,y2],x3]} \/ {[[y1,x2],x3],[[y1,y2],x3] } by
ZFMISC_1:30
.= { [x1,x2,x3],[x1,y2,x3],[y1,x2,x3],[[y1,y2],x3] } by ENUMSET1:5
.= { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] } by ENUMSET1:62;
end;
theorem
[:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,
y3] }
proof
thus [:{x1,y1},{x2},{x3,y3}:] = [:[:{x1,y1},{x2}:],{x3,y3}:] by
ZFMISC_1:def 3
.= [:{[x1,x2],[y1,x2]},{x3,y3}:] by ZFMISC_1:30
.= { [[x1,x2],x3],[[x1,x2],y3],[[y1,x2],x3],[[y1,x2],y3] } by Th17
.= { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] } by ENUMSET1:62;
end;
theorem
[:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,
y3] }
proof
thus [:{x1},{x2,y2},{x3,y3}:] = [:[:{x1},{x2,y2}:],{x3,y3}:] by
ZFMISC_1:def 3
.= [:{[x1,x2],[x1,y2]},{x3,y3}:] by ZFMISC_1:30
.= { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3],[[x1,y2],y3] } by Th17
.= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] } by ENUMSET1:62;
end;
theorem
[:{x1,y1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,
y2,y3], [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] }
proof
A1: [:{[x1,x2],[x1,y2]},{x3,y3}:] = { [[x1,x2],x3],[[x1,x2],y3],[[x1,y2],x3]
,[[x1,y2],y3]} by Th17
.= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} by ENUMSET1:62;
A2: [:{[y1,x2],[y1,y2]},{x3,y3}:] = { [[y1,x2],x3],[[y1,x2],y3],[[y1,y2],x3]
,[[y1,y2],y3]} by Th17
.= { [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3]} by ENUMSET1:62;
thus [:{x1,y1},{x2,y2},{x3,y3}:] = [:[:{x1,y1},{x2,y2}:],{x3,y3}:] by
ZFMISC_1:def 3
.= [:{[x1,x2],[x1,y2],[y1,x2],[y1,y2]},{x3,y3}:] by Th17
.= [:{[x1,x2],[x1,y2]} \/ {[y1,x2],[y1,y2]},{x3,y3}:] by ENUMSET1:5
.= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3]} \/ {[y1,x2,x3],[y1,y2,
x3],[y1,x2,y3],[y1,y2,y3] } by A1,A2,ZFMISC_1:97
.= { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3], [y1,x2,x3],[y1,y2,x3],
[y1,x2,y3],[y1,y2,y3] } by ENUMSET1:25;
end;
registration
let X1,X2,X3 be non empty set;
cluster -> triple for Element of [:X1,X2,X3:];
coherence
proof let x be Element of [:X1,X2,X3:];
ex xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] by Lm2;
hence thesis;
end;
end;
definition
::$CD 4
let X1,X2,X3 be non empty set;
let x be Element of [:X1,X2,X3:];
redefine func x`1_3 -> Element of X1 means :: redefines `1_3 (XTUPLE_0, definition)
x = [x1,x2,x3] implies it = x1;
coherence
proof
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A1: x = [xx1,xx2,xx3] by Lm2;
thus x`1_3 is Element of X1 by A1;
end;
compatibility
proof let y be Element of X1;
thus y = x`1_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1;
assume
A2: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x1;
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A3: x = [xx1,xx2,xx3] by Lm2;
thus y = x`1_3 by A2,A3;
end;
redefine func x`2_3 -> Element of X2 means :: redefines `2_3 (XTUPLE_0, definition)
x = [x1,x2,x3] implies it = x2;
coherence
proof
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A4: x = [xx1,xx2,xx3] by Lm2;
thus x`2_3 is Element of X2 by A4;
end;
compatibility
proof let y be Element of X2;
thus y = x`2_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2;
assume
A5: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x2;
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A6: x = [xx1,xx2,xx3] by Lm2;
thus y = x`2_3 by A5,A6;
end;
redefine func x`3_3 -> Element of X3 means :: redefines `3_3 (XTUPLE_0, synonym) → `2 (XTUPLE_0, definition)
x = [x1,x2,x3] implies it = x3;
coherence
proof
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A7: x = [xx1,xx2,xx3] by Lm2;
thus x`3_3 is Element of X3 by A7;
end;
compatibility
proof let y be Element of X3;
thus y = x`3_3 implies for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3;
assume
A8: for x1,x2,x3 holds x = [x1,x2,x3] implies y = x3;
consider xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 such that
A9: x = [xx1,xx2,xx3] by Lm2;
thus y = x`3_3 by A8,A9;
end;
end;
::$CT 2
theorem Th34:
X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {}
proof
assume that
A1: X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] and
A2: X <> {};
[:X,Y,Z:]<>{} or [:Y,Z,X:]<>{} or [:Z,X,Y:]<>{} by A1,A2;
then reconsider X,Y,Z as non empty set by Th21;
per cases by A1;
suppose
A3: X c= [:X,Y,Z:];
consider v such that
A4: v in X and
A5: for x,y,z st x in X or y in X holds v <> [x,y,z] by Th19;
reconsider v as Element of [:X,Y,Z:] by A3,A4;
v = [v`1_3,v`2_3,v`3_3];
hence contradiction by A5;
end;
suppose
X c= [:Y,Z,X:];
then X c= [:[:Y,Z:],X:] by ZFMISC_1:def 3;
hence thesis by ZFMISC_1:111;
end;
suppose
A6: X c= [:Z,X,Y:];
consider v such that
A7: v in X and
A8: for z,x,y st z in X or x in X holds v <> [z,x,y] by Th19;
reconsider v as Element of [:Z,X,Y:] by A6,A7;
v = [v`1_3,v`2_3,v`3_3];
hence thesis by A8;
end;
end;
::$CT
theorem Th35:
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,X3:]
holds x <> x`1_3 & x <> x`2_3 & x <> x`3_3
proof let X1,X2,X3 be non empty set;
let x be Element of [:X1,X2,X3:];
set Y9 = { x`1_3,x`2_3 }, Y = { Y9,{x`1_3}},
X9 = { Y,x`3_3 }, X = { X9,{Y} };
A1: x = [x`1_3,x`2_3,x`3_3]
.= [[x`1_3,x`2_3],x`3_3];
then x = x`1_3 or x = x`2_3 implies X in Y9 & Y9 in Y & Y in X9 & X9 in X
by TARSKI:def 2;
hence x <> x`1_3 & x <> x`2_3 by XREGULAR:8;
thus thesis by A1,Th14;
end;
theorem
[:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies X1 meets Y1 & X2 meets Y2 & X3
meets Y3
proof
assume
A1: [:X1,X2,X3:] meets [:Y1,Y2,Y3:];
A2: [:[:X1,X2:],X3:] = [:X1,X2,X3:] & [:[:Y1,Y2:],Y3:] = [:Y1,Y2,Y3:] by
ZFMISC_1:def 3;
then [:X1,X2:] meets [:Y1,Y2:] by A1,ZFMISC_1:104;
hence thesis by A2,A1,ZFMISC_1:104;
end;
::
:: Cartesian products of four sets
::
theorem Th37:
[:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:]
proof
thus [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4
.= [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3;
end;
theorem Th38:
[:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:]
proof
thus [:[:X1,X2:],X3,X4:] = [:[:[:X1,X2:],X3:],X4:] by ZFMISC_1:def 3
.= [:X1,X2,X3,X4:] by Th37;
end;
theorem Th39:
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <>
{}
proof
A1: [:[:X1,X2,X3:],X4:] = [:X1,X2,X3,X4:] by ZFMISC_1:def 4;
X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {} by Th21;
hence thesis by A1,ZFMISC_1:90;
end;
theorem Th40:
X1<>{} & X2<>{} & X3<>{} & X4<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3
,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4
proof
A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
assume
A2: X1<>{} & X2<>{} & X3<>{};
assume
A3: X4<>{};
assume [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:];
then
A4: [:[:X1,X2,X3:],X4:] = [:[:Y1,Y2,Y3:],Y4:] by A1,ZFMISC_1:def 4;
[:X1,X2,X3:] = [:Y1,Y2,Y3:] by A3,A4,A2,ZFMISC_1:110;
hence thesis by A2,A3,A4,Th22,ZFMISC_1:110;
end;
theorem
[:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1
& X2=Y2 & X3=Y3 & X4=Y4
proof
assume
A1: [:X1,X2,X3,X4:]<>{};
then
A2: X3<>{} & X4<>{} by Th39;
X1<>{} & X2<>{} by A1,Th39;
hence thesis by A2,Th40;
end;
theorem
[:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y
proof
assume [:X,X,X,X:] = [:Y,Y,Y,Y:];
then X<>{} or Y<>{} implies thesis by Th40;
hence thesis;
end;
reserve xx4 for Element of X4;
Lm3: X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies for x being Element of
[:X1,X2,X3,X4:] ex xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4]
proof
assume that
A1: X1 <> {} & X2 <> {} & X3 <> {} and
A2: X4 <> {};
let x be Element of [:X1,X2,X3,X4:];
reconsider x9=x as Element of [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
consider x123 being (Element of [:X1,X2,X3:]), xx4 such that
A3: x9 = [x123,xx4] by A2,Lm1,A1;
consider xx1,xx2,xx3 such that
A4: x123 = [xx1,xx2,xx3] by A1,Lm2;
take xx1,xx2,xx3,xx4;
thus thesis by A3,A4;
end;
registration
let X1,X2,X3,X4 be non empty set;
cluster -> quadruple for Element of [:X1,X2,X3,X4:];
coherence
proof let x be Element of [:X1,X2,X3,X4:];
ex xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4
st x = [xx1,xx2,xx3,xx4] by Lm3;
hence thesis;
end;
end;
definition
let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
redefine func x`1_4 -> Element of X1 means :: redefines `1_4 (XTUPLE_0, definition)
x = [x1,x2,x3,x4] implies it = x1;
coherence
proof
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A1: x = [xx1,xx2,xx3,xx4] by Lm3;
thus x`1_4 is Element of X1 by A1;
end;
compatibility
proof let y be Element of X1;
thus y = x`1_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
implies y = x1;
assume
A2: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x1;
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A3: x = [xx1,xx2,xx3,xx4] by Lm3;
thus y = x`1_4 by A2,A3;
end;
redefine func x`2_4 -> Element of X2 means :: redefines `2_4 (XTUPLE_0, definition)
x = [x1,x2,x3,x4] implies it = x2;
coherence
proof
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A4: x = [xx1,xx2,xx3,xx4] by Lm3;
thus x`2_4 is Element of X2 by A4;
end;
compatibility
proof let y be Element of X2;
thus y = x`2_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
implies y = x2;
assume
A5: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x2;
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A6: x = [xx1,xx2,xx3,xx4] by Lm3;
thus y = x`2_4 by A5,A6;
end;
redefine func x`3_4 -> Element of X3 means :: redefines `3_4 (XTUPLE_0, synonym) → `2_3 (XTUPLE_0, definition)
x = [x1,x2,x3,x4] implies it = x3;
coherence
proof
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A7: x = [xx1,xx2,xx3,xx4] by Lm3;
thus x`3_4 is Element of X3 by A7;
end;
compatibility
proof let y be Element of X3;
thus y = x`3_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
implies y = x3;
assume
A8: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x3;
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A9: x = [xx1,xx2,xx3,xx4] by Lm3;
thus y = x`3_4 by A8,A9;
end;
redefine func x`4_4 -> Element of X4 means :: redefines `4_4 (XTUPLE_0, synonym) → `2 (XTUPLE_0, definition)
x = [x1,x2,x3,x4] implies it = x4;
coherence
proof
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A10: x = [xx1,xx2,xx3,xx4] by Lm3;
thus x`4_4 is Element of X4 by A10;
end;
compatibility
proof let y be Element of X4;
thus y = x`4_4 implies for x1,x2,x3,x4 holds x = [x1,x2,x3,x4]
implies y = x4;
assume
A11: for x1,x2,x3,x4 holds x = [x1,x2,x3,x4] implies y = x4;
consider xx1 being Element of X1, xx2 being Element of X2,
xx3 being Element of X3, xx4 being Element of X4 such that
A12: x = [xx1,xx2,xx3,xx4] by Lm3;
thus y = x`4_4 by A11,A12;
end;
end;
::$CT 3
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
holds x <> x`1_4 & x <> x`2_4 & x <> x`3_4 & x <> x`4_4
proof let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
reconsider Y = [:X1,X2:], X3, X4 as non empty set;
reconsider x9=x as Element of [:Y,X3,X4:] by Th38;
set Z9 = { x`1_4,x`2_4 }, Z = { Z9,{x`1_4}},
Y9 = { Z,x`3_4 }, Y = { Y9,{Z} }, X9 =
{ Y,x`4_4 }, X = { X9,{Y} };
x = [x`1_4,x`2_4,x`3_4,x`4_4]
.= X;
then
x = x`1_4 or x = x`2_4
implies X in Z9 & Z9 in Z & Z in Y9 & Y9 in Y & Y in X9 & X9 in X
by TARSKI:def 2;
hence x <> x`1_4 & x <> x`2_4 by XREGULAR:10;
x`3_4 = (x qua set)`1`2
.= x9`2_3;
hence thesis by Th35;
end;
theorem
X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,X2
:] or X1 c= [:X4,X1,X2,X3:] implies X1 = {}
proof
assume that
A1: X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:] or X1 c= [:X3,X4,X1,
X2:] or X1 c= [:X4,X1,X2,X3:] and
A2: X1 <> {};
A3: [:X1,X2,X3,X4:]<>{} or [:X2,X3,X4,X1:]<>{} or [:X3,X4,X1,X2:]<>{} or [:
X4,X1,X2,X3:]<>{} by A1,A2;
reconsider X1,X2,X3,X4 as non empty set by A3,Th39;
per cases by A1;
suppose
A4: X1 c= [:X1,X2,X3,X4:];
consider v such that
A5: v in X1 and
A6: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4]
by Th20;
reconsider v as Element of [:X1,X2,X3,X4:] by A4,A5;
v = [v`1_4,v`2_4,v`3_4,v`4_4];
hence contradiction by A6;
end;
suppose
X1 c= [:X2,X3,X4,X1:];
then X1 c= [:[:X2,X3:],X4,X1:] by Th38;
hence thesis by Th34;
end;
suppose
X1 c= [:X3,X4,X1,X2:];
then X1 c= [:[:X3,X4:],X1,X2:] by Th38;
hence thesis by Th34;
end;
suppose
A7: X1 c= [:X4,X1,X2,X3:];
consider v such that
A8: v in X1 and
A9: for x1,x2,x3,x4 st x1 in X1 or x2 in X1 holds v <> [x1,x2,x3,x4]
by Th20;
reconsider v as Element of [:X4,X1,X2,X3:] by A7,A8;
v = [v`1_4,v`2_4,v`3_4,v`4_4];
hence thesis by A9;
end;
end;
theorem
[:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies X1 meets Y1 & X2 meets
Y2 & X3 meets Y3 & X4 meets Y4
proof
assume
A1: [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:];
A2: [:[:[:X1,X2:],X3:],X4:] = [:X1,X2,X3,X4:] & [:[:[:Y1,Y2:],Y3:],Y4:] = [:
Y1, Y2,Y3,Y4:] by Th37;
then
A3: [:[:X1,X2:],X3:] meets [:[:Y1,Y2:],Y3:] by A1,ZFMISC_1:104;
then [:X1,X2:] meets [:Y1,Y2:] by ZFMISC_1:104;
hence thesis by A2,A1,A3,ZFMISC_1:104;
end;
theorem
[:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] }
proof
thus [:{x1},{x2},{x3},{x4}:] = [:[:{x1},{x2}:],{x3},{x4}:] by Th38
.= [:{[x1,x2]},{x3},{x4}:] by ZFMISC_1:29
.= {[[x1,x2],x3,x4]} by Th25
.= { [x1,x2,x3,x4] };
end;
:: Ordered pairs
theorem Th48:
[:X,Y:] <> {} implies for x being Element of [:X,Y:] holds x <>
x`1 & x <> x`2
proof
assume [:X,Y:] <> {};
then X <> {} & Y <> {} by ZFMISC_1:90;
hence thesis by Th18;
end;
theorem
x in [:X,Y:] implies x <> x`1 & x <> x`2 by Th48;
:: Triples
reserve A1 for Subset of X1,
A2 for Subset of X2,
A3 for Subset of X3,
A4 for Subset of X4;
reserve x for Element of [:X1,X2,X3:];
theorem
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,X3:]
for x1,x2,x3 st x = [x1,x2,x3] holds
x`1_3 = x1 & x`2_3 = x2 & x`3_3 = x3;
theorem
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,X3:]
st for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1
holds y1 =x`1_3
proof let X1,X2,X3 be non empty set;
let x be Element of [:X1,X2,X3:];
assume that
A1: for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1;
x = [x`1_3,x`2_3,x`3_3];
hence thesis by A1;
end;
theorem
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,X3:]
st for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2
holds y2 =x`2_3
proof let X1,X2,X3 be non empty set;
let x be Element of [:X1,X2,X3:];
assume that
A1: for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y2 = xx2;
x = [x`1_3,x`2_3,x`3_3];
hence thesis by A1;
end;
theorem
for X1,X2,X3 being non empty set
for x being Element of [:X1,X2,X3:]
st for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3
holds y3 =x`3_3
proof
let X1,X2,X3 be non empty set;
let x be Element of [:X1,X2,X3:];
assume that
A1: for xx1 being Element of X1,xx2 being Element of X2,
xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3;
x = [x`1_3,x`2_3,x`3_3];
hence thesis by A1;
end;
theorem Th54:
z in [: X1,X2,X3 :] implies ex x1,x2,x3 st x1 in X1 & x2 in X2 &
x3 in X3 & z = [x1,x2,x3]
proof
assume z in [: X1,X2,X3 :];
then z in [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
then consider x12, x3 being object such that
A1: x12 in [:X1,X2:] and
A2: x3 in X3 and
A3: z = [x12,x3] by ZFMISC_1:def 2;
consider x1,x2 being object such that
A4: x1 in X1 & x2 in X2 and
A5: x12 = [x1,x2] by A1,ZFMISC_1:def 2;
z = [x1,x2,x3] by A3,A5;
hence thesis by A2,A4;
end;
theorem Th55:
[x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3
proof
A1: [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87;
[:X1,X2,X3:] = [:[:X1,X2:],X3:] by ZFMISC_1:def 3;
hence thesis by A1,ZFMISC_1:87;
end;
theorem
(for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3
& z = [x1,x2,x3]) implies Z = [: X1,X2,X3 :]
proof
assume
A1: for z holds z in Z iff ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3
& z = [x1,x2,x3];
now
let z be object;
thus z in Z implies z in [:[:X1,X2:],X3:]
proof
assume z in Z;
then consider x1,x2,x3 such that
A2: x1 in X1 & x2 in X2 and
A3: x3 in X3 & z = [x1,x2,x3] by A1;
[x1,x2] in [:X1,X2:] by A2,ZFMISC_1:def 2;
hence thesis by A3,ZFMISC_1:def 2;
end;
assume z in [:[:X1,X2:],X3:];
then consider x12,x3 being object such that
A4: x12 in [:X1,X2:] and
A5: x3 in X3 and
A6: z = [x12,x3] by ZFMISC_1:def 2;
consider x1,x2 being object such that
A7: x1 in X1 & x2 in X2 and
A8: x12 = [x1,x2] by A4,ZFMISC_1:def 2;
z = [x1,x2,x3] by A6,A8;
hence z in Z by A1,A5,A7;
end;
then Z = [:[:X1,X2:],X3:] by TARSKI:2;
hence thesis by ZFMISC_1:def 3;
end;
::$CT
theorem
for X1,X2,X3 being non empty set
for A1 being non empty Subset of X1, A2 being non empty Subset of X2,
A3 being non empty Subset of X3
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:]
holds x`1_3 in A1 & x`2_3 in A2 & x`3_3 in A3
proof
let X1,X2,X3 be non empty set;
let A1 be non empty Subset of X1, A2 be non empty Subset of X2,
A3 be non empty Subset of X3;
let x be Element of [:X1,X2,X3:];
assume
x in [:A1,A2,A3:];
then reconsider y = x as Element of [:A1,A2,A3:];
A1: y`2_3 in A2;
A2: y`3_3 in A3;
y`1_3 in A1;
hence thesis by A1,A2;
end;
theorem Th58:
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,
Y3:]
proof
A1: [:X1,X2,X3:] = [:[:X1,X2:],X3:] & [:Y1,Y2,Y3:] = [:[:Y1,Y2:],Y3:] by
ZFMISC_1:def 3;
assume X1 c= Y1 & X2 c= Y2;
then
A2: [:X1,X2:] c= [:Y1,Y2:] by ZFMISC_1:96;
assume X3 c= Y3;
hence thesis by A2,A1,ZFMISC_1:96;
end;
:: Quadruples
reserve x for Element of [:X1,X2,X3,X4:];
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
for x1,x2,x3,x4 being set st x = [x1,
x2,x3,x4] holds x`1_4 = x1 & x`2_4 = x2 & x`3_4 = x3 & x`4_4 = x4;
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
st for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1
holds y1 =x`1_4
proof
let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
assume that
A1: for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1;
x = [x`1_4,x`2_4,x`3_4,x`4_4];
hence thesis by A1;
end;
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
st for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,
xx2,xx3,xx4] holds y2 = xx2
holds y2 =x`2_4
proof
let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
assume that
A1: for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2;
x = [x`1_4,x`2_4,x`3_4,x`4_4];
hence thesis by A1;
end;
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
st for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,
xx2,xx3,xx4] holds y3 = xx3
holds y3 =x`3_4
proof
let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
assume that
A1: for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3;
x = [x`1_4,x`2_4,x`3_4,x`4_4];
hence thesis by A1;
end;
theorem
for X1,X2,X3,X4 being non empty set
for x being Element of [:X1,X2,X3,X4:]
st for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,
xx2,xx3,xx4] holds y4 = xx4
holds y4 =x`4_4
proof
let X1,X2,X3,X4 be non empty set;
let x be Element of [:X1,X2,X3,X4:];
assume that
A1: for xx1 being Element of X1,
xx2 being Element of X2,
xx3 being Element of X3,
xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4;
x = [x`1_4,x`2_4,x`3_4,x`4_4];
hence thesis by A1;
end;
theorem
z in [: X1,X2,X3,X4 :] implies ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 &
x3 in X3 & x4 in X4 & z = [x1,x2,x3,x4]
proof
assume z in [: X1,X2,X3,X4 :];
then z in [:[:X1,X2,X3:],X4:] by ZFMISC_1:def 4;
then consider x123, x4 being object such that
A1: x123 in [:X1,X2,X3:] and
A2: x4 in X4 and
A3: z = [x123,x4] by ZFMISC_1:def 2;
consider x1, x2, x3 such that
A4: x1 in X1 & x2 in X2 & x3 in X3 and
A5: x123 = [x1,x2,x3] by A1,Th54;
z = [x1,x2,x3,x4] by A3,A5;
hence thesis by A2,A4;
end;
theorem
[x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3
& x4 in X4
proof
A1: [x1,x2] in [:X1,X2:] iff x1 in X1 & x2 in X2 by ZFMISC_1:87;
[:X1,X2,X3,X4:] = [:[:X1,X2:],X3,X4:] & [x1,x2,x3,x4] = [[x1,x2],x3,x4]
by Th38;
hence thesis by A1,Th55;
end;
theorem
(for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in
X3 & x4 in X4 & z = [x1,x2,x3,x4]) implies Z = [: X1,X2,X3,X4 :]
proof
assume
A1: for z holds z in Z iff ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in
X3 & x4 in X4 & z = [x1,x2,x3,x4];
now
let z be object;
thus z in Z implies z in [:[:X1,X2,X3:],X4:]
proof
assume z in Z;
then consider x1,x2,x3,x4 such that
A2: x1 in X1 & x2 in X2 & x3 in X3 and
A3: x4 in X4 & z = [x1,x2,x3,x4] by A1;
[x1,x2,x3] in [:X1,X2,X3:] by A2,Th55;
hence thesis by A3,ZFMISC_1:def 2;
end;
assume z in [:[:X1,X2,X3:],X4:];
then consider x123,x4 being object such that
A4: x123 in [:X1,X2,X3:] and
A5: x4 in X4 and
A6: z = [x123,x4] by ZFMISC_1:def 2;
consider x1,x2,x3 such that
A7: x1 in X1 & x2 in X2 & x3 in X3 and
A8: x123 = [x1,x2,x3] by A4,Th54;
z = [x1,x2,x3,x4] by A6,A8;
hence z in Z by A1,A5,A7;
end;
then Z = [:[:X1,X2,X3:],X4:] by TARSKI:2;
hence thesis by ZFMISC_1:def 4;
end;
::$CT
theorem
for X1,X2,X3,X4 being non empty set,
A1 being non empty Subset of X1, A2 being non empty Subset of X2,
A3 being non empty Subset of X3, A4 being non empty Subset of X4
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:]
holds x`1_4 in A1 & x`2_4 in A2 & x`3_4 in A3 & x`4_4 in A4
proof
let X1,X2,X3,X4 be non empty set,
A1 be non empty Subset of X1, A2 be non empty Subset of X2,
A3 be non empty Subset of X3, A4 be non empty Subset of X4;
let x be Element of [:X1,X2,X3,X4:];
assume
x in [:A1,A2,A3,A4:];
then reconsider y = x as Element of [:A1,A2,A3,A4:];
A1: y`2_4 in A2;
A2: y`4_4 in A4;
A3: y`3_4 in A3;
y`1_4 in A1;
hence thesis by A1,A3,A2;
end;
theorem Th68:
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4
implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:]
proof
A1: [:X1,X2,X3,X4:] = [:[:X1,X2,X3:],X4:] & [:Y1,Y2,Y3,Y4:] = [:[:Y1,Y2,Y3:]
,Y4 :] by ZFMISC_1:def 4;
assume X1 c= Y1 & X2 c= Y2 & X3 c= Y3;
then
A2: [:X1,X2,X3:] c= [:Y1,Y2,Y3:] by Th58;
assume X4 c= Y4;
hence thesis by A2,A1,ZFMISC_1:96;
end;
definition
let X1,X2,A1,A2;
redefine func [:A1,A2:] -> Subset of [:X1,X2:]; :: redefines [: (ZFMISC_1, definition)
coherence by ZFMISC_1:96;
end;
definition
let X1,X2,X3,A1,A2,A3;
redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:]; :: redefines [: (ZFMISC_1, definition)
coherence by Th58;
end;
definition
let X1,X2,X3,X4,A1,A2,A3,A4;
redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:]; :: redefines [: (ZFMISC_1, definition)
coherence by Th68;
end;
begin :: Addenda
:: from DTCONSTR
definition
let f be Function;
func pr1 f -> Function means
dom it = dom f & for x being object st x in dom f
holds it.x = (f.x)`1;
existence
proof
deffunc F(object) = (f.$1)`1;
ex g being Function st dom g = dom f & for x being object st x in dom f
holds g.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let p1, p2 be Function such that
A1: dom p1 = dom f and
A2: for x being object st x in dom f holds p1.x = (f.x)`1 and
A3: dom p2 = dom f and
A4: for x being object st x in dom f holds p2.x = (f.x)`1;
now
let x be object;
assume
A5: x in dom f;
then p1.x = (f.x)`1 by A2;
hence p1.x = p2.x by A4,A5;
end;
hence thesis by A1,A3,FUNCT_1:2;
end;
func pr2 f -> Function means
dom it = dom f & for x being object st x in dom f
holds it.x = (f.x)`2;
existence
proof
deffunc F(object) = (f.$1)`2;
ex g being Function st dom g = dom f & for x being object st x in dom f
holds g.x = F(x) from FUNCT_1:sch 3;
hence thesis;
end;
uniqueness
proof
let p1, p2 be Function such that
A6: dom p1 = dom f and
A7: for x being object st x in dom f holds p1.x = (f.x)`2 and
A8: dom p2 = dom f and
A9: for x being object st x in dom f holds p2.x = (f.x)`2;
now
let x be object;
assume
A10: x in dom f;
then p1.x = (f.x)`2 by A7;
hence p1.x = p2.x by A9,A10;
end;
hence thesis by A6,A8,FUNCT_1:2;
end;
end;
definition
let x be object;
func x`11 -> set equals
x`1`1;
coherence by TARSKI:1;
func x`12 -> set equals
x`1`2;
coherence by TARSKI:1;
func x`21 -> set equals
x`2`1;
coherence by TARSKI:1;
func x`22 -> set equals
x`2`2;
coherence by TARSKI:1;
end;
reserve x for object;
theorem
[[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[
y1,y2]]`22 = y2;
:: missing, 2007.04.13, A.T.
theorem
x in R implies x`1 in dom R & x`2 in rng R
proof
assume
A1: x in R;
then x = [x`1,x`2] by Th15;
hence thesis by A1,XTUPLE_0:def 12,def 13;
end;
:: 2009.08.29, A.T.
theorem Th71:
for R being non empty Relation, x being object
holds Im(R,x) = { I`2 where I is Element of R: I`1 = x }
proof let R be non empty Relation, x being object;
set X = { I`2 where I is Element of R: I`1 = x };
thus Im(R,x) c= X
proof let z be object;
assume z in Im(R,x);
then consider y being object such that
A1: [y,z] in R and
A2: y in {x} by RELAT_1:def 13;
A3: y = x by A2,TARSKI:def 1;
y = [y,z]`1 & z = [y,z]`2;
hence z in X by A1,A3;
end;
let z be object;
assume z in X;
then consider I being Element of R such that
A4: z= I`2 and
A5: I`1 = x;
A6: I = [I`1,I`2] by Th15;
x in {x} by TARSKI:def 1;
hence z in Im(R,x) by A4,A5,A6,RELAT_1:def 13;
end;
theorem
x in R implies x`2 in Im(R,x`1)
proof
assume
A1: x in R;
then x`2 in { I`2 where I is Element of R: I`1 = x`1 };
hence thesis by A1,Th71;
end;
theorem Th73:
x in R & y in R & x`1 = y`1 & x`2 = y`2 implies x = y
proof assume x in R & y in R;
then x = [x`1,x`2] & y = [y`1,y`2] by Th15;
hence thesis;
end;
theorem
for R being non empty Relation, x,y being Element of R
st x`1 = y`1 & x`2 = y`2
holds x = y by Th73;
:: 2010.05.120, A.T.
theorem
proj1 proj1 {[x1,x2,x3],[y1,y2,y3]} = {x1,y1}
proof
thus proj1 proj1 {[x1,x2,x3],[y1,y2,y3]}
= proj1 {[x1,x2],[y1,y2]} by RELAT_1:10
.= {x1,y1} by RELAT_1:10;
end;
theorem
proj1 proj1 {[x1,x2,x3]} = {x1}
proof
thus proj1 proj1 {[x1,x2,x3]}
= proj1 {[x1,x2]} by RELAT_1:9
.= {x1} by RELAT_1:9;
end;
scheme
BiFuncEx{A()->set,B()->set,C()->set,P[object,object,object]}:
ex f,g being Function
st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x]
provided
A1: x in A() implies ex y,z st y in B() & z in C() & P[x,y,z];
defpred H[object,object] means
for y,z st $2`1 = y & $2`2 = z holds P[$1,y,z];
A2: for x being object st x in A()
ex p being object st p in [:B(),C():] & H[x,p]
proof let x be object;
assume x in A();
then consider y,z such that
A3: y in B() & z in C() and
A4: P[x,y,z] by A1;
reconsider p=[y,z] as set;
take p;
thus p in [:B(),C():] by A3,ZFMISC_1:87;
thus for y,z st p`1 = y & p`2 = z holds P[x,y,z]
by A4;
end;
consider h being Function such that
dom h = A() & rng h c= [:B(),C():] and
A5: for x being object st x in A() holds H[x,h.x] from FUNCT_1:sch 6(A2);
deffunc g(object) = (h.$1)`2;
deffunc f(object) = (h.$1)`1;
consider f being Function such that
A6: dom f = A() and
A7: for x being object st x in A() holds f.x = f(x) from FUNCT_1:sch 3;
consider g being Function such that
A8: dom g = A() and
A9: for x being object st x in A() holds g.x = g(x) from FUNCT_1:sch 3;
take f,g;
thus dom f = A() & dom g = A() by A6,A8;
thus for x st x in A() holds P[x,f.x,g.x]
proof
let x;
assume
A10: x in A();
then f.x = (h.x)`1 & g.x = (h.x)`2 by A7,A9;
hence thesis by A5,A10;
end;
end;
theorem
[[x1,x2],[x3,x4]] = [[y1,y2],[y3,y4]] implies x1=y1 & x2=y2 & x3=y3 & x4=y4
proof
assume [[x1,x2],[x3,x4]] = [[y1,y2],[y3,y4]];
then [x1,x2] = [y1,y2] & [x3,x4] = [y3,y4] by XTUPLE_0:1;
hence x1=y1 & x2=y2 & x3=y3 & x4=y4 by XTUPLE_0:1;
end;