The abstract of the Mizar article:

Domains and Their Cartesian Products

by

Andrzej Trybulec

Received April 3, 1989

MML identifier: DOMAIN_1

[ Mizar article, MML identifier index ]

environ

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


begin

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


:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::
::
::   Domains and their elements
::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

canceled 8;

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

canceled 2;

theorem :: DOMAIN_1:12
     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
::
:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::

canceled 2;

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

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

theorem :: DOMAIN_1:17
    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;

canceled 6;

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

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

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

canceled;

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

canceled 2;

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

theorem :: DOMAIN_1:32
 (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:33
   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;

canceled 6;

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

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

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

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

canceled;

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

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

scheme Fraenkel1 {P[set]}:
 for X1 holds { x1 : P[x1] } is Subset of X1;

scheme Fraenkel2 {P[set,set]}:
 for X1,X2 holds { [x1,x2] : P[x1,x2] } is Subset of [:X1,X2:];

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

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

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

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

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

canceled 2;

theorem :: DOMAIN_1:48
   X1 = { x1 : not contradiction };

theorem :: DOMAIN_1:49
   [:X1,X2:] = { [x1,x2] : not contradiction };

theorem :: DOMAIN_1:50
   [:X1,X2,X3:] = { [x1,x2,x3] : not contradiction };

theorem :: DOMAIN_1:51
   [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] : not contradiction };

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: DOMAIN_1:64
   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;
end;