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


begin

:: Domains and their elements
theorem :: DOMAIN_1:1
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]
proofend;

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

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:87;
end;

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

:: Cartesian products of three sets
theorem Th3: :: DOMAIN_1:3
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] )
proofend;

theorem Th4: :: DOMAIN_1:4
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:]
proofend;

theorem :: DOMAIN_1:5
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 Th3, Th4;

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:69;
end;

theorem :: DOMAIN_1:6
for a being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( a = x `1_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
a = x1 )
proofend;

theorem :: DOMAIN_1:7
for b being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( b = x `2_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
b = x2 )
proofend;

theorem :: DOMAIN_1:8
for c being set
for X1, X2, X3 being non empty set
for x being Element of [:X1,X2,X3:] holds
( c = x `3_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 )
proofend;

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

theorem Th10: :: DOMAIN_1:10
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] )
proofend;

theorem Th11: :: DOMAIN_1:11
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:]
proofend;

theorem :: DOMAIN_1:12
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 Th10, Th11;

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:80;
end;

theorem :: DOMAIN_1:13
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_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
a = x1 )
proofend;

theorem :: DOMAIN_1:14
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_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
b = x2 )
proofend;

theorem :: DOMAIN_1:15
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_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
c = x3 )
proofend;

theorem :: DOMAIN_1:16
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_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 )
proofend;

theorem :: DOMAIN_1:17
for X1, X2, X3, X4 being non empty set
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
proofend;

scheme :: DOMAIN_1:sch 1
Fraenkel1{ P1[ set ] } :
 for X1 being non empty set holds  {  x1 where x1 is Element of X1 : P1[x1]  }  is Subset of X1
proofend;

scheme :: DOMAIN_1:sch 2
Fraenkel2{ P1[ set , set ] } :
 for X1, X2 being non empty set holds  {  [x1,x2] where x1 is Element of X1, x2 is Element of X2 : P1[x1,x2]  }  is Subset of [:X1,X2:]
proofend;

scheme :: DOMAIN_1:sch 3
Fraenkel3{ P1[ 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 : P1[x1,x2,x3]  }  is Subset of [:X1,X2,X3:]
proofend;

scheme :: DOMAIN_1:sch 4
Fraenkel4{ P1[ 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 : P1[x1,x2,x3,x4]  }  is Subset of [:X1,X2,X3,X4:]
proofend;

scheme :: DOMAIN_1:sch 5
Fraenkel5{ P1[ set ], P2[ set ] } :
 for X1 being non empty set st ( for x1 being Element of X1 st P1[x1] holds
P2[x1] ) holds
{  y1 where y1 is Element of X1 : P1[y1]  }  c=  {  z1 where z1 is Element of X1 : P2[z1]  }
proofend;

scheme :: DOMAIN_1:sch 6
Fraenkel6{ P1[ set ], P2[ set ] } :
 for X1 being non empty set st ( for x1 being Element of X1 holds
( P1[x1] iff P2[x1] ) ) holds
{  y1 where y1 is Element of X1 : P1[y1]  }  =  {  z1 where z1 is Element of X1 : P2[z1]  }
proofend;

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

theorem :: DOMAIN_1:18
for X1 being non empty set holds X1 =  {  x1 where x1 is Element of X1 : verum  }
proofend;

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

theorem :: DOMAIN_1:20
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  }
proofend;

theorem :: DOMAIN_1:21
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  }
proofend;

theorem :: DOMAIN_1:22
for X1 being non empty set
for A1 being Subset of X1 holds A1 =  {  x1 where x1 is Element of X1 : x1 in A1  }
proofend;

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

theorem :: DOMAIN_1:24
for X1, X2, X3 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3 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 )  }
proofend;

theorem :: DOMAIN_1:25
for X1, X2, X3, X4 being non empty set
for A1 being Subset of X1
for A2 being Subset of X2
for A3 being Subset of X3
for A4 being Subset of X4 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 )  }
proofend;

theorem :: DOMAIN_1:26
for X1 being non empty set holds {} X1 =  {  x1 where x1 is Element of X1 : contradiction  }
proofend;

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

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

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

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

theorem Th31: :: DOMAIN_1:31
for X1 being non empty set
for A1, B1 being Subset of X1 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 ) )  }
proofend;

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

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

theorem :: DOMAIN_1:34
for X1 being non empty set
for A1, B1 being Subset of X1 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 ) )  }
proofend;

definition
let D be non empty set ;
let x1 be Element of D;
:: original:{
redefine func{x1} ->  Subset of D;
coherence
 {x1} is Subset of D by SUBSET_1:33;
let x2 be Element of D;
:: original:{
redefine func{x1,x2} ->  Subset of D;
coherence
 {x1,x2} is Subset of D by SUBSET_1:34;
let x3 be Element of D;
:: original:{
redefine func{x1,x2,x3} ->  Subset of D;
coherence
 {x1,x2,x3} is Subset of D by SUBSET_1:35;
let x4 be Element of D;
:: original:{
redefine func{x1,x2,x3,x4} ->  Subset of D;
coherence
 {x1,x2,x3,x4} is Subset of D by SUBSET_1:36;
let x5 be Element of D;
:: original:{
redefine func{x1,x2,x3,x4,x5} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5} is Subset of D by SUBSET_1:37;
let x6 be Element of D;
:: original:{
redefine func{x1,x2,x3,x4,x5,x6} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6} is Subset of D by SUBSET_1:38;
let x7 be Element of D;
:: original:{
redefine func{x1,x2,x3,x4,x5,x6,x7} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6,x7} is Subset of D by SUBSET_1:39;
let x8 be Element of D;
:: original:{
redefine func{x1,x2,x3,x4,x5,x6,x7,x8} ->  Subset of D;
coherence
 {x1,x2,x3,x4,x5,x6,x7,x8} is Subset of D by SUBSET_1:40;
end;

begin

scheme :: DOMAIN_1:sch 8
SubsetFD{ F1() ->  non empty set , F2() ->  non empty set , F3( set ) ->  Element of F2(), P1[ set ] } :
  {  F3(x) where x is Element of F1() : P1[x]  }  is Subset of F2()
proofend;

scheme :: DOMAIN_1:sch 9
SubsetFD2{ F1() ->  non empty set , F2() ->  non empty set , F3() ->  non empty set , F4( set , set ) ->  Element of F3(), P1[ set , set ] } :
  {  F4(x,y) where x is Element of F1(), y is Element of F2() : P1[x,y]  }  is Subset of F3()
proofend;

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

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

scheme :: DOMAIN_1:sch 10
AndScheme{ F1() ->  non empty set , P1[ set ], P2[ set ] } :
  {  a where a is Element of F1() : ( P1[a] & P2[a] )  }  =  {  a1 where a1 is Element of F1() : P1[a1]  }  /\  {  a2 where a2 is Element of F1() : P2[a2]  }
proofend;

:: from HAHNBAN, 2011.04.26, A.T.
registration
let A be non empty set ;
cluster non empty c=-linear for Element of bool A;
existence
 ex b1 being Subset of A st
( b1 is c=-linear & not b1 is empty )
proofend;
end;