:: Tuples, Projections and Cartesian Products
::  by Andrzej Trybulec
::
:: Received March 30, 1989
:: Copyright (c) 1990-2021 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies XBOOLE_0, SUBSET_1, TARSKI, ZFMISC_1, RELAT_1, FUNCT_1, MCART_1,
      XTUPLE_0, RECDEF_2, FACIRC_1;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, RELAT_1,
      FUNCT_1;
 constructors TARSKI, ENUMSET1, XTUPLE_0, SUBSET_1, FUNCT_1;
 registrations RELAT_1, XTUPLE_0, SUBSET_1;
 requirements SUBSET, BOOLE;


begin

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

reserve p for pair object;

::
::   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.

::$CT 8

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;

::$CT

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.

reserve R for Relation;

theorem :: MCART_1:21
  x in R implies x = [x`1,x`2];

registration
 let X1,X2 be non empty set;
 cluster -> pair for Element of [:X1,X2:];
end;

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

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

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

::
::   Triples
::

::$CT

theorem :: MCART_1:26
  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
::

::$CT 3

theorem :: MCART_1:30
  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:31
  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:32
  X1<>{} & X2<>{} & X3<>{} implies ( [:X1,X2,X3:] = [:Y1,Y2,Y3:]
  implies X1=Y1 & X2=Y2 & X3=Y3);

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

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

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

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

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

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

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

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

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

theorem :: MCART_1:42
  [:{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] };

registration
 let X1,X2,X3 be non empty set;
 cluster -> triple for Element of [:X1,X2,X3:];
end;

definition
::$CD 4
  let X1,X2,X3 be non empty set;
  let x be Element of [:X1,X2,X3:];
  redefine func x`1_3 -> Element of X1 means
:: MCART_1:def 5

  x = [x1,x2,x3] implies it = x1;
  redefine func x`2_3 -> Element of X2 means
:: MCART_1:def 6

  x = [x1,x2,x3] implies it = x2;
  redefine func x`3_3 -> Element of X3 means
:: MCART_1:def 7

  x = [x1,x2,x3] implies it = x3;
end;

::$CT 2

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

::$CT

theorem :: MCART_1:47
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
   holds x <> x`1_3 & x <> x`2_3 & x <> x`3_3;

theorem :: MCART_1:48
  [: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:49
  [:X1,X2,X3,X4:] = [:[:[:X1,X2:],X3:],X4:];

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

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

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

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

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

reserve xx4 for Element of X4;

registration
 let X1,X2,X3,X4 be non empty set;
 cluster -> quadruple for Element of [:X1,X2,X3,X4:];
end;

definition
  let X1,X2,X3,X4 be non empty set;
  let x be Element of [:X1,X2,X3,X4:];
  redefine func x`1_4 -> Element of X1 means
:: MCART_1:def 8

  x = [x1,x2,x3,x4] implies it = x1;
  redefine func x`2_4 -> Element of X2 means
:: MCART_1:def 9

  x = [x1,x2,x3,x4] implies it = x2;
  redefine func x`3_4 -> Element of X3 means
:: MCART_1:def 10

  x = [x1,x2,x3,x4] implies it = x3;
  redefine func x`4_4 -> Element of X4 means
:: MCART_1:def 11

  x = [x1,x2,x3,x4] implies it = x4;
end;

::$CT 3

theorem :: MCART_1:58
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
  holds x <> x`1_4 & x <> x`2_4 & x <> x`3_4 & x <> x`4_4;

theorem :: MCART_1:59
  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:60
  [: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:61
  [:{x1},{x2},{x3},{x4}:] = { [x1,x2,x3,x4] };

:: Ordered pairs

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

theorem :: MCART_1:63
  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:64
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
 for x1,x2,x3 st x = [x1,x2,x3] holds
  x`1_3 = x1 & x`2_3 = x2 & x`3_3 = x3;

theorem :: MCART_1:65
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y1 = xx1
 holds y1 =x`1_3;

theorem :: MCART_1:66
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds  y2 = xx2
 holds y2 =x`2_3;

theorem :: MCART_1:67
 for X1,X2,X3 being non empty set
 for x being Element of [:X1,X2,X3:]
  st for xx1 being Element of X1,xx2 being Element of X2,
             xx3 being Element of X3 st x = [xx1,xx2,xx3] holds y3 = xx3
 holds y3 =x`3_3;

theorem :: MCART_1:68
  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:69
  [x1,x2,x3] in [: X1,X2,X3 :] iff x1 in X1 & x2 in X2 & x3 in X3;

theorem :: MCART_1:70
  (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 :];

::$CT

theorem :: MCART_1:72
 for X1,X2,X3 being non empty set
 for A1 being non empty Subset of X1, A2 being non empty Subset of X2,
     A3 being non empty Subset of X3
  for x being Element of [:X1,X2,X3:] st x in [:A1,A2,A3:]
   holds x`1_3 in A1 & x`2_3 in A2 & x`3_3 in A3;

theorem :: MCART_1:73
  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:74
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 for x1,x2,x3,x4 being set st x = [x1,
  x2,x3,x4] holds x`1_4 = x1 & x`2_4 = x2 & x`3_4 = x3 & x`4_4 = x4;

theorem :: MCART_1:75
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,xx2,xx3,xx4] holds y1 = xx1
 holds y1 =x`1_4;

theorem :: MCART_1:76
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y2 = xx2
 holds y2 =x`2_4;

theorem :: MCART_1:77
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
 st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y3 = xx3
 holds y3 =x`3_4;

theorem :: MCART_1:78
 for X1,X2,X3,X4 being non empty set
 for x being Element of [:X1,X2,X3,X4:]
  st for xx1 being Element of X1,
             xx2 being Element of X2,
             xx3 being Element of X3,
             xx4 being Element of X4 st x = [xx1,
  xx2,xx3,xx4] holds y4 = xx4
 holds y4 =x`4_4;

theorem :: MCART_1:79
  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:80
  [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:81
  (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 :];

::$CT

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

theorem :: MCART_1:84
  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;

begin :: Addenda

:: from DTCONSTR

definition
  let f be Function;
  func pr1 f -> Function means
:: MCART_1:def 12
  dom it = dom f & for x being object st x in dom f
  holds it.x = (f.x)`1;
  func pr2 f -> Function means
:: MCART_1:def 13
  dom it = dom f & for x being object st x in dom f
  holds it.x = (f.x)`2;
end;

definition
  let x be object;
  func x`11 -> set equals
:: MCART_1:def 14
  x`1`1;
  func x`12 -> set equals
:: MCART_1:def 15
  x`1`2;
  func x`21 -> set equals
:: MCART_1:def 16
  x`2`1;
  func x`22 -> set equals
:: MCART_1:def 17
  x`2`2;
end;

reserve x for object;

theorem :: MCART_1:85
  [[x1,x2],y]`11 = x1 & [[x1,x2],y]`12 = x2 & [x,[y1,y2]]`21 = y1 & [x,[
  y1,y2]]`22 = y2;

:: missing, 2007.04.13, A.T.

theorem :: MCART_1:86
  x in R implies x`1 in dom R & x`2 in rng R;

:: 2009.08.29, A.T.

theorem :: MCART_1:87
 for R being non empty Relation, x being object
  holds Im(R,x) = { I`2 where I is Element of R: I`1 = x };

theorem :: MCART_1:88
 x in R implies x`2 in Im(R,x`1);

theorem :: MCART_1:89
 x in R & y in R & x`1 = y`1 & x`2 = y`2 implies x = y;

theorem :: MCART_1:90
 for R being non empty Relation, x,y being Element of R
   st x`1 = y`1 & x`2 = y`2
 holds x = y;

:: 2010.05.120, A.T.

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

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

scheme :: MCART_1:sch 1
  BiFuncEx{A()->set,B()->set,C()->set,P[object,object,object]}:
ex f,g being Function
  st dom f = A() & dom g = A() & for x st x in A() holds P[x,f.x,g.x]
provided
 x in A() implies ex y,z st y in B() & z in C() & P[x,y,z];

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