Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Tuples, Projections and Cartesian Products

by
Andrzej Trybulec

MML identifier: MCART_1
[ Mizar article, MML identifier index ]

```environ

vocabulary BOOLE, TARSKI, MCART_1;
notation TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1;
constructors TARSKI, ENUMSET1, SUBSET_1, XBOOLE_0;
clusters XBOOLE_0, ZFMISC_1;
requirements SUBSET, BOOLE;

begin

reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for set,
X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set;

::
::   Regularity
::

:: We start with some auxiliary theorems related to the regularity axiom.
:: We need them to prove theorems below. Nevertheless they are
:: marked as theorems because they seem to be of general interest.

theorem :: MCART_1:1
X <> {} implies ex Y st Y in X & Y misses X;

theorem :: MCART_1:2
X <> {} implies ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X;

theorem :: MCART_1:3
X <> {} implies
ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X;

theorem :: MCART_1:4
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X;

theorem :: MCART_1:5
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in
Y holds Y1 misses X;

theorem :: MCART_1:6
X <> {} implies
ex Y st Y in X &
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;

::
::   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.

definition let x;
given x1,x2 being set such that
x = [x1,x2];
func x`1 means
:: MCART_1:def 1
x = [y1,y2] implies it = y1;
func x`2 means
:: MCART_1:def 2
x = [y1,y2] implies it = y2;
end;

theorem :: MCART_1:7
[x,y]`1=x & [x,y]`2=y;

theorem :: MCART_1:8
(ex x,y st z=[x,y]) implies [z`1,z`2] =z;

theorem :: MCART_1:9
X <> {} implies
ex v st v in X & not ex x,y st (x in X or y in X) & v = [x,y];

:: Now we prove theorems describing relationships between projections
:: of ordered pairs and Cartesian products of two sets.

theorem :: MCART_1:10
z in [:X,Y:] implies z`1 in X & z`2 in Y;

theorem :: MCART_1:11
(ex x,y st z=[x,y]) & z`1 in X & z`2 in Y implies z in [:X,Y:];

theorem :: MCART_1:12
z in [:{x},Y:] implies z`1=x & z`2 in Y;

theorem :: MCART_1:13
z in [:X,{y}:] implies z`1 in X & z`2 = y;

theorem :: MCART_1:14
z in [:{x},{y}:] implies z`1 = x & z`2 = y;

theorem :: MCART_1:15
z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y;

theorem :: MCART_1:16
z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:17
z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y;

theorem :: MCART_1:18
z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:19
z in [:{x1,x2},{y1,y2}:] implies
(z`1 = x1 or z`1 = x2) & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:20
(ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2;

:: Some of theorems proved above may be simplified , if we state them
:: for elements of Cartesian product rather than for arbitrary objects.

canceled 2;

theorem :: MCART_1:23
x in [:X,Y:] implies x = [x`1,x`2];

theorem :: MCART_1:24
X <> {} & Y <> {} implies
for x being Element of [:X,Y:] holds x = [x`1,x`2];

theorem :: MCART_1:25
[:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]};

theorem :: MCART_1:26
X <> {} & Y <> {} implies
for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2;

::
::   Triples
::

definition let x1,x2,x3;
func [x1,x2,x3] equals
:: MCART_1:def 3
[[x1,x2],x3];
end;

canceled;

theorem :: MCART_1:28
[x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3;

theorem :: MCART_1:29
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];

::
::

definition let x1,x2,x3,x4;
func [x1,x2,x3,x4] equals
:: MCART_1:def 4
[[x1,x2,x3],x4];
end;

canceled;

theorem :: MCART_1:31
[x1,x2,x3,x4] = [[[x1,x2],x3],x4];

theorem :: MCART_1:32
[x1,x2,x3,x4] = [[x1,x2],x3,x4];

theorem :: MCART_1:33
[x1,x2,x3,x4] = [y1,y2,y3,y4] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4;

theorem :: MCART_1:34
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];

::
::   Cartesian products of three sets
::

theorem :: MCART_1:35
X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {};

reserve xx1 for Element of X1,
xx2 for Element of X2,
xx3 for Element of X3;

theorem :: MCART_1:36
X1<>{} & X2<>{} & X3<>{} implies
( [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3);

theorem :: MCART_1:37
[:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:]
implies X1=Y1 & X2=Y2 & X3=Y3;

theorem :: MCART_1:38
[:X,X,X:] = [:Y,Y,Y:] implies X = Y;

theorem :: MCART_1:39
[:{x1},{x2},{x3}:] = { [x1,x2,x3] };

theorem :: MCART_1:40
[:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] };

theorem :: MCART_1:41
[:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] };

theorem :: MCART_1:42
[:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] };

theorem :: MCART_1:43
[:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] };

theorem :: MCART_1:44
[:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] };

theorem :: MCART_1:45
[:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] };

theorem :: MCART_1:46
[:{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] };

definition let X1,X2,X3;
assume
X1<>{} & X2<>{} & X3<>{};
let x be Element of [:X1,X2,X3:];
func x`1 -> Element of X1 means
:: MCART_1:def 5
x = [x1,x2,x3] implies it = x1;
func x`2 -> Element of X2 means
:: MCART_1:def 6
x = [x1,x2,x3] implies it = x2;
func x`3 -> Element of X3 means
:: MCART_1:def 7
x = [x1,x2,x3] implies it = x3;
end;

theorem :: MCART_1:47
X1<>{} & X2<>{} & X3<>{} implies
for x being Element of [:X1,X2,X3:]
for x1,x2,x3 st x = [x1,x2,x3] holds
x`1 = x1 & x`2 = x2 & x`3 = x3;

theorem :: MCART_1:48
X1<>{} & X2<>{} & X3<>{} implies
for x being Element of [:X1,X2,X3:] holds x = [x`1,x`2,x`3];

theorem :: MCART_1:49
X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {};

theorem :: MCART_1:50
X1<>{} & X2<>{} & X3<>{} implies
for x being Element of [:X1,X2,X3:] holds
x`1 = (x qua set)`1`1 &
x`2 = (x qua set)`1`2 &
x`3 = (x qua set)`2;

theorem :: MCART_1:51
X1<>{} & X2<>{} & X3<>{} implies
for x being Element of [:X1,X2,X3:] holds
x <> x`1 & x <> x`2 & x <> x`3;

theorem :: MCART_1:52
[:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies
X1 meets Y1 & X2 meets Y2 & X3 meets Y3;

::
::   Cartesian products of four sets
::

theorem :: MCART_1:53
[:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:];

theorem :: MCART_1:54
[:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:];

theorem :: MCART_1:55
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {};

theorem :: MCART_1:56
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
( [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4);

theorem :: MCART_1:57
[:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:]
implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4;

theorem :: MCART_1:58
[:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y;

reserve xx4 for Element of X4;

definition let X1,X2,X3,X4;
assume
X1<>{} & X2<>{} & X3<>{} & X4 <> {};
let x be Element of [:X1,X2,X3,X4:];
func x`1 -> Element of X1 means
:: MCART_1:def 8
x = [x1,x2,x3,x4] implies it = x1;
func x`2 -> Element of X2 means
:: MCART_1:def 9
x = [x1,x2,x3,x4] implies it = x2;
func x`3 -> Element of X3 means
:: MCART_1:def 10
x = [x1,x2,x3,x4] implies it = x3;
func x`4 -> Element of X4 means
:: MCART_1:def 11
x = [x1,x2,x3,x4] implies it = x4;
end;

theorem :: MCART_1:59
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
for x being Element of [:X1,X2,X3,X4:]
for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds
x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4;

theorem :: MCART_1:60
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
for x being Element of [:X1,X2,X3,X4:] holds x = [x`1,x`2,x`3,x`4];

theorem :: MCART_1:61
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
for x being Element of [:X1,X2,X3,X4:] holds
x`1 = (x qua set)`1`1`1 &
x`2 = (x qua set)`1`1`2 &
x`3 = (x qua set)`1`2 &
x`4 = (x qua set)`2;

theorem :: MCART_1:62
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
for x being Element of [:X1,X2,X3,X4:] holds
x <> x`1 & x <> x`2 & x <> x`3 & x <> x`4;

theorem :: MCART_1:63
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 = {};

theorem :: MCART_1:64
[:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies
X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4;

theorem :: MCART_1:65
[:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] };

:: Ordered pairs

theorem :: MCART_1:66
[:X,Y:] <> {} implies
for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2;

theorem :: MCART_1:67
x in [:X,Y:] implies x <> x`1 & x <> x`2;

:: 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 :: MCART_1:68
X1<>{} & X2<>{} & X3<>{} implies
for x1,x2,x3 st x = [x1,x2,x3] holds x`1 = x1 & x`2 = x2 & x`3 = x3;

theorem :: MCART_1:69
X1<>{} & X2<>{} & X3<>{} &
(for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y1 = xx1) implies y1 =x`1;

theorem :: MCART_1:70
X1<>{} & X2<>{} & X3<>{} &
(for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y2 = xx2) implies y2 =x`2;

theorem :: MCART_1:71
X1<>{} & X2<>{} & X3<>{} &
(for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y3 = xx3) implies y3 =x`3;

theorem :: MCART_1:72
z in [: X1,X2,X3 :] implies
ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3];

theorem :: MCART_1:73
[x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3;

theorem :: MCART_1:74
(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 :];
theorem :: MCART_1:75
X1 <> {} & X2 <> {} & X3 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} implies
for x being (Element of [:X1,X2,X3:]), y being Element of [:Y1,Y2,Y3:]
holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3;

theorem :: MCART_1:76
for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:]
holds x`1 in A1 & x`2 in A2 & x`3 in A3;

theorem :: MCART_1:77
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,Y3:];

reserve x for Element of [:X1,X2,X3,X4:];

theorem :: MCART_1:78
X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
for x1,x2,x3,x4 st x = [x1,x2,x3,x4]
holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4;

theorem :: MCART_1:79
X1<>{} & X2<>{} & X3<>{} & X4<>{} &
(for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1)
implies y1 =x`1;

theorem :: MCART_1:80
X1<>{} & X2<>{} & X3<>{} & X4<>{} &
(for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y2 = xx2)
implies y2 =x`2;

theorem :: MCART_1:81
X1<>{} & X2<>{} & X3<>{} & X4<>{} &
(for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y3 = xx3)
implies y3 =x`3;

theorem :: MCART_1:82
X1<>{} & X2<>{} & X3<>{} & X4<>{} &
(for xx1,xx2,xx3,xx4 st x = [xx1,xx2,xx3,xx4] holds y4 = xx4)
implies y4 =x`4;

theorem :: MCART_1:83
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];

theorem :: MCART_1:84
[x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4
in
X4;

theorem :: MCART_1:85
(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 :];

theorem :: MCART_1:86
X1<>{} & X2<>{} & X3<>{} & X4<>{} & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} implies
for x being (Element of [:X1,X2,X3,X4:]), y being Element of [:Y1,Y2,Y3,Y4:]
holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4;

theorem :: MCART_1:87
for x being Element of [:X1,X2,X3,X4:] st x in [:A1,A2,A3,A4:]
holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4;

theorem :: MCART_1:88
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4
implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:];

definition let X1,X2,A1,A2;
redefine func [:A1,A2:] -> Subset of [:X1,X2:];
end;
definition let X1,X2,X3,A1,A2,A3;
redefine func [:A1,A2,A3:] -> Subset of [:X1,X2,X3:];
end;
definition let X1,X2,X3,X4,A1,A2,A3,A4;
redefine func [:A1,A2,A3,A4:] -> Subset of [:X1,X2,X3,X4:];
end;
```