:: Domains and Their Cartesian Products
::  by Andrzej Trybulec
::
:: Received April 3, 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, ZFMISC_1, MCART_1, TARSKI, ORDINAL1,
      RECDEF_2;
 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, SUBSET_1, ORDINAL1,
      FUNCT_1, MCART_1;
 constructors TARSKI, ENUMSET1, MCART_1, ORDINAL1, PARTFUN1, XTUPLE_0;
 registrations XBOOLE_0, SUBSET_1, RELAT_1, XTUPLE_0, MCART_1;
 requirements SUBSET, BOOLE;


begin

reserve a,b,c,d for set,
  D,X1,X2,X3,X4 for non empty set,
  x1,y1,z1 for Element of X1,
  x2 for Element of X2,
  x3 for Element of X3,
  x4 for Element of X4,
  A1,B1 for Subset of X1;

::   Domains and their elements

theorem :: DOMAIN_1:1
  a in [:X1,X2:] implies ex x1,x2 st a=[x1,x2];

theorem :: DOMAIN_1:2
  for x,y being Element of [:X1,X2:] st x`1=y`1 & x`2=y`2 holds x=y;

definition
  let X1,X2,x1,x2;
  redefine func [x1,x2] -> Element of [:X1,X2:];
end;

definition
  let X1,X2;
  let x be Element of [:X1,X2:];
  redefine func x`1 -> Element of X1;
  redefine func x`2 -> Element of X2;
end;

::   Cartesian products of three sets

theorem :: DOMAIN_1:3
  a in [: X1,X2,X3 :] iff ex x1,x2,x3 st a = [x1,x2,x3];

theorem :: DOMAIN_1:4
  (for a holds a in D iff ex x1,x2,x3 st a = [x1,x2,x3]) implies D
  = [: X1,X2,X3 :];

theorem :: DOMAIN_1:5
  D = [: X1,X2,X3 :] iff for a holds a in D iff ex x1,x2,x3 st a = [x1,
  x2,x3];

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

definition
  let X1,X2,X3,x1,x2,x3;
  redefine func [x1,x2,x3] -> Element of [:X1,X2,X3:];
end;

theorem :: DOMAIN_1:6
  a =x`1_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds a = x1;

theorem :: DOMAIN_1:7
  b =x`2_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds b = x2;

theorem :: DOMAIN_1:8
  c =x`3_3 iff for x1,x2,x3 st x = [x1,x2,x3] holds c = x3;

theorem :: DOMAIN_1:9
  x`1_3=y`1_3 & x`2_3=y`2_3 & x`3_3=y`3_3 implies x=y;

theorem :: DOMAIN_1:10
  a in [: X1,X2,X3,X4 :] iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4];

theorem :: DOMAIN_1:11
  (for a holds a in D iff ex x1,x2,x3,x4 st a = [x1,x2,x3,x4])
  implies D = [: X1,X2,X3,X4 :];

theorem :: DOMAIN_1:12
  D = [: X1,X2,X3,X4 :] iff for a holds a in D iff ex x1,x2,x3,x4 st a =
  [x1,x2,x3,x4];

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

definition
  let X1,X2,X3,X4,x1,x2,x3,x4;
  redefine func [x1,x2,x3,x4] -> Element of [:X1,X2,X3,X4:];
end;

theorem :: DOMAIN_1:13
  a=x`1_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds a = x1;

theorem :: DOMAIN_1:14
  b=x`2_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds b = x2;

theorem :: DOMAIN_1:15
  c = x`3_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds c = x3;

theorem :: DOMAIN_1:16
  d=x`4_4 iff for x1,x2,x3,x4 st x = [x1,x2,x3,x4] holds d = x4;

theorem :: DOMAIN_1:17
  for x,y being Element of [:X1,X2,X3,X4:]
   st x`1_4=y`1_4 & x`2_4=y`2_4 & x`3_4=y
  `3_4 & x`4_4=y`4_4 holds x=y;

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

scheme :: DOMAIN_1:sch 1
  Fraenkel1 {P[object]}: for X1 holds { x1 : P[x1] } is Subset of X1;

scheme :: DOMAIN_1:sch 2
  Fraenkel2 {P[object,object]}:
  for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:];

scheme :: DOMAIN_1:sch 3
  Fraenkel3 {P[object,object,object]}:
  for X1,X2,X3 holds { [x1,x2,x3] : P[x1,x2,x3] } is Subset of [:X1,X2,X3:];

scheme :: DOMAIN_1:sch 4
  Fraenkel4 {P[object,object,object,object]}:
  for X1,X2,X3,X4 holds
  { [x1,x2,x3,x4] : P[x1,x2,x3,x4] } is Subset of [:X1,X2,X3,X4:];

scheme :: DOMAIN_1:sch 5
  Fraenkel5 {P,Q[object]}: for X1 st for x1 holds P[x1] implies Q[x1] holds
  { y1 : P[y1] } c= { z1 : Q[z1] };

scheme :: DOMAIN_1:sch 6
  Fraenkel6 {P,Q[object]}: for X1 st for x1 holds P[x1] iff Q[x1] holds { y1
  : P[y1] } = { z1 : Q[z1] };

scheme :: DOMAIN_1:sch 7
  SubsetD{D() -> non empty set,P[object]}: {d where d is Element of D() : P[d]}
  is Subset of D();

theorem :: DOMAIN_1:18
  X1 = the set of all x1;

theorem :: DOMAIN_1:19
  [:X1,X2:] = the set of all  [x1,x2];

theorem :: DOMAIN_1:20
  [:X1,X2,X3:] = the set of all  [x1,x2,x3];

theorem :: DOMAIN_1:21
  [:X1,X2,X3,X4:] = the set of all  [x1,x2,x3,x4];

theorem :: DOMAIN_1:22
  A1 = { x1 : x1 in A1 };

theorem :: DOMAIN_1:23
  [:A1,A2:] = { [x1,x2] : x1 in A1 & x2 in A2 };

theorem :: DOMAIN_1:24
  [:A1,A2,A3:] = { [x1,x2,x3] : x1 in A1 & x2 in A2 & x3 in A3 };

theorem :: DOMAIN_1:25
  [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] : x1 in A1 & x2 in A2 & x3 in A3 &
  x4 in A4 };

theorem :: DOMAIN_1:26
  {} X1 = { x1 : contradiction };

theorem :: DOMAIN_1:27
  A1` = { x1 : not x1 in A1 };

theorem :: DOMAIN_1:28
  A1 /\ B1 = { x1 : x1 in A1 & x1 in B1 };

theorem :: DOMAIN_1:29
  A1 \/ B1 = { x1 : x1 in A1 or x1 in B1 };

theorem :: DOMAIN_1:30
  A1 \ B1 = { x1 : x1 in A1 & not x1 in B1 };

theorem :: DOMAIN_1:31
  A1 \+\ B1 = { x1 : x1 in A1 & not x1 in B1 or not x1 in A1 & x1 in B1 };

theorem :: DOMAIN_1:32
  A1 \+\ B1 = { x1 : not x1 in A1 iff x1 in B1 };

theorem :: DOMAIN_1:33
  A1 \+\ B1 = { x1 : x1 in A1 iff not x1 in B1 };

theorem :: DOMAIN_1:34
  A1 \+\ B1 = { x1 : not(x1 in A1 iff x1 in B1) };

definition
  let D be non empty set;
  let x1 be Element of D;
  redefine func {x1} -> Subset of D;
  let x2 be Element of D;
  redefine func {x1,x2} -> Subset of D;
  let x3 be Element of D;
  redefine func {x1,x2,x3} -> Subset of D;
  let x4 be Element of D;
  redefine func {x1,x2,x3,x4} -> Subset of D;
  let x5 be Element of D;
  redefine func {x1,x2,x3,x4,x5} -> Subset of D;
  let x6 be Element of D;
  redefine func {x1,x2,x3,x4,x5,x6} -> Subset of D;
  let x7 be Element of D;
  redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of D;
  let x8 be Element of D;
  redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of D;
  let x9 be Element of D;
  redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9} -> Subset of D;
  let x10 be Element of D;
  redefine func {x1,x2,x3,x4,x5,x6,x7,x8,x9,x10} -> Subset of D;
end;

begin :: Addenda
:: from COMPLSP1

scheme :: DOMAIN_1:sch 8
  SubsetFD { A, D() -> non empty set, F(object) -> Element of D(), P[object] }:
  { F(x) where x is Element of A(): P[x]} is Subset of D();

scheme :: DOMAIN_1:sch 9
  SubsetFD2 { A, B, D() -> non empty set, F(object,object) -> Element of D(),
  P[object,object] }:
  { F(x,y) where x is Element of A(), y is Element of B(): P[x,y]}
  is Subset of D();

definition
  let D1,D2,D3 be non empty set, x be Element of [:[:D1,D2:],D3:];
  redefine func x`11 -> Element of D1;
  redefine func x`12 -> Element of D2;
end;

definition
  let D1,D2,D3 be non empty set, x be Element of [:D1,[:D2,D3:]:];
  redefine func x`21 -> Element of D2;
  redefine func x`22 -> Element of D3;
end;

:: from JORDAN_A, 2005.10.12 , A.T.

scheme :: DOMAIN_1:sch 10
  AndScheme{A()-> non empty set, P,Q[object]}: { a where a is Element of A():
  P[a] & Q[a] } = { a1 where a1 is Element of A(): P[a1] } /\ { a2 where a2 is
  Element of A(): Q[a2] };

:: from HAHNBAN, 2011.04.26, A.T.

registration
  let A be non empty set;
  cluster c=-linear non empty for Subset of A;
end;