The abstract of the Mizar article:

Tuples, Projections and Cartesian Products

by

Andrzej Trybulec

Received March 30, 1989

MML identifier: MCART_1

[ Mizar article, MML identifier index ]

environ

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


begin

  reserve v,x,x1,x2,x3,x4,y,y1,y2,y3,y4,z,z1,z2 for set,
            X,X1,X2,X3,X4,Y,Y1,Y2,Y3,Y4,Y5,Z,Z1,Z2,Z3,Z4,Z5 for set;

::
::   Regularity
::

:: We start with some auxiliary theorems related to the regularity axiom.
:: We need them to prove theorems below. Nevertheless they are
:: marked as theorems because they seem to be of general interest.

theorem :: MCART_1:1
 X <> {} implies ex Y st Y in X & Y misses X;

theorem :: MCART_1:2
 X <> {} implies ex Y st Y in X & for Y1 st Y1 in Y holds Y1 misses X;

theorem :: MCART_1:3
   X <> {} implies
  ex Y st Y in X & for Y1,Y2 st Y1 in Y2 & Y2 in Y holds Y1 misses X;

theorem :: MCART_1:4
 X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3 st Y1 in Y2 & Y2 in Y3 & Y3 in Y holds Y1 misses X;

theorem :: MCART_1:5
   X <> {} implies
  ex Y st Y in X &
   for Y1,Y2,Y3,Y4 st Y1 in Y2 & Y2 in Y3 & Y3 in Y4 & Y4 in
 Y holds Y1 misses X;

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

::
::   Ordered pairs
::

::  Now we introduce the projections of ordered pairs (functions that assign
::  to an ordered pair its first and its second element). The definitions
::  are permissive, function are defined for an arbitrary object. If it is not
::  an ordered pair, they are of course meaningless.


 definition let x;
  given x1,x2 being set such that
 x = [x1,x2];
  func x`1 means
:: MCART_1:def 1
 x = [y1,y2] implies it = y1;
  func x`2 means
:: MCART_1:def 2
 x = [y1,y2] implies it = y2;
 end;

theorem :: MCART_1:7
  [x,y]`1=x & [x,y]`2=y;

theorem :: MCART_1:8
   (ex x,y st z=[x,y]) implies [z`1,z`2] =z;

theorem :: MCART_1:9
   X <> {} implies
  ex v st v in X & not ex x,y st (x in X or y in X) & v = [x,y];

:: Now we prove theorems describing relationships between projections
:: of ordered pairs and Cartesian products of two sets.

theorem :: MCART_1:10
   z in [:X,Y:] implies z`1 in X & z`2 in Y;

theorem :: MCART_1:11
     (ex x,y st z=[x,y]) & z`1 in X & z`2 in Y implies z in [:X,Y:];

theorem :: MCART_1:12
    z in [:{x},Y:] implies z`1=x & z`2 in Y;

theorem :: MCART_1:13
    z in [:X,{y}:] implies z`1 in X & z`2 = y;

theorem :: MCART_1:14
    z in [:{x},{y}:] implies z`1 = x & z`2 = y;

theorem :: MCART_1:15
    z in [:{x1,x2},Y:] implies (z`1=x1 or z`1=x2) & z`2 in Y;

theorem :: MCART_1:16
    z in [:X,{y1,y2}:] implies z`1 in X & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:17
    z in [:{x1,x2},{y}:] implies (z`1=x1 or z`1=x2) & z`2 = y;

theorem :: MCART_1:18
    z in [:{x},{y1,y2}:] implies z`1 = x & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:19
    z in [:{x1,x2},{y1,y2}:] implies
       (z`1 = x1 or z`1 = x2) & (z`2 = y1 or z`2 = y2);

theorem :: MCART_1:20
 (ex y,z st x = [y,z]) implies x <> x`1 & x <> x`2;

:: Some of theorems proved above may be simplified , if we state them
:: for elements of Cartesian product rather than for arbitrary objects.

canceled 2;

theorem :: MCART_1:23
  x in [:X,Y:] implies x = [x`1,x`2];

theorem :: MCART_1:24
 X <> {} & Y <> {} implies
  for x being Element of [:X,Y:] holds x = [x`1,x`2];

theorem :: MCART_1:25
 [:{x1,x2},{y1,y2}:] = {[x1,y1],[x1,y2],[x2,y1],[x2,y2]};

theorem :: MCART_1:26
X <> {} & Y <> {} implies
 for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2;

::
::   Triples
::

definition let x1,x2,x3;
 func [x1,x2,x3] equals
:: MCART_1:def 3
  [[x1,x2],x3];
end;

canceled;

theorem :: MCART_1:28
 [x1,x2,x3] = [y1,y2,y3] implies x1 = y1 & x2 = y2 & x3 = y3;

theorem :: MCART_1:29
 X <> {} implies
  ex v st v in X & not ex x,y,z st (x in X or y in X) & v = [x,y,z];

::
::   Quadruples
::

definition let x1,x2,x3,x4;
 func [x1,x2,x3,x4] equals
:: MCART_1:def 4
  [[x1,x2,x3],x4];
end;

canceled;

theorem :: MCART_1:31
 [x1,x2,x3,x4] = [[[x1,x2],x3],x4];

theorem :: MCART_1:32
 [x1,x2,x3,x4] = [[x1,x2],x3,x4];

theorem :: MCART_1:33
 [x1,x2,x3,x4] = [y1,y2,y3,y4] implies x1 = y1 & x2 = y2 & x3 = y3 & x4 = y4;

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

::
::   Cartesian products of three sets
::

theorem :: MCART_1:35
 X1 <> {} & X2 <> {} & X3 <> {} iff [:X1,X2,X3:] <> {};

 reserve xx1 for Element of X1,
         xx2 for Element of X2,
         xx3 for Element of X3;

theorem :: MCART_1:36
 X1<>{} & X2<>{} & X3<>{} implies
  ( [:X1,X2,X3:] = [:Y1,Y2,Y3:] implies X1=Y1 & X2=Y2 & X3=Y3);

theorem :: MCART_1:37
   [:X1,X2,X3:]<>{} & [:X1,X2,X3:] = [:Y1,Y2,Y3:]
   implies X1=Y1 & X2=Y2 & X3=Y3;

theorem :: MCART_1:38
[:X,X,X:] = [:Y,Y,Y:] implies X = Y;

theorem :: MCART_1:39
[:{x1},{x2},{x3}:] = { [x1,x2,x3] };

theorem :: MCART_1:40
[:{x1,y1},{x2},{x3}:] = { [x1,x2,x3],[y1,x2,x3] };

theorem :: MCART_1:41
[:{x1},{x2,y2},{x3}:] = { [x1,x2,x3],[x1,y2,x3] };

theorem :: MCART_1:42
[:{x1},{x2},{x3,y3}:] = { [x1,x2,x3],[x1,x2,y3] };

theorem :: MCART_1:43
   [:{x1,y1},{x2,y2},{x3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,y2,x3],[y1,y2,x3] };

theorem :: MCART_1:44
   [:{x1,y1},{x2},{x3,y3}:] = { [x1,x2,x3],[y1,x2,x3],[x1,x2,y3],[y1,x2,y3] };

theorem :: MCART_1:45
   [:{x1},{x2,y2},{x3,y3}:] = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3] };

theorem :: MCART_1:46
   [:{x1,y1},{x2,y2},{x3,y3}:]
  = { [x1,x2,x3],[x1,y2,x3],[x1,x2,y3],[x1,y2,y3],
      [y1,x2,x3],[y1,y2,x3],[y1,x2,y3],[y1,y2,y3] };

definition let X1,X2,X3;
 assume
  X1<>{} & X2<>{} & X3<>{};
 let x be Element of [:X1,X2,X3:];
  func x`1 -> Element of X1 means
:: MCART_1:def 5
 x = [x1,x2,x3] implies it = x1;
  func x`2 -> Element of X2 means
:: MCART_1:def 6
 x = [x1,x2,x3] implies it = x2;
  func x`3 -> Element of X3 means
:: MCART_1:def 7
 x = [x1,x2,x3] implies it = x3;
end;

theorem :: MCART_1:47
  X1<>{} & X2<>{} & X3<>{} implies
 for x being Element of [:X1,X2,X3:]
  for x1,x2,x3 st x = [x1,x2,x3] holds
     x`1 = x1 & x`2 = x2 & x`3 = x3;

theorem :: MCART_1:48
 X1<>{} & X2<>{} & X3<>{} implies
 for x being Element of [:X1,X2,X3:] holds x = [x`1,x`2,x`3];

theorem :: MCART_1:49
 X c= [:X,Y,Z:] or X c= [:Y,Z,X:] or X c= [:Z,X,Y:] implies X = {};

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

theorem :: MCART_1:51
 X1<>{} & X2<>{} & X3<>{} implies
 for x being Element of [:X1,X2,X3:] holds
  x <> x`1 & x <> x`2 & x <> x`3;

theorem :: MCART_1:52
   [:X1,X2,X3:] meets [:Y1,Y2,Y3:] implies
   X1 meets Y1 & X2 meets Y2 & X3 meets Y3;

::
::   Cartesian products of four sets
::

theorem :: MCART_1:53
 [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:];

theorem :: MCART_1:54
 [:[:X1,X2:],X3,X4:] = [:X1,X2,X3,X4:];

theorem :: MCART_1:55
  X1 <> {} & X2 <> {} & X3 <> {} & X4 <> {} iff [:X1,X2,X3,X4:] <> {};

theorem :: MCART_1:56
 X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
  ( [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:] implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4);

theorem :: MCART_1:57
   [:X1,X2,X3,X4:]<>{} & [:X1,X2,X3,X4:] = [:Y1,Y2,Y3,Y4:]
   implies X1=Y1 & X2=Y2 & X3=Y3 & X4=Y4;

theorem :: MCART_1:58
[:X,X,X,X:] = [:Y,Y,Y,Y:] implies X = Y;

 reserve xx4 for Element of X4;

definition let X1,X2,X3,X4;
 assume
  X1<>{} & X2<>{} & X3<>{} & X4 <> {};
 let x be Element of [:X1,X2,X3,X4:];
  func x`1 -> Element of X1 means
:: MCART_1:def 8
 x = [x1,x2,x3,x4] implies it = x1;
  func x`2 -> Element of X2 means
:: MCART_1:def 9
 x = [x1,x2,x3,x4] implies it = x2;
  func x`3 -> Element of X3 means
:: MCART_1:def 10
 x = [x1,x2,x3,x4] implies it = x3;
  func x`4 -> Element of X4 means
:: MCART_1:def 11
 x = [x1,x2,x3,x4] implies it = x4;
 end;

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

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

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

theorem :: MCART_1:62
   X1<>{} & X2<>{} & X3<>{} & X4<>{} implies
 for x being Element of [:X1,X2,X3,X4:] holds
  x <> x`1 & x <> x`2 & x <> x`3 & x <> x`4;

theorem :: MCART_1:63
   X1 c= [:X1,X2,X3,X4:] or X1 c= [:X2,X3,X4,X1:]
  or X1 c= [:X3,X4,X1,X2:] or X1 c= [:X4,X1,X2,X3:] implies X1 = {};

theorem :: MCART_1:64
   [:X1,X2,X3,X4:] meets [:Y1,Y2,Y3,Y4:] implies
   X1 meets Y1 & X2 meets Y2 & X3 meets Y3 & X4 meets Y4;

theorem :: MCART_1:65
[:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] };

:: Ordered pairs

theorem :: MCART_1:66
 [:X,Y:] <> {} implies
 for x being Element of [:X,Y:] holds x <> x`1 & x <> x`2;

theorem :: MCART_1:67
   x in [:X,Y:] implies x <> x`1 & x <> x`2;

:: Triples

reserve A1 for Subset of X1,
        A2 for Subset of X2,
        A3 for Subset of X3,
        A4 for Subset of X4;

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

theorem :: MCART_1:68
   X1<>{} & X2<>{} & X3<>{} implies
  for x1,x2,x3 st x = [x1,x2,x3] holds x`1 = x1 & x`2 = x2 & x`3 = x3;

theorem :: MCART_1:69
   X1<>{} & X2<>{} & X3<>{} &
  (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y1 = xx1) implies y1 =x`1;

theorem :: MCART_1:70
   X1<>{} & X2<>{} & X3<>{} &
 (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y2 = xx2) implies y2 =x`2;

theorem :: MCART_1:71
   X1<>{} & X2<>{} & X3<>{} &
  (for xx1,xx2,xx3 st x = [xx1,xx2,xx3] holds y3 = xx3) implies y3 =x`3;

theorem :: MCART_1:72
  z in [: X1,X2,X3 :] implies
  ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3];

theorem :: MCART_1:73
 [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3;

theorem :: MCART_1:74
   (for z holds z in Z iff
   ex x1,x2,x3 st x1 in X1 & x2 in X2 & x3 in X3 & z = [x1,x2,x3])
  implies Z = [: X1,X2,X3 :];
theorem :: MCART_1:75
 X1 <> {} & X2 <> {} & X3 <> {} & Y1 <> {} & Y2 <> {} & Y3 <> {} implies
 for x being (Element of [:X1,X2,X3:]), y being Element of [:Y1,Y2,Y3:]
  holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3;

theorem :: MCART_1:76
   for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:]
   holds x`1 in A1 & x`2 in A2 & x`3 in A3;

theorem :: MCART_1:77
 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 implies [:X1,X2,X3:] c= [:Y1,Y2,Y3:];

:: Quadruples

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

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

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

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

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

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

theorem :: MCART_1:83
   z in [: X1,X2,X3,X4 :] implies
  ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in
 X4 & z = [x1,x2,x3,x4];

theorem :: MCART_1:84
   [x1,x2,x3,x4] in [: X1,X2,X3,X4 :] iff x1 in X1 & x2 in X2 & x3 in X3 & x4
in
 X4;

theorem :: MCART_1:85
   (for z holds z in Z iff
  ex x1,x2,x3,x4 st x1 in X1 & x2 in X2 & x3 in X3 & x4 in
 X4 & z = [x1,x2,x3,x4])
  implies Z = [: X1,X2,X3,X4 :];

theorem :: MCART_1:86
 X1<>{} & X2<>{} & X3<>{} & X4<>{} & Y1<>{} & Y2<>{} & Y3<>{} & Y4<>{} implies
 for x being (Element of [:X1,X2,X3,X4:]), y being Element of [:Y1,Y2,Y3,Y4:]
  holds x = y implies x`1 = y`1 & x`2 = y`2 & x`3 = y`3 & x`4 = y`4;

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

theorem :: MCART_1:88
 X1 c= Y1 & X2 c= Y2 & X3 c= Y3 & X4 c= Y4
  implies [:X1,X2,X3,X4:] c= [:Y1,Y2,Y3,Y4:];

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