The abstract of the Mizar article:

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

by

Michal Muzalewski, and

Wojciech Skaba

Received October 15, 1990

MML identifier: MCART_3

[ Mizar article, MML identifier index ]

environ

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


begin

  reserve v,z,x1,x2,x3,x4,x5,x6,y1,y2,y3,y4,y5,y6,
          X,X1,X2,X3,X4,X5,X6,Y,Y1,Y2,Y3,Y4,Y5,Y6,Y7,Y8,Y9,
          Z,Z1,Z2,Z3,Z4,Z5,Z6,Z7,Z8,Z9 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;

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

theorem :: MCART_3:2

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


::
::   Tuples for n=6
::


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

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


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


canceled;

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


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


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


theorem :: MCART_3:8

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


theorem :: MCART_3:9

 X <> {} implies
  ex v st v in X &
   not ex x1,x2,x3,x4,x5,x6 st (x1 in X or x2 in X) & v = [x1,x2,x3,x4,x5,x6];


::
::   Cartesian products of six sets
::


definition
  let X1,X2,X3,X4,X5,X6;

  func [:X1,X2,X3,X4,X5,X6:] -> set equals
:: MCART_3:def 2
    [:[: X1,X2,X3,X4,X5 :],X6 :];
end;


theorem :: MCART_3:10

 [:X1,X2,X3,X4,X5,X6:] = [:[:[:[:[:X1,X2:],X3:],X4:],X5:],X6:];


canceled;

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


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


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


theorem :: MCART_3:15
  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} & X5 <> {} & X6 <> {}
   iff [:X1,X2,X3,X4,X5,X6:] <> {};


theorem :: MCART_3:16

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


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


theorem :: MCART_3:18
    [:X,X,X,X,X,X:] = [:Y,Y,Y,Y,Y,Y:] implies X = Y;


 reserve xx6 for Element of X6;


theorem :: MCART_3:19

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


definition
  let X1,X2,X3,X4,X5,X6;

  assume
           X1<>{} & X2<>{} & X3<>{} & X4<>{} & X5<>{} & X6<>{};

 let x be Element of [:X1,X2,X3,X4,X5,X6:];

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

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

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

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

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

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

 end;


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


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


theorem :: MCART_3:22

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


theorem :: MCART_3:23
      X1 c= [:X1,X2,X3,X4,X5,X6:]
 or X1 c= [:X2,X3,X4,X5,X6,X1:]
 or X1 c= [:X3,X4,X5,X6,X1,X2:]
 or X1 c= [:X4,X5,X6,X1,X2,X3:]
 or X1 c= [:X5,X6,X1,X2,X3,X4:]
 or X1 c= [:X6,X1,X2,X3,X4,X5:]
 implies X1 = {};


theorem :: MCART_3:24
   [:X1,X2,X3,X4,X5,X6:] meets [:Y1,Y2,Y3,Y4,Y5,Y6:] implies
   X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4 & X5 meets Y5
 & X6 meets Y6;

theorem :: MCART_3:25
[:{x1},{x2},{x3},{x4},{x5},{x6}:] = { [x1,x2,x3,x4,x5,x6] };

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;

:: 6 - Tuples

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

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

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

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

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

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

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

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

theorem :: MCART_3:33
   z in [: X1,X2,X3,X4,X5,X6 :] implies
  ex x1,x2,x3,x4,x5,x6
  st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & x6 in X6
   & z = [x1,x2,x3,x4,x5,x6];

theorem :: MCART_3:34
       [x1,x2,x3,x4,x5,x6] in [: X1,X2,X3,X4,X5,X6 :]
 iff x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & x6 in X6;

theorem :: MCART_3:35
   (for z holds z in Z iff
  ex x1,x2,x3,x4,x5,x6
  st x1 in X1 & x2 in X2 & x3 in X3 & x4 in X4 & x5 in X5
   & x6 in X6
   & z = [x1,x2,x3,x4,x5,x6])
  implies Z = [: X1,X2,X3,X4,X5,X6 :];

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

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

theorem :: MCART_3:38
 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4 & X5 c= Y5 & X6 c= Y6
  implies [:X1,X2,X3,X4,X5,X6:] c= [:Y1,Y2,Y3,Y4,Y5,Y6:];

theorem :: MCART_3:39
    [:A1,A2,A3,A4,A5,A6:] is Subset of [:X1,X2,X3,X4,X5,X6:];