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


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

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

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

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

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

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

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

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)
proof end;

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

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

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

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

theorem :: RELSET_2:12
for x being object
for R1, R2 being Relation holds Im ((R1 \ R2),x) = (Im (R1,x)) \ (Im (R2,x))
proof end;

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

definition
let X, Y be set ;
let R be Relation of X,Y;
let x be object ;
:: original: Im
redefine func Im (R,x) -> Subset of Y;
coherence
Im (R,x) is Subset of Y
proof end;
:: original: Coim
redefine func Coim (R,x) -> Subset of X;
coherence
Coim (R,x) is Subset of X
proof end;
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 }
proof end;

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

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

theorem :: RELSET_2:17
for A, 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 }
proof end;

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
proof end;

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 ) )
proof end;
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
proof end;
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
proof end;

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

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))
proof end;

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);
proof end;
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)
proof end;

definition
let A, B be set ;
let X be Subset of A;
let R be Subset of [:A,B:];
func R .:^ 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 func R .:^ 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 = {} )
proof end;

theorem Th24: :: RELSET_2:24
for y being object
for A, B 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)
proof end;

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) )
proof end;

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
proof end;

:: 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)
proof end;

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
proof end;

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 by Th23, SETFAM_1:def 9;

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
proof end;

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
proof end;

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)
proof end;

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)
proof end;

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 }
proof end;

:: (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
proof end;

:: (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 = {} & X <> {} holds
R .:^ X = {}
proof end;

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
proof end;

theorem :: RELSET_2:38
for A, B 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
proof end;

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
proof end;

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
proof end;

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

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
proof end;

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 & y in Y & x in Im ((R ~),y) ) )
proof end;

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 & y in Y & x in Im ((R ~),y) ) iff Y meets R .: X )
proof end;

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 )
proof end;

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))
proof end;

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))
proof end;

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
proof end;

definition
let A, B, C be set ;
let R be Subset of [:A,B:];
let S be Subset of [:B,C:];
:: original: *
redefine func R * S -> Relation of A,C;
coherence
R * S is Relation of A,C
proof end;
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
proof end;

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

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) & proj1 (R * S) c= proj1 R )
proof end;

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) & proj2 (R * S) c= proj2 S )
proof end;

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 )
proof end;

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 )
proof end;

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

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

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

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
proof end;

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

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 )
proof end;

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 )
proof end;

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) & 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)) & (R ~) .:^ Y = (R ~) .:^ (R .:^ ((R ~) .:^ Y)) )
proof end;

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