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

### \$N\$-Tuples and Cartesian Products for \$n=5\$

by
Michal Muzalewski, and
Wojciech Skaba

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

```environ

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

begin

reserve x,x1,x2,x3,x4,x5, y,y1,y2,y3,y4,y5,
X,X1,X2,X3,X4,X5, Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,
Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7 for set;
reserve xx1 for Element of X1, xx2 for Element of X2,
xx3 for Element of X3, xx4 for Element of X4,
xx5 for Element of X5;

theorem :: MCART_2:1
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y
holds Y1 misses X;

theorem :: MCART_2:2

X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7
st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in Y5 & Y5 in Y6 & Y6 in Y7 & Y7 in
Y
holds Y1 misses X;

::
::   Tuples for n=5
::

definition
let x1,x2,x3,x4,x5;
func [x1,x2,x3,x4,x5] equals
:: MCART_2:def 1
[[x1,x2,x3,x4],x5];
end;

theorem :: MCART_2:3
[x1,x2,x3,x4,x5] = [[[[x1,x2],x3],x4],x5];

canceled;

theorem :: MCART_2:5
[x1,x2,x3,x4,x5] = [[x1,x2,x3],x4,x5];

theorem :: MCART_2:6
[x1,x2,x3,x4,x5] = [[x1,x2],x3,x4,x5];

theorem :: MCART_2:7
[x1,x2,x3,x4,x5] = [y1,y2,y3,y4,y5]
implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5;

theorem :: MCART_2:8
X <> {} implies
ex x st x in X &
not ex x1,x2,x3,x4,x5 st (x1 in X or x2 in X) & x = [x1,x2,x3,x4,x5];

::
::   Cartesian products of five sets
::

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

theorem :: MCART_2:9
[:X1,X2,X3,X4,X5:] = [:[:[:[:X1,X2:],X3:],X4:],X5:];

canceled;

theorem :: MCART_2:11
[:X1,X2,X3,X4,X5:] = [:[:X1,X2,X3:],X4,X5:];

theorem :: MCART_2:12
[:X1,X2,X3,X4,X5:] = [:[:X1,X2:],X3,X4,X5:];

theorem :: MCART_2:13
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {}
iff [:X1,X2,X3,X4,X5:] <> {};

theorem :: MCART_2:14
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} implies
( [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:]
implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 );

theorem :: MCART_2:15
[:X1,X2,X3,X4,X5:]<>{} & [:X1,X2,X3,X4,X5:] = [:Y1,Y2,Y3,Y4,Y5:]
implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5;

theorem :: MCART_2:16
[:X,X,X,X,X:] = [:Y,Y,Y,Y,Y:] implies X = Y;

theorem :: MCART_2:17
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} implies
for x being Element of [:X1,X2,X3,X4,X5:]
ex xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5];

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

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

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

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

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

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

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

theorem :: MCART_2:20

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

theorem :: MCART_2:21
X1 c= [:X1,X2,X3,X4,X5:]
or X1 c= [:X2,X3,X4,X5,X1:]
or X1 c= [:X3,X4,X5,X1,X2:]
or X1 c= [:X4,X5,X1,X2,X3:]
or X1 c= [:X5,X1,X2,X3,X4:]
implies X1 = {};

theorem :: MCART_2:22
[:X1,X2,X3,X4,X5:] meets [:Y1,Y2,Y3,Y4,Y5:] implies
X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5;

theorem :: MCART_2:23
[:{x1},{x2},{x3},{x4},{x5}:] = { [x1,x2,x3,x4,x5] };

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;

:: 5 - Tuples

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

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

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

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

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

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

theorem :: MCART_2:29
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} &
(for xx1,xx2,xx3,xx4,xx5 st x = [xx1,xx2,xx3,xx4,xx5] holds y5 = xx5)
implies y5 =x`5;

theorem :: MCART_2:30
y in [: X1,X2,X3,X4,X5 :] implies
ex x1,x2,x3,x4,x5
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& y = [x1,x2,x3,x4,x5];

theorem :: MCART_2:31
[x1,x2,x3,x4,x5] in [: X1,X2,X3,X4,X5 :]
iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5;

theorem :: MCART_2:32
(for y holds y in Z iff
ex x1,x2,x3,x4,x5
st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
& y = [x1,x2,x3,x4,x5])
implies Z = [: X1,X2,X3,X4,X5 :];

theorem :: MCART_2:33
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{}
& Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} implies
for x being Element of [:X1,X2,X3,X4,X5:],
y being Element of [:Y1,Y2,Y3,Y4,Y5:]
holds x = y
implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4 & x`5 = y`5;

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

theorem :: MCART_2:35
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5
implies [:X1,X2,X3,X4,X5:] c= [:Y1,Y2,Y3,Y4,Y5:];

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

theorem :: MCART_2:36
X1 <> {} & X2 <> {} implies
for xx being Element of [:X1,X2:]
ex xx1 being (Element of X1),
xx2 being Element of X2 st xx = [xx1,xx2];

theorem :: MCART_2:37
X1 <> {} & X2 <> {} & X3 <> {} implies
for xx being Element of [:X1,X2,X3:]
ex xx1,xx2,xx3 st xx = [xx1,xx2,xx3];

theorem :: MCART_2:38
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} implies
for xx being Element of [:X1,X2,X3,X4:]
ex xx1,xx2,xx3,xx4 st xx = [xx1,xx2,xx3,xx4];

```