:: by Krzysztof Retel

::

:: Received April 25, 2005

:: Copyright (c) 2005-2021 Association of Mizar Users

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 ) )

for X being set holds

( y in {_{X}_} iff ex x being object st

( y = {x} & x in X ) )

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)

for B1, B2 being Subset-Family of M holds (Intersect B1) /\ (Intersect B2) c= Intersect (B1 /\ B2)

proof end;

theorem :: RELSET_2:13

for X being set

for R1, R2 being Relation holds (R1 /\ R2) .: {_{X}_} c= (R1 .: {_{X}_}) /\ (R2 .: {_{X}_})

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

redefine func Coim (R,x) -> Subset of X;

coherence

Coim (R,x) is Subset of X

end;
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: Coimredefine func Coim (R,x) -> Subset of X;

coherence

Coim (R,x) is Subset of X

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

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 :: 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

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 }

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

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;

ex b_{1} being Function st

( dom b_{1} = bool A & ( for X being set st X c= A holds

b_{1} . X = R .: X ) )

for b_{1}, b_{2} being Function st dom b_{1} = bool A & ( for X being set st X c= A holds

b_{1} . X = R .: X ) & dom b_{2} = bool A & ( for X being set st X c= A holds

b_{2} . X = R .: X ) holds

b_{1} = b_{2}

end;
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 ( dom it = bool A & ( for X being set st X c= A holds

it . X = R .: X ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof end;

:: deftheorem Def1 defines .: RELSET_2:def 1 :

for A being set

for R being Relation

for b_{3} being Function holds

( b_{3} = .: (R,A) iff ( dom b_{3} = bool A & ( for X being set st X c= A holds

b_{3} . X = R .: X ) ) );

for A being set

for R being Relation

for b

( b

b

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

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

definition

let A, B be set ;

let X be Subset of A;

let R be Subset of [:A,B:];

correctness

coherence

Intersect ((.: R) .: {_{X}_}) is set ;

;

end;
let X be Subset of A;

let R be Subset of [:A,B:];

correctness

coherence

Intersect ((.: R) .: {_{X}_}) is set ;

;

:: 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}_});

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

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 = {} )

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)

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) )

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

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

:: (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)

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

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 :: 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

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

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)

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)

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 }

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

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 = {}

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

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

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

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

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 ) )

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

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) ) )

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 )

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 )

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))

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))

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

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

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

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

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 :: 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 )

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 )

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 )

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 )

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

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

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 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 )

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 )

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

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)) )

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;