:: Relations Defined on Sets
:: by Edmund Woronowicz
::
:: Received April 14, 1989
:: Copyright (c) 1990 Association of Mizar Users
:: deftheorem Def1 defines Relation RELSET_1:def 1 :
theorem :: RELSET_1:1
canceled;
theorem :: RELSET_1:2
canceled;
theorem :: RELSET_1:3
canceled;
:: deftheorem defines c= RELSET_1:def 2 :
:: deftheorem defines = RELSET_1:def 3 :
theorem :: RELSET_1:4
theorem :: RELSET_1:5
canceled;
theorem :: RELSET_1:6
for
a,
X,
Y being
set for
R being
Relation of
X,
Y st
a in R holds
ex
x,
y being
set st
(
a = [x,y] &
x in X &
y in Y )
theorem :: RELSET_1:7
canceled;
theorem :: RELSET_1:8
theorem :: RELSET_1:9
canceled;
theorem :: RELSET_1:10
canceled;
theorem :: RELSET_1:11
theorem Th12: :: RELSET_1:12
theorem :: RELSET_1:13
theorem :: RELSET_1:14
theorem :: RELSET_1:15
canceled;
theorem :: RELSET_1:16
canceled;
theorem :: RELSET_1:17
theorem :: RELSET_1:18
canceled;
theorem :: RELSET_1:19
theorem :: RELSET_1:20
canceled;
theorem :: RELSET_1:21
canceled;
theorem :: RELSET_1:22
for
Y,
X being
set for
R being
Relation of
X,
Y holds
( ( for
x being
set st
x in X holds
ex
y being
set st
[x,y] in R ) iff
dom R = X )
theorem :: RELSET_1:23
for
X,
Y being
set for
R being
Relation of
X,
Y holds
( ( for
y being
set st
y in Y holds
ex
x being
set st
[x,y] in R ) iff
rng R = Y )
theorem :: RELSET_1:24
theorem Th25: :: RELSET_1:25
theorem :: RELSET_1:26
canceled;
theorem :: RELSET_1:27
canceled;
theorem Th28: :: RELSET_1:28
theorem :: RELSET_1:29
theorem Th30: :: RELSET_1:30
theorem :: RELSET_1:31
theorem :: RELSET_1:32
theorem :: RELSET_1:33
theorem :: RELSET_1:34
for
Y,
X,
X1 being
set for
R being
Relation of
X,
Y st
X c= X1 holds
R | X1 = R
theorem :: RELSET_1:35
theorem :: RELSET_1:36
for
X,
Y,
Y1 being
set for
R being
Relation of
X,
Y st
Y c= Y1 holds
Y1 | R = R
theorem :: RELSET_1:37
canceled;
theorem Th38: :: RELSET_1:38
theorem :: RELSET_1:39
theorem :: RELSET_1:40
canceled;
theorem :: RELSET_1:41
canceled;
theorem :: RELSET_1:42
canceled;
theorem :: RELSET_1:43
canceled;
theorem :: RELSET_1:44
canceled;
theorem :: RELSET_1:45
canceled;
theorem :: RELSET_1:46
canceled;
theorem :: RELSET_1:47
theorem :: RELSET_1:48
theorem :: RELSET_1:49
theorem :: RELSET_1:50
theorem :: RELSET_1:51
theorem :: RELSET_1:52
theorem :: RELSET_1:53
theorem :: RELSET_1:54
for
N being
set for
R,
S being
Relation of
N st ( for
i being
set st
i in N holds
Im R,
i = Im S,
i ) holds
R = S
scheme :: RELSET_1:sch 4
Sch4{
F1()
-> set ,
F2()
-> set ,
P1[
set ,
set ],
F3()
-> Relation of
F1(),
F2(),
F4()
-> Relation of
F1(),
F2() } :
provided
A1:
for
p being
Element of
F1()
for
q being
Element of
F2() holds
(
[p,q] in F3() iff
P1[
p,
q] )
and A2:
for
p being
Element of
F1()
for
q being
Element of
F2() holds
(
[p,q] in F4() iff
P1[
p,
q] )
theorem :: RELSET_1:55