:: Domains and Their Cartesian Products
:: by Andrzej Trybulec
::
:: Received April 3, 1989
:: Copyright (c) 1990 Association of Mizar Users

begin

theorem :: DOMAIN_1:1

canceled;

theorem :: DOMAIN_1:2

canceled;

theorem :: DOMAIN_1:3

canceled;

theorem :: DOMAIN_1:4

canceled;

theorem :: DOMAIN_1:5

canceled;

theorem :: DOMAIN_1:6

canceled;

theorem :: DOMAIN_1:7

canceled;

theorem :: DOMAIN_1:8

canceled;

theorem :: DOMAIN_1:9

for a being set
for X1, X2 being non empty set st a in [:X1,X2:] holds
ex x1 being Element of X1 ex x2 being Element of X2 st a = [x1,x2]

proof end;

theorem :: DOMAIN_1:10

canceled;

theorem :: DOMAIN_1:11

canceled;

theorem :: DOMAIN_1:12

for X1, X2 being non empty set
for x, y being Element of [:X1,X2:] st x `1 = y `1 & x `2 = y `2 holds
x = y

proof end;

definition

let X1, X2 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
:: original: [
redefine func [x1,x2] -> Element of [:X1,X2:];
coherence
[x1,x2] is Element of [:X1,X2:] by ZFMISC_1:106;

end;

definition

let X1, X2 be non empty set ;
let x be Element of [:X1,X2:];
:: original: `1
redefine func x `1 -> Element of X1;
coherence
x `1 is Element of X1 by MCART_1:10;
:: original: `2
redefine func x `2 -> Element of X2;
coherence
x `2 is Element of X2 by MCART_1:10;

end;

theorem :: DOMAIN_1:13

canceled;

theorem :: DOMAIN_1:14

canceled;

theorem Th15: :: DOMAIN_1:15

for a being set
for X1, X2, X3 being non empty set holds
( a in [:X1,X2,X3:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] )

proof end;

theorem Th16: :: DOMAIN_1:16

for D, X1, X2, X3 being non empty set st ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) holds
D = [:X1,X2,X3:]

proof end;

theorem :: DOMAIN_1:17

for D, X1, X2, X3 being non empty set holds
( D = [:X1,X2,X3:] iff for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 st a = [x1,x2,x3] ) ) by Th15, Th16;

definition

let X1, X2, X3 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
let x3 be Element of X3;
:: original: [
redefine func [x1,x2,x3] -> Element of [:X1,X2,X3:];
coherence
[x1,x2,x3] is Element of [:X1,X2,X3:] by MCART_1:73;

end;

theorem :: DOMAIN_1:18

canceled;

theorem :: DOMAIN_1:19

canceled;

theorem :: DOMAIN_1:20

canceled;

theorem :: DOMAIN_1:21

canceled;

theorem :: DOMAIN_1:22

canceled;

theorem :: DOMAIN_1:23

canceled;

theorem :: DOMAIN_1:24

for a being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( a = x `1 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
a = x1 )

proof end;

theorem :: DOMAIN_1:25

for b being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( b = x `2 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
b = x2 )

proof end;

theorem :: DOMAIN_1:26

for c being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( c = x `3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3 st x = [x1,x2,x3] holds
c = x3 )

proof end;

theorem :: DOMAIN_1:27

canceled;

theorem :: DOMAIN_1:28

for X1, X2, X3 being non empty set
for x, y being Element of [:X1,X2,X3:] st x `1 = y `1 & x `2 = y `2 & x `3 = y `3 holds
x = y

proof end;

theorem :: DOMAIN_1:29

canceled;

theorem :: DOMAIN_1:30

canceled;

theorem Th31: :: DOMAIN_1:31

for a being set
for X1, X2, X3, X4 being non empty set holds
( a in [:X1,X2,X3,X4:] iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] )

proof end;

theorem Th32: :: DOMAIN_1:32

for D, X1, X2, X3, X4 being non empty set st ( for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) holds
D = [:X1,X2,X3,X4:]

proof end;

theorem :: DOMAIN_1:33

for D, X1, X2, X3, X4 being non empty set holds
( D = [:X1,X2,X3,X4:] iff for a being set holds
( a in D iff ex x1 being Element of X1 ex x2 being Element of X2 ex x3 being Element of X3 ex x4 being Element of X4 st a = [x1,x2,x3,x4] ) ) by Th31, Th32;

definition

let X1, X2, X3, X4 be non empty set ;
let x1 be Element of X1;
let x2 be Element of X2;
let x3 be Element of X3;
let x4 be Element of X4;
:: original: [
redefine func [x1,x2,x3,x4] -> Element of [:X1,X2,X3,X4:];
coherence
[x1,x2,x3,x4] is Element of [:X1,X2,X3,X4:] by MCART_1:84;

end;

theorem :: DOMAIN_1:34

canceled;

theorem :: DOMAIN_1:35

canceled;

theorem :: DOMAIN_1:36

canceled;

theorem :: DOMAIN_1:37

canceled;

theorem :: DOMAIN_1:38

canceled;

theorem :: DOMAIN_1:39

canceled;

theorem :: DOMAIN_1:40

for a being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( a = x `1 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
a = x1 )

proof end;

theorem :: DOMAIN_1:41

for b being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( b = x `2 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
b = x2 )

proof end;

theorem :: DOMAIN_1:42

for c being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( c = x `3 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
c = x3 )

proof end;

theorem :: DOMAIN_1:43

for d being set
for X1, X2, X3, X4 being non empty set
for x being Element of [:X1,X2,X3,X4:] holds
( d = x `4 iff for x1 being Element of X1
for x2 being Element of X2
for x3 being Element of X3
for x4 being Element of X4 st x = [x1,x2,x3,x4] holds
d = x4 )

proof end;

theorem :: DOMAIN_1:44

canceled;

theorem :: DOMAIN_1:45

for X1, X2, X3, X4 being non empty set
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

proof end;

scheme :: DOMAIN_1:sch 1
Fraenkel1{ P₁[ set ] } :

for X1 being non empty set holds { x1 where x1 is Element of X1 : P₁[x1] } is Subset of

proof end;

scheme :: DOMAIN_1:sch 2
Fraenkel2{ P₁[ set , set ] } :

for X1, X2 being non empty set holds { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P₁[x1,x2] } is Subset of

proof end;

scheme :: DOMAIN_1:sch 3
Fraenkel3{ P₁[ set , set , set ] } :

for X1, X2, X3 being non empty set holds { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : P₁[x1,x2,x3] } is Subset of

proof end;

scheme :: DOMAIN_1:sch 4
Fraenkel4{ P₁[ set , set , set , set ] } :

for X1, X2, X3, X4 being non empty set holds { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : P₁[x1,x2,x3,x4] } is Subset of

proof end;

scheme :: DOMAIN_1:sch 5
Fraenkel5{ P₁[ set ], P₂[ set ] } :

for X1 being non empty set st ( for x1 being Element of X1 st P₁[x1] holds
P₂[x1] ) holds
{ y1 where y1 is Element of X1 : P₁[y1] } c= { z1 where z1 is Element of X1 : P₂[z1] }

proof end;

scheme :: DOMAIN_1:sch 6
Fraenkel6{ P₁[ set ], P₂[ set ] } :

for X1 being non empty set st ( for x1 being Element of X1 holds
( P₁[x1] iff P₂[x1] ) ) holds
{ y1 where y1 is Element of X1 : P₁[y1] } = { z1 where z1 is Element of X1 : P₂[z1] }

proof end;

scheme :: DOMAIN_1:sch 7
SubsetD{ F₁() -> non empty set , P₁[ set ] } :

{ d where d is Element of F₁() : P₁[d] } is Subset of

proof end;

theorem :: DOMAIN_1:46

canceled;

theorem :: DOMAIN_1:47

canceled;

theorem :: DOMAIN_1:48

for X1 being non empty set holds X1 = { x1 where x1 is Element of X1 : verum }

proof end;

theorem :: DOMAIN_1:49

for X1, X2 being non empty set holds [:X1,X2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : verum }

proof end;

theorem :: DOMAIN_1:50

for X1, X2, X3 being non empty set holds [:X1,X2,X3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : verum }

proof end;

theorem :: DOMAIN_1:51

for X1, X2, X3, X4 being non empty set holds [:X1,X2,X3,X4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : verum }

proof end;

theorem :: DOMAIN_1:52

for X1 being non empty set
for A1 being Subset of holds A1 = { x1 where x1 is Element of X1 : x1 in A1 }

proof end;

theorem :: DOMAIN_1:53

for X1, X2 being non empty set
for A1 being Subset of
for A2 being Subset of holds [:A1,A2:] = { [x1,x2] where x1 is Element of X1, x2 is Element of X2 : ( x1 in A1 & x2 in A2 ) }

proof end;

theorem :: DOMAIN_1:54

for X1, X2, X3 being non empty set
for A1 being Subset of
for A2 being Subset of
for A3 being Subset of holds [:A1,A2,A3:] = { [x1,x2,x3] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3 : ( x1 in A1 & x2 in A2 & x3 in A3 ) }

proof end;

theorem :: DOMAIN_1:55

for X1, X2, X3, X4 being non empty set
for A1 being Subset of
for A2 being Subset of
for A3 being Subset of
for A4 being Subset of holds [:A1,A2,A3,A4:] = { [x1,x2,x3,x4] where x1 is Element of X1, x2 is Element of X2, x3 is Element of X3, x4 is Element of X4 : ( x1 in A1 & x2 in A2 & x3 in A3 & x4 in A4 ) }

proof end;

theorem :: DOMAIN_1:56

for X1 being non empty set holds {} X1 = { x1 where x1 is Element of X1 : contradiction }

proof end;

theorem :: DOMAIN_1:57

for X1 being non empty set
for A1 being Subset of holds A1 ` = { x1 where x1 is Element of X1 : not x1 in A1 }

proof end;

theorem :: DOMAIN_1:58

for X1 being non empty set
for A1, B1 being Subset of holds A1 /\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & x1 in B1 ) }

proof end;

theorem :: DOMAIN_1:59

for X1 being non empty set
for A1, B1 being Subset of holds A1 \/ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 or x1 in B1 ) }

proof end;

theorem :: DOMAIN_1:60

for X1 being non empty set
for A1, B1 being Subset of holds A1 \ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 & not x1 in B1 ) }

proof end;

theorem Th61: :: DOMAIN_1:61

for X1 being non empty set
for A1, B1 being Subset of holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( not x1 in A1 & x1 in B1 ) ) }

proof end;

theorem Th62: :: DOMAIN_1:62

for X1 being non empty set
for A1, B1 being Subset of holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( not x1 in A1 iff x1 in B1 ) }

proof end;

theorem :: DOMAIN_1:63

for X1 being non empty set
for A1, B1 being Subset of holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( x1 in A1 iff not x1 in B1 ) }

proof end;

theorem :: DOMAIN_1:64

for X1 being non empty set
for A1, B1 being Subset of holds A1 \+\ B1 = { x1 where x1 is Element of X1 : ( ( x1 in A1 & not x1 in B1 ) or ( x1 in B1 & not x1 in A1 ) ) }

proof end;

definition

let D be non empty set ;
let x1 be Element of D;
:: original: {
redefine func {x1} -> Subset of ;
coherence
{x1} is Subset of by SUBSET_1:55;
let x2 be Element of D;
:: original: {
redefine func {x1,x2} -> Subset of ;
coherence
{x1,x2} is Subset of by SUBSET_1:56;
let x3 be Element of D;
:: original: {
redefine func {x1,x2,x3} -> Subset of ;
coherence
{x1,x2,x3} is Subset of by SUBSET_1:57;
let x4 be Element of D;
:: original: {
redefine func {x1,x2,x3,x4} -> Subset of ;
coherence
{x1,x2,x3,x4} is Subset of by SUBSET_1:58;
let x5 be Element of D;
:: original: {
redefine func {x1,x2,x3,x4,x5} -> Subset of ;
coherence
{x1,x2,x3,x4,x5} is Subset of by SUBSET_1:59;
let x6 be Element of D;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6} -> Subset of ;
coherence
{x1,x2,x3,x4,x5,x6} is Subset of by SUBSET_1:60;
let x7 be Element of D;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7} -> Subset of ;
coherence
{x1,x2,x3,x4,x5,x6,x7} is Subset of by SUBSET_1:61;
let x8 be Element of D;
:: original: {
redefine func {x1,x2,x3,x4,x5,x6,x7,x8} -> Subset of ;
coherence
{x1,x2,x3,x4,x5,x6,x7,x8} is Subset of by SUBSET_1:62;

end;

begin

scheme :: DOMAIN_1:sch 8
SubsetFD{ F₁() -> non empty set , F₂() -> non empty set , F₃( set ) -> Element of F₂(), P₁[ set ] } :

{ F₃(x) where x is Element of F₁() : P₁[x] } is Subset of

proof end;

scheme :: DOMAIN_1:sch 9
SubsetFD2{ F₁() -> non empty set , F₂() -> non empty set , F₃() -> non empty set , F₄( set , set ) -> Element of F₃(), P₁[ set , set ] } :

{ F₄(x,y) where x is Element of F₁(), y is Element of F₂() : P₁[x,y] } is Subset of

proof end;

definition

let D1, D2, D3 be non empty set ;
let x be Element of [:[:D1,D2:],D3:];
:: original: `11
redefine func x `11 -> Element of D1;
coherence
x `11 is Element of D1

proof end;

:: original: `12
redefine func x `12 -> Element of D2;
coherence
x `12 is Element of D2

proof end;

end;

definition

let D1, D2, D3 be non empty set ;
let x be Element of [:D1,[:D2,D3:]:];
:: original: `21
redefine func x `21 -> Element of D2;
coherence
x `21 is Element of D2

proof end;

:: original: `22
redefine func x `22 -> Element of D3;
coherence
x `22 is Element of D3

proof end;

end;

scheme :: DOMAIN_1:sch 10
AndScheme{ F₁() -> non empty set , P₁[ set ], P₂[ set ] } :

{ a where a is Element of F₁() : ( P₁[a] & P₂[a] ) } = { a1 where a1 is Element of F₁() : P₁[a1] } /\ { a2 where a2 is Element of F₁() : P₂[a2] }

proof end;