Journal of Formalized Mathematics
Volume 2, 1990
University of Bialystok
Copyright (c) 1990
Association of Mizar Users
The abstract of the Mizar article:
-
- by
- Michal Muzalewski,
and
- Wojciech Skaba
- Received October 15, 1990
- MML identifier: MCART_6
- [
Mizar article,
MML identifier index
]
environ
vocabulary BOOLE, TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5,
MCART_6;
notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, MCART_1, MCART_2, MCART_3,
MCART_4, MCART_5;
constructors TARSKI, MCART_1, MCART_2, MCART_3, MCART_4, MCART_5, MEMBERED,
XBOOLE_0;
clusters MEMBERED, ZFMISC_1, XBOOLE_0;
requirements SUBSET, BOOLE;
begin
reserve x1,x2,x3,x4,x5,x6,x7,x8,x9 for set;
reserve y,y1,y2,y3,y4,y5,y6,y7,y8,y9 for set;
reserve X,X1,X2,X3,X4,X5,X6,X7,X8,X9 for set;
reserve Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE,YF for set;
reserve Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9,ZA,ZB,ZC,ZD,ZE,ZF 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;
reserve xx8 for Element of X8;
theorem :: MCART_6:1
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE
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 YE & YE
in Y
holds Y1 misses X;
theorem :: MCART_6:2
X <> {} implies
ex Y st Y in X &
for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB,YC,YD,YE,YF
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 YE & YE
in YF
& YF in Y
holds Y1 misses X;
::
:: Tuples for n=9
::
definition
let x1,x2,x3,x4,x5,x6,x7,x8,x9;
func [x1,x2,x3,x4,x5,x6,x7,x8,x9] equals
:: MCART_6:def 1
[[x1,x2,x3,x4,x5,x6,x7,x8],x9];
end;
theorem :: MCART_6:3
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[[[[[[[x1,x2],x3],x4],x5],x6],x7],x8],x9];
canceled;
theorem :: MCART_6:5
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6,x7],x8,x9];
theorem :: MCART_6:6
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5,x6],x7,x8,x9];
theorem :: MCART_6:7
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4,x5],x6,x7,x8,x9];
theorem :: MCART_6:8
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3,x4],x5,x6,x7,x8,x9];
theorem :: MCART_6:9
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2,x3],x4,x5,x6,x7,x8,x9];
theorem :: MCART_6:10
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [[x1,x2],x3,x4,x5,x6,x7,x8,x9];
theorem :: MCART_6:11
[x1,x2,x3,x4,x5,x6,x7,x8,x9] = [y1,y2,y3,y4,y5,y6,y7,y8,y9]
implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6
& x7 = y7 & x8 = y8 & x9 =y9;
::
:: Cartesian products of nine sets
::
definition
let X1,X2,X3,X4,X5,X6,X7,X8,X9;
func [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] -> set equals
:: MCART_6:def 2
[:[: X1,X2,X3,X4,X5,X6,X7,X8 :],X9 :];
end;
theorem :: MCART_6:12
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] =
[:[:[:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:],X8:],X9:];
canceled;
theorem :: MCART_6:14
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
= [:[:X1,X2,X3,X4,X5,X6,X7:],X8,X9:];
theorem :: MCART_6:15
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
= [:[:X1,X2,X3,X4,X5,X6:],X7,X8,X9:];
theorem :: MCART_6:16
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
= [:[:X1,X2,X3,X4,X5:],X6,X7,X8,X9:];
theorem :: MCART_6:17
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3,X4:],X5,X6,X7,X8,X9:];
theorem :: MCART_6:18
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2,X3:],X4,X5,X6,X7,X8,X9:];
theorem :: MCART_6:19
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:[:X1,X2:],X3,X4,X5,X6,X7,X8,X9:];
theorem :: MCART_6:20
X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {}
& X7 <> {} & X8 <> {} & X9 <> {}
iff [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] <> {};
theorem :: MCART_6:21
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
( [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
implies
X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8 & X9=Y9);
theorem :: MCART_6:22
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:]<>{}
& [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] = [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
implies
X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4 & X5=Y5 & X6=Y6 & X7=Y7 & X8=Y8 & X9=Y9;
theorem :: MCART_6:23
[:X,X,X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y,Y,Y:] implies X = Y;
reserve xx9 for Element of X9;
theorem :: MCART_6:24
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
ex xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9];
definition
let X1,X2,X3,X4,X5,X6,X7,X8,X9;
assume
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{}
& X9<>{};
let x be Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
func x`1 -> Element of X1 means
:: MCART_6:def 3
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x1;
func x`2 -> Element of X2 means
:: MCART_6:def 4
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x2;
func x`3 -> Element of X3 means
:: MCART_6:def 5
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x3;
func x`4 -> Element of X4 means
:: MCART_6:def 6
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x4;
func x`5 -> Element of X5 means
:: MCART_6:def 7
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x5;
func x`6 -> Element of X6 means
:: MCART_6:def 8
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x6;
func x`7 -> Element of X7 means
:: MCART_6:def 9
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x7;
func x`8 -> Element of X8 means
:: MCART_6:def 10
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x8;
func x`9 -> Element of X9 means
:: MCART_6:def 11
x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] implies it = x9;
end;
theorem :: MCART_6:25
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
for x1,x2,x3,x4,x5,x6,x7,x8,x9
st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9] 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 & x`9 = x9;
theorem :: MCART_6:26
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
holds x = [x`1,x`2,x`3,x`4,x`5,x`6,x`7,x`8,x`9];
theorem :: MCART_6:27
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>{}
implies
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] holds
x`1 = (x qua set)`1`1`1`1`1`1`1`1 &
x`2 = (x qua set)`1`1`1`1`1`1`1`2 &
x`3 = (x qua set)`1`1`1`1`1`1`2 &
x`4 = (x qua set)`1`1`1`1`1`2 &
x`5 = (x qua set)`1`1`1`1`2 &
x`6 = (x qua set)`1`1`1`2 &
x`7 = (x qua set)`1`1`2 &
x`8 = (x qua set)`1`2 &
x`9 = (x qua set)`2;
theorem :: MCART_6:28
[:X1,X2,X3,X4,X5,X6,X7,X8,X9:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:] 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 & X9 meets Y9;
theorem :: MCART_6:29
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7},{x8},{x9}:]
= { [x1,x2,x3,x4,x5,x6,x7,x8,x9] };
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,
A9 for Subset of X9;
:: 9 - Tuples
reserve x for Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
theorem :: MCART_6:30
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
implies
for x1,x2,x3,x4,x5,x6,x7,x8,x9 st x = [x1,x2,x3,x4,x5,x6,x7,x8,x9]
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 & x`9 = x9;
theorem :: MCART_6:31
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y1 = xx1)
implies y1 =x`1;
theorem :: MCART_6:32
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y2 = xx2)
implies y2 =x`2;
theorem :: MCART_6:33
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y3 = xx3)
implies y3 =x`3;
theorem :: MCART_6:34
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y4 = xx4)
implies y4 =x`4;
theorem :: MCART_6:35
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y5 = xx5)
implies y5 =x`5;
theorem :: MCART_6:36
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y6 = xx6)
implies y6 =x`6;
theorem :: MCART_6:37
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y7 = xx7)
implies y7 =x`7;
theorem :: MCART_6:38
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y8 = xx8)
implies y8 =x`8;
theorem :: MCART_6:39
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
&
(for xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9
st x = [xx1,xx2,xx3,xx4,xx5,xx6,xx7,xx8,xx9] holds y9 = xx9)
implies y9 =x`9;
theorem :: MCART_6:40
y in [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :] implies
ex x1,x2,x3,x4,x5,x6,x7,x8,x9
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 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9];
theorem :: MCART_6:41
[x1,x2,x3,x4,x5,x6,x7,x8,x9] in [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :]
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 & x9 in X9;
theorem :: MCART_6:42
(for y holds y in Z iff
ex x1,x2,x3,x4,x5,x6,x7,x8,x9
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 & x9 in X9
& y = [x1,x2,x3,x4,x5,x6,x7,x8,x9])
implies Z = [: X1,X2,X3,X4,X5,X6,X7,X8,X9 :];
theorem :: MCART_6:43
X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{} & X8<>{} & X9<>
{}
& Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} & Y8<>{} & Y9<>
{}
implies
for x being (Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]),
y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:]
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 & x`9 = y`9;
theorem :: MCART_6:44
for x being Element of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:]
st x in [:A1,A2,A3,A4,A5,A6,A7,A8,A9:]
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 & x`9 in A9;
theorem :: MCART_6:45
X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6 & X7 c= Y7
& X8 c= Y8 & X9 c= Y9
implies [:X1,X2,X3,X4,X5,X6,X7,X8,X9:] c= [:Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9:];
theorem :: MCART_6:46
[:A1,A2,A3,A4,A5,A6,A7,A8,A9:] is Subset of [:X1,X2,X3,X4,X5,X6,X7,X8,X9:];
Back to top