The abstract of the Mizar article:

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

by

Michal Muzalewski, and

Wojciech Skaba

Received October 13, 1990

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];