Journal of Formalized Mathematics
Volume 1, 1989
University of Bialystok
Copyright (c) 1989 Association of Mizar Users

### Domains and Their Cartesian Products

by
Andrzej Trybulec

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;

```