The abstract of the Mizar article:

$N$-Tuples and Cartesian Products for $n=7$

by

Michal Muzalewski, and

Wojciech Skaba

Received October 15, 1990

MML identifier: MCART_4

[ Mizar article, MML identifier index ]

environ

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


begin

  reserve x,x1,x2,x3,x4,x5,x6,x7 for set;
  reserve y,y1,y2,y3,y4,y5,y6,y7 for set;
  reserve X,X1,X2,X3,X4,X5,X6,X7 for set;
  reserve Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB for set;
  reserve Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9,ZA,ZB 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;

theorem :: MCART_4:1
   X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA
    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 Y
        holds Y1 misses X;

theorem :: MCART_4:2
 X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,YA,YB
    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 Y
        holds Y1 misses X;

::
::   Tuples for n=7
::

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

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

canceled;

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

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

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

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

theorem :: MCART_4:9
  [x1,x2,x3,x4,x5,x6,x7] = [y1,y2,y3,y4,y5,y6,y7]
  implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4 & x5 = y5 & x6 = y6
        & x7 = y7;

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

::
::   Cartesian products of seven sets
::

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

theorem :: MCART_4:11
 [:X1,X2,X3,X4,X5,X6,X7:] = [:[:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:],X7:];

canceled;

theorem :: MCART_4:13
   [:X1,X2,X3,X4,X5,X6,X7:] = [:[:X1,X2,X3,X4,X5:],X6,X7:];

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

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

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

theorem :: MCART_4:17
  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {}
     & X7 <> {}
   iff [:X1,X2,X3,X4,X5,X6,X7:] <> {};

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

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

theorem :: MCART_4:20
    [:X,X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y,Y:] implies X = Y;

 reserve xx7 for Element of X7;

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


definition
  let X1,X2,X3,X4,X5,X6,X7;
  assume  X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{};
  let x be Element of [:X1,X2,X3,X4,X5,X6,X7:];

  func x`1 -> Element of X1 means
:: MCART_4:def 3
 x = [x1,x2,x3,x4,x5,x6,x7] implies it = x1;

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

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

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

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

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

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

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

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

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

theorem :: MCART_4:25
      X1 c= [:X1,X2,X3,X4,X5,X6,X7:]
 or X1 c= [:X2,X3,X4,X5,X6,X7,X1:]
 or X1 c= [:X3,X4,X5,X6,X7,X1,X2:]
 or X1 c= [:X4,X5,X6,X7,X1,X2,X3:]
 or X1 c= [:X5,X6,X7,X1,X2,X3,X4:]
 or X1 c= [:X6,X7,X1,X2,X3,X4,X5:]
 or X1 c= [:X7,X1,X2,X3,X4,X5,X6:]
 implies X1 = {};

theorem :: MCART_4:26
   [:X1,X2,X3,X4,X5,X6,X7:] meets [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:] implies
   X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5
 & X6 meets Y6 & X7 meets Y7;

theorem :: MCART_4:27
[:{x1},{x2},{x3},{x4},{x5},{x6},{x7}:]
      = { [x1,x2,x3,x4,x5,x6,x7] };

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;

:: 7 - Tuples

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

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

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

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

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

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

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

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

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

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

theorem :: MCART_4:37
       [x1,x2,x3,x4,x5,x6,x7] in [: X1,X2,X3,X4,X5,X6,X7 :]
 iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & x6 in X6 & x7 in X7;

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

theorem :: MCART_4:39
   X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{} & X7<>{}
 & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} & Y5<>{} & Y6<>{} & Y7<>{} implies
  for x being (Element of [:X1,X2,X3,X4,X5,X6,X7:]),
      y being Element of [:Y1,Y2,Y3,Y4,Y5,Y6,Y7:]
  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;

theorem :: MCART_4:40
   for x being Element of [:X1,X2,X3,X4,X5,X6,X7:]
      st x in [:A1,A2,A3,A4,A5,A6,A7:]
   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;

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

theorem :: MCART_4:42
    [:A1,A2,A3,A4,A5,A6,A7:] is Subset of [:X1,X2,X3,X4,X5,X6,X7:];