:: Properties of First and Second Order Cutting of Binary Relations
:: by Krzysztof Retel
::
:: Received April 25, 2005
:: Copyright (c) 2005-2012 Association of Mizar Users


begin

notation
let X be set ;
synonym {_{X}_} for  SmallestPartition X;
end;

theorem Th1: :: RELSET_2:1
for y, X being set holds
( y in {_{X}_} iff ex x being set st
( y = {x} & x in X ) )
proofend;

theorem Th2: :: RELSET_2:2
for X being set holds
( X = {} iff {_{X}_} = {} )
proofend;

theorem Th3: :: RELSET_2:3
for X, Y being set holds {_{(X \/ Y)}_} = {_{X}_} \/ {_{Y}_}
proofend;

theorem Th4: :: RELSET_2:4
for X, Y being set holds {_{(X /\ Y)}_} = {_{X}_} /\ {_{Y}_}
proofend;

theorem :: RELSET_2:5
for X, Y being set holds {_{(X \ Y)}_} = {_{X}_} \ {_{Y}_}
proofend;

theorem Th6: :: RELSET_2:6
for X, Y being set holds
( X c= Y iff {_{X}_} c= {_{Y}_} )
proofend;

theorem :: RELSET_2:7
for M being set
for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)
proofend;

theorem :: RELSET_2:8
for P, Q, R being Relation holds (P /\ Q) * R c= (P * R) /\ (Q * R)
proofend;

begin

theorem Th9: :: RELSET_2:9
for y, x being set
for R being Relation holds
( y in Im (R,x) iff [x,y] in R )
proofend;

theorem Th10: :: RELSET_2:10
for x being set
for R1, R2 being Relation holds Im ((R1 \/ R2),x) = (Im (R1,x)) \/ (Im (R2,x))
proofend;

theorem Th11: :: RELSET_2:11
for x being set
for R1, R2 being Relation holds Im ((R1 /\ R2),x) = (Im (R1,x)) /\ (Im (R2,x))
proofend;

theorem :: RELSET_2:12
for x being set
for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
proofend;

theorem :: RELSET_2:13
for X being set
for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})
proofend;

definition
let X, Y be set ;
let R be Relation of X,Y;
let x be set ;
:: original:Im
redefine func Im (R,x) ->  Subset of Y;
coherence
 Im (R,x) is Subset of Y
proofend;
:: original:Coim
redefine func Coim (R,x) ->  Subset of X;
coherence
 Coim (R,x) is Subset of X
proofend;
end;

theorem :: RELSET_2:14
for A being set
for F being Subset-Family of A
for R being Relation holds R .: (union F) = union  {  (R .: X) where X is Subset of A : X in F  }
proofend;

:: (3.1.2) - RELAT_1:149
theorem Th15: :: RELSET_2:15
for A being non empty set
for X being Subset of A holds X = union  {  {x} where x is Element of A : x in X  }
proofend;

theorem :: RELSET_2:16
for A being non empty set
for X being Subset of A holds  {  {x} where x is Element of A : x in X  }  is Subset-Family of A
proofend;

theorem :: RELSET_2:17
for A being non empty set
for B being set
for X being Subset of A
for R being Relation of A,B holds R .: X = union  {  (Class (R,x)) where x is Element of A : x in X  }
proofend;

theorem :: RELSET_2:18
for A being non empty set
for B being set
for X being Subset of A
for R being Relation of A,B holds  {  (R .: x) where x is Element of A : x in X  }  is Subset-Family of B
proofend;

definition
let A be set ;
let R be Relation;
func .: (R,A) ->  Function means :Def1: :: RELSET_2:def 1
( dom it = bool A & ( for X being set st X c= A holds
it . X = R .: X ) );
existence
 ex b1 being Function st
( dom b1 = bool A & ( for X being set st X c= A holds
b1 . X = R .: X ) )
proofend;
uniqueness
 for b1, b2 being Function st dom b1 = bool A & ( for X being set st X c= A holds
b1 . X = R .: X ) & dom b2 = bool A & ( for X being set st X c= A holds
b2 . X = R .: X ) holds
b1 = b2
proofend;
end;

:: deftheorem Def1 defines .: RELSET_2:def_1_:_
 for A being set
for R being Relation
for b3 being Function holds
( b3 = .: (R,A) iff ( dom b3 = bool A & ( for X being set st X c= A holds
b3 . X = R .: X ) ) );

notation
let B, A be set ;
let R be Subset of [:A,B:];
synonym  .: R for  .: (A,B);
end;

theorem Th19: :: RELSET_2:19
for X, A, B being set
for R being Subset of [:A,B:] st X in dom (.: ) holds
(.: ) . X = R .: X
proofend;

theorem Th20: :: RELSET_2:20
for A, B being set
for R being Subset of [:A,B:] holds rng (.: ) c= bool (rng R)
proofend;

theorem Th21: :: RELSET_2:21
for A, B being set
for R being Subset of [:A,B:] holds .: is Function of (bool A),(bool (rng R))
proofend;

definition
let B, A be set ;
let R be Subset of [:A,B:];
:: original:.:
redefine func .: R ->  Function of (bool A),(bool B);
correctness
coherence
.: (R,A) is Function of (bool A),(bool B);
proofend;
end;

theorem :: RELSET_2:22
for A, B being set
for R being Subset of [:A,B:] holds union ((.: R) .: A) c= R .: (union A)
proofend;

begin

definition
let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];
funcR .:^ X ->  set  equals :: RELSET_2:def 2
 Intersect ((.: R) .: {_{X}_});
correctness
coherence
Intersect ((.: R) .: {_{X}_}) is set ;
;
end;

:: deftheorem  defines .:^ RELSET_2:def_2_:_
 for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds R .:^ X = Intersect ((.: R) .: {_{X}_});

definition
let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];
:: original:.:^
redefine funcR .:^ X ->  Subset of B;
coherence
 R .:^ X is Subset of B ;
end;

theorem Th23: :: RELSET_2:23
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds
( (.: R) .: {_{X}_} = {} iff X = {} )
proofend;

theorem Th24: :: RELSET_2:24
for A, B, y being set
for X being Subset of A
for R being Subset of [:A,B:] st y in R .:^ X holds
for x being set st x in X holds
y in Im (R,x)
proofend;

theorem Th25: :: RELSET_2:25
for B being non empty set
for A being set
for X being Subset of A
for y being Element of B
for R being Subset of [:A,B:] holds
( y in R .:^ X iff for x being set st x in X holds
y in Im (R,x) )
proofend;

theorem :: RELSET_2:26
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st (.: R) .: {_{X1}_} = {} holds
R .:^ (X1 \/ X2) = R .:^ X2
proofend;

:: ksiazka S o R = SR a w MML jest to R*S
:: (1) S .:(R.:X) = (S o R).:X
:: w notacji uzytej w MML: S.:(R.:X) = (R*S).:X
theorem :: RELSET_2:27
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds R .:^ (X1 \/ X2) = (R .:^ X1) /\ (R .:^ X2)
proofend;

theorem :: RELSET_2:28
for A being non empty set
for B being set
for F being Subset-Family of A
for R being Relation of A,B holds  {  (R .:^ X) where X is Subset of A : X in F  }  is Subset-Family of B
proofend;

theorem Th29: :: RELSET_2:29
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X = {} holds
R .:^ X = B
proofend;

theorem :: RELSET_2:30
for A being set
for B being non empty set
for R being Relation of A,B
for F being Subset-Family of A
for G being Subset-Family of B st G =  {  (R .:^ Y) where Y is Subset of A : Y in F  }  holds
R .:^ (union F) = Intersect G
proofend;

theorem Th31: :: RELSET_2:31
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] st X1 c= X2 holds
R .:^ X2 c= R .:^ X1
proofend;

theorem :: RELSET_2:32
for A, B being set
for X1, X2 being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X1) \/ (R .:^ X2) c= R .:^ (X1 /\ X2)
proofend;

theorem :: RELSET_2:33
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 /\ R2) .:^ X = (R1 .:^ X) /\ (R2 .:^ X)
proofend;

theorem :: RELSET_2:34
for A, B being set
for X being Subset of A
for FR being Subset-Family of [:A,B:] holds (union FR) .: X = union  {  (R .: X) where R is Subset of [:A,B:] : R in FR  }
proofend;

:: (7.1.2) - RELAT_1:150
theorem :: RELSET_2:35
for A, B being set
for FR being Subset-Family of [:A,B:]
for A, B being set
for X being Subset of A holds  {  (R .:^ X) where R is Subset of [:A,B:] : R in FR  }  is Subset-Family of B
proofend;

:: (11.2) theorem TH40.
theorem Th36: :: RELSET_2:36
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = {} &amp; X <> {} holds
R .:^ X = {}
proofend;

theorem Th37: :: RELSET_2:37
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st R = [:A,B:] holds
R .:^ X = B
proofend;

theorem :: RELSET_2:38
for B, A being set
for X being Subset of A
for FR being Subset-Family of [:A,B:]
for G being Subset-Family of B st G =  {  (R .:^ X) where R is Subset of [:A,B:] : R in FR  }  holds
(Intersect FR) .:^ X = Intersect G
proofend;

theorem :: RELSET_2:39
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] st R1 c= R2 holds
R1 .:^ X c= R2 .:^ X
proofend;

theorem :: RELSET_2:40
for A, B being set
for X being Subset of A
for R1, R2 being Subset of [:A,B:] holds (R1 .:^ X) \/ (R2 .:^ X) c= (R1 \/ R2) .:^ X
proofend;

theorem Th41: :: RELSET_2:41
for y, x, A, B being set
for R being Subset of [:A,B:] holds
( y in Im ((R `),x) iff ( not [x,y] in R &amp; x in A &amp; y in B ) )
proofend;

theorem :: RELSET_2:42
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] st X <> {} holds
R .:^ X c= R .: X
proofend;

theorem Th43: :: RELSET_2:43
for A, B being set
for R being Subset of [:A,B:]
for X, Y being set holds
( X meets (R ~) .: Y iff ex x, y being set st
( x in X &amp; y in Y &amp; x in Im ((R ~),y) ) )
proofend;

theorem Th44: :: RELSET_2:44
for A, B being set
for R being Subset of [:A,B:]
for X, Y being set holds
( ex x, y being set st
( x in X &amp; y in Y &amp; x in Im ((R ~),y) ) iff Y meets R .: X )
proofend;

theorem Th45: :: RELSET_2:45
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Subset of [:A,B:] holds
( X misses (R ~) .: Y iff Y misses R .: X )
proofend;

theorem Th46: :: RELSET_2:46
for A, B being set
for R being Subset of [:A,B:]
for X being set holds R .: X = R .: (X /\ (proj1 R))
proofend;

theorem Th47: :: RELSET_2:47
for A, B being set
for R being Subset of [:A,B:]
for Y being set holds (R ~) .: Y = (R ~) .: (Y /\ (proj2 R))
proofend;

theorem Th48: :: RELSET_2:48
for A, B being set
for X being Subset of A
for R being Subset of [:A,B:] holds (R .:^ X) ` = (R `) .: X
proofend;

definition
let A, B, C be set ;
let R be Subset of [:A,B:];
let S be Subset of [:B,C:];
:: original:*
redefine funcR * S ->  Relation of A,C;
coherence
 R * S is Relation of A,C
proofend;
end;

theorem Th49: :: RELSET_2:49
for A, B being set
for X being Subset of A
for R being Relation of A,B holds (R .: X) ` = (R `) .:^ X
proofend;

:: (12) - FUNCT_5:20, RELAT_1:37
theorem Th50: :: RELSET_2:50
for B, A being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B &amp; proj2 R = R .: A )
proofend;

theorem :: RELSET_2:51
for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj1 (R * S) = (R ~) .: (proj1 S) &amp; proj1 (R * S) c= proj1 R )
proofend;

theorem :: RELSET_2:52
for A, B, C being set
for R being Relation of A,B
for S being Relation of B,C holds
( proj2 (R * S) = S .: (proj2 R) &amp; proj2 (R * S) c= proj2 S )
proofend;

theorem :: RELSET_2:53
for A, B being set
for X being Subset of A
for R being Relation of A,B holds
( X c= proj1 R iff X c= (R * (R ~)) .: X )
proofend;

theorem :: RELSET_2:54
for A, B being set
for Y being Subset of B
for R being Relation of A,B holds
( Y c= proj2 R iff Y c= ((R ~) * R) .: Y )
proofend;

theorem :: RELSET_2:55
for B, A being set
for R being Relation of A,B holds
( proj1 R = (R ~) .: B &amp; (R ~) .: (R .: A) = (R ~) .: (proj2 R) ) by Th50;

theorem :: RELSET_2:56
for B, A being set
for R being Relation of A,B holds (R ~) .: B = (R * (R ~)) .: A
proofend;

theorem :: RELSET_2:57
for A, B being set
for R being Relation of A,B holds R .: A = ((R ~) * R) .: B
proofend;

theorem :: RELSET_2:58
for A, B, C being set
for X being Subset of A
for R being Relation of A,B
for S being Relation of B,C holds S .:^ (R .: X) = ((R * (S `)) `) .:^ X
proofend;

theorem Th59: :: RELSET_2:59
for A, B being set
for R being Relation of A,B holds (R `) ~ = (R ~) `
proofend;

theorem Th60: :: RELSET_2:60
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ Y iff Y c= R .:^ X )
proofend;

theorem :: RELSET_2:61
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .: (X `) c= Y ` iff (R ~) .: Y c= X )
proofend;

theorem :: RELSET_2:62
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( X c= (R ~) .:^ (R .:^ X) &amp; Y c= R .:^ ((R ~) .:^ Y) ) by Th60;

theorem :: RELSET_2:63
for A, B being set
for X being Subset of A
for Y being Subset of B
for R being Relation of A,B holds
( R .:^ X = R .:^ ((R ~) .:^ (R .:^ X)) &amp; (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
proofend;

theorem :: RELSET_2:64
for A, B being set
for R being Relation of A,B holds (id A) * R = R * (id B)
proofend;