Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990 Association of Mizar Users

\$N\$-Tuples and Cartesian Products for \$n=8\$

by
Michal Muzalewski, and
Wojciech Skaba

Received October 15, 1990

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

```environ

vocabulary BOOLE, TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, MCART_2, MCART_3,
MCART_4;
constructors TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MEMBERED, XBOOLE_0;
clusters MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;

begin

reserve x1,x2,x3,x4,x5,x6,x7,x8 for set;
reserve y,y1,y2,y3,y4,y5,y6,y7,y8 for set;
reserve X,X1,X2,X3,X4,X5,X6,X7,X8 for set;
reserve Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD for set;
reserve Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9,ZA,ZB,ZC,ZD for set;
reserve xx1 for Element of X1;
reserve xx2 for Element of X2;
reserve xx3 for Element of X3;
reserve xx4 for Element of X4;
reserve xx5 for Element of X5;
reserve xx6 for Element of X6;
reserve xx7 for Element of X7;

theorem :: MCART_5:1
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in Y
holds Y1 misses X;

theorem :: MCART_5:2
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y8
& Y8 in Y9 & Y9 in YA & YA in YB & YB in YC & YC in YD & YD in Y
holds Y1 misses X;

::
::   Tuples for n=8
::

definition
let x1,x2,x3,x4,x5,x6,x7,x8;

func [x1,x2,x3,x4,x5,x6,x7,x8] equals
:: MCART_5:def 1
[[x1,x2,x3,x4,x5,x6,x7],x8];
end;

theorem :: MCART_5:3
[x1,x2,x3,x4,x5,x6,x7,x8] = [[[[[[[x1,x2],x3],x4],x5],x6],x7],x8];

canceled;

theorem :: MCART_5:5
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5,x6],x7,x8];

theorem :: MCART_5:6
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4,x5],x6,x7,x8];

theorem :: MCART_5:7
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3,x4],x5,x6,x7,x8];

theorem :: MCART_5:8
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2,x3],x4,x5,x6,x7,x8];

theorem :: MCART_5:9
[x1,x2,x3,x4,x5,x6,x7,x8] = [[x1,x2],x3,x4,x5,x6,x7,x8];

theorem :: MCART_5:10

[x1,x2,x3,x4,x5,x6,x7,x8] = [y1,y2,y3,y4,y5,y6,y7,y8]
implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6
& x7 = y7 & x8 = y8;

theorem :: MCART_5:11
X <> {} implies
ex y st y in X &
not ex x1,x2,x3,x4,x5,x6,x7,x8
st (x1 in X or x2 in X) & y = [x1,x2,x3,x4,x5,x6,x7,x8];

::
::   Cartesian products of eight sets
::

definition
let X1,X2,X3,X4,X5,X6,X7,X8;
func [:X1,X2,X3,X4,X5,X6,X7,X8:] -> set equals
:: MCART_5:def 2
[:[: X1,X2,X3,X4,X5,X6,X7 :],X8 :];
end;

theorem :: MCART_5:12
[:X1,X2,X3,X4,X5,X6,X7,X8:] =
[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:];

canceled;

theorem :: MCART_5:14
[:X1,X2,X3,X4,X5,X6,X7,X8:]
= [:[:X1,X2,X3,X4,X5,X6:],X7,X8:];

theorem :: MCART_5:15
[:X1,X2,X3,X4,X5,X6,X7,X8:]
= [:[:X1,X2,X3,X4,X5:],X6,X7,X8:];

theorem :: MCART_5:16
[:X1,X2,X3,X4,X5,X6,X7,X8:]
= [:[:X1,X2,X3,X4:],X5,X6,X7,X8:];

theorem :: MCART_5:17
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8:];

theorem :: MCART_5:18
[:X1,X2,X3,X4,X5,X6,X7,X8:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8:];

theorem :: MCART_5:19
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {}
& X7 <> {} & X8 <> {}
iff [:X1,X2,X3,X4,X5,X6,X7,X8:] <> {};

theorem :: MCART_5:20

X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies
( [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]
implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8);

theorem :: MCART_5:21
[:X1,X2,X3,X4,X5,X6,X7,X8:]<>{}
& [:X1,X2,X3,X4,X5,X6,X7,X8:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]
implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8;

theorem :: MCART_5:22
[:X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y:] implies X = Y;

reserve xx8 for Element of X8;

theorem :: MCART_5:23
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
ex xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8];

definition
let X1,X2,X3,X4,X5,X6,X7,X8;
assume  X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{}
& X8<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8:];
func x`1 -> Element of X1 means
:: MCART_5:def 3
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x1;

func x`2 -> Element of X2 means
:: MCART_5:def 4
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x2;

func x`3 -> Element of X3 means
:: MCART_5:def 5
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x3;

func x`4 -> Element of X4 means
:: MCART_5:def 6
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x4;

func x`5 -> Element of X5 means
:: MCART_5:def 7
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x5;

func x`6 -> Element of X6 means
:: MCART_5:def 8
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x6;

func x`7 -> Element of X7 means
:: MCART_5:def 9
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x7;

func x`8 -> Element of X8 means
:: MCART_5:def 10
x = [x1,x2,x3,x4,x5,x6,x7,x8] implies it = x8;
end;

theorem :: MCART_5:24
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
for x1,x2,x3,x4,x5,x6,x7,x8
st x = [x1,x2,x3,x4,x5,x6,x7,x8] holds
x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5 & x`6 = x6
& x`7 = x7 & x`8 =x8;

theorem :: MCART_5:25
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
holds x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8];

theorem :: MCART_5:26
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:] holds
x`1 = (x qua set)`1`1`1`1`1`1`1 &
x`2 = (x qua set)`1`1`1`1`1`1`2 &
x`3 = (x qua set)`1`1`1`1`1`2 &
x`4 = (x qua set)`1`1`1`1`2 &
x`5 = (x qua set)`1`1`1`2 &
x`6 = (x qua set)`1`1`2 &
x`7 = (x qua set)`1`2 &
x`8 = (x qua set)`2;

theorem :: MCART_5:27
X1 c= [:X1,X2,X3,X4,X5,X6,X7,X8:]
or X1 c= [:X2,X3,X4,X5,X6,X7,X8,X1:]
or X1 c= [:X3,X4,X5,X6,X7,X8,X1,X2:]
or X1 c= [:X4,X5,X6,X7,X8,X1,X2,X3:]
or X1 c= [:X5,X6,X7,X8,X1,X2,X3,X4:]
or X1 c= [:X6,X7,X8,X1,X2,X3,X4,X5:]
or X1 c= [:X7,X8,X1,X2,X3,X4,X5,X6:]
or X1 c= [:X8,X1,X2,X3,X4,X5,X6,X7:]
implies X1 = {};

theorem :: MCART_5:28
[:X1,X2,X3,X4,X5,X6,X7,X8:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:] implies
X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5
& X6 meets Y6 & X7 meets Y7 &X8 meets Y8;

theorem :: MCART_5:29
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8}:]
= { [x1,x2,x3,x4,x5,x6,x7,x8] };

reserve A1 for Subset of X1,
A2 for Subset of X2,
A3 for Subset of X3,
A4 for Subset of X4,
A5 for Subset of X5,
A6 for Subset of X6,
A7 for Subset of X7,
A8 for Subset of X8;

:: 8 - Tuples

reserve x for Element of [:X1,X2,X3,X4,X5,X6,X7,X8:];

theorem :: MCART_5:30
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
implies
for x1,x2,x3,x4,x5,x6,x7,x8 st x = [x1,x2,x3,x4,x5,x6,x7,x8]
holds x`1 = x1 & x`2 = x2 & x`3 = x3 & x`4 = x4 & x`5 = x5
& x`6 = x6 & x`7 = x7 & x`8 = x8;

theorem :: MCART_5:31
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y1 = xx1)
implies y1 =x`1;

theorem :: MCART_5:32
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y2 = xx2)
implies y2 =x`2;

theorem :: MCART_5:33
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y3 = xx3)
implies y3 =x`3;

theorem :: MCART_5:34
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y4 = xx4)
implies y4 =x`4;

theorem :: MCART_5:35
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y5 = xx5)
implies y5 =x`5;

theorem :: MCART_5:36
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y6 = xx6)
implies y6 =x`6;

theorem :: MCART_5:37
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y7 = xx7)
implies y7 =x`7;

theorem :: MCART_5:38
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} &
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8] holds y8 = xx8)
implies y8 =x`8;

theorem :: MCART_5:39
y in [: X1,X2,X3,X4,X5,X6,X7,X8 :] implies
ex x1,x2,x3,x4,x5,x6,x7,x8
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8
& y = [x1,x2,x3,x4,x5,x6,x7,x8];

theorem :: MCART_5:40
[x1,x2,x3,x4,x5,x6,x7,x8] in [: X1,X2,X3,X4,X5,X6,X7,X8 :]
iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8;

theorem :: MCART_5:41
(for y holds y in Z iff
ex x1,x2,x3,x4,x5,x6,x7,x8
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& x6 in X6 & x7 in X7 & x8 in X8
& y = [x1,x2,x3,x4,x5,x6,x7,x8])
implies Z = [: X1,X2,X3,X4,X5,X6,X7,X8 :];

theorem :: MCART_5:42
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:],
y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:]
holds x = y
implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5
& x`6 = y`6 & x`7 = y`7 & x`8 = y`8;

theorem :: MCART_5:43
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8:]
st x in [:A1,A2,A3,A4,A5,A6,A7,A8:]
holds x`1 in A1 & x`2 in A2 & x`3 in A3 & x`4 in A4 & x`5 in A5
& x`6 in A6 & x`7 in A7 & x`8 in A8;

theorem :: MCART_5:44
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7
& X8 c= Y8
implies [:X1,X2,X3,X4,X5,X6,X7,X8:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8:];

theorem :: MCART_5:45
[:A1,A2,A3,A4,A5,A6,A7,A8:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8:]
;

```