begin
:: deftheorem Def1 defines Relation-like RELAT_1:def 1 :
theorem
canceled;
theorem
canceled;
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
Lm1:
for x, y, X being set st [x,y] in X holds
( x in union (union X) & y in union (union X) )
:: deftheorem Def2 defines = RELAT_1:def 2 :
:: deftheorem Def3 defines c= RELAT_1:def 3 :
:: deftheorem Def4 defines proj1 RELAT_1:def 4 :
for
R,
b2 being
set holds
(
b2 = proj1 R iff for
x being
set holds
(
x in b2 iff ex
y being
set st
[x,y] in R ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th13:
theorem Th14:
theorem
:: deftheorem Def5 defines proj2 RELAT_1:def 5 :
for
R,
b2 being
set holds
(
b2 = proj2 R iff for
y being
set holds
(
y in b2 iff ex
x being
set st
[x,y] in R ) );
theorem
canceled;
theorem
canceled;
theorem
theorem
theorem
theorem Th21:
theorem
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem
:: deftheorem defines field RELAT_1:def 6 :
theorem
canceled;
theorem
theorem
theorem
theorem
theorem
definition
let R be
Relation;
func R ~ -> Relation means :
Def7:
for
x,
y being
set holds
(
[x,y] in it iff
[y,x] in R );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff [y,x] in R )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in R ) ) & ( for x, y being set holds
( [x,y] in b2 iff [y,x] in R ) ) holds
b1 = b2
involutiveness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff [y,x] in b2 ) ) holds
for x, y being set holds
( [x,y] in b2 iff [y,x] in b1 )
;
end;
:: deftheorem Def7 defines ~ RELAT_1:def 7 :
theorem
canceled;
theorem
canceled;
theorem Th37:
theorem
theorem
theorem
theorem
definition
let P,
R be
Relation;
func P * R -> Relation means :
Def8:
for
x,
y being
set holds
(
[x,y] in it iff ex
z being
set st
(
[x,z] in P &
[z,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ex z being set st
( [x,z] in P & [z,y] in R ) ) ) holds
b1 = b2
end;
:: deftheorem Def8 defines * RELAT_1:def 8 :
for
P,
R,
b3 being
Relation holds
(
b3 = P * R iff for
x,
y being
set holds
(
[x,y] in b3 iff ex
z being
set st
(
[x,z] in P &
[z,y] in R ) ) );
theorem
canceled;
theorem
canceled;
theorem Th44:
theorem Th45:
theorem
theorem
theorem Th48:
theorem Th49:
theorem
theorem
theorem
theorem
theorem
theorem Th55:
theorem Th56:
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th60:
theorem
canceled;
theorem Th62:
theorem
theorem Th64:
theorem
theorem
theorem
:: deftheorem Def9 defines non-empty RELAT_1:def 9 :
:: deftheorem Def10 defines id RELAT_1:def 10 :
for
X being
set for
b2 being
Relation holds
(
b2 = id X iff for
x,
y being
set holds
(
[x,y] in b2 iff (
x in X &
x = y ) ) );
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th71:
theorem
theorem
theorem Th74:
theorem Th75:
theorem Th76:
theorem Th77:
theorem
theorem Th79:
theorem
theorem
theorem
definition
let R be
Relation;
let X be
set ;
func R | X -> Relation means :
Def11:
for
x,
y being
set holds
(
[x,y] in it iff (
x in X &
[x,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( x in X & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( x in X & [x,y] in R ) ) ) holds
b1 = b2
end;
:: deftheorem Def11 defines | RELAT_1:def 11 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th86:
theorem Th87:
theorem Th88:
theorem Th89:
theorem Th90:
theorem
theorem
theorem
theorem
theorem
theorem Th96:
theorem Th97:
theorem
theorem Th99:
theorem Th100:
theorem
theorem
theorem
theorem Th104:
theorem Th105:
theorem Th106:
theorem Th107:
theorem
theorem
theorem
theorem
theorem
definition
let Y be
set ;
let R be
Relation;
func Y | R -> Relation means :
Def12:
for
x,
y being
set holds
(
[x,y] in it iff (
y in Y &
[x,y] in R ) );
existence
ex b1 being Relation st
for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) )
uniqueness
for b1, b2 being Relation st ( for x, y being set holds
( [x,y] in b1 iff ( y in Y & [x,y] in R ) ) ) & ( for x, y being set holds
( [x,y] in b2 iff ( y in Y & [x,y] in R ) ) ) holds
b1 = b2
end;
:: deftheorem Def12 defines | RELAT_1:def 12 :
for
Y being
set for
R,
b3 being
Relation holds
(
b3 = Y | R iff for
x,
y being
set holds
(
[x,y] in b3 iff (
y in Y &
[x,y] in R ) ) );
theorem
canceled;
theorem
canceled;
theorem Th115:
theorem Th116:
theorem Th117:
theorem Th118:
theorem Th119:
theorem
theorem
theorem
theorem
theorem Th124:
theorem Th125:
theorem
theorem Th127:
theorem
theorem
theorem
theorem Th131:
theorem Th132:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem Def13 defines .: RELAT_1:def 13 :
for
R being
Relation for
X,
b3 being
set holds
(
b3 = R .: X iff for
y being
set holds
(
y in b3 iff ex
x being
set st
(
[x,y] in R &
x in X ) ) );
theorem
canceled;
theorem
canceled;
theorem Th143:
theorem Th144:
theorem
theorem Th146:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th156:
theorem Th157:
theorem
theorem
theorem Th160:
theorem
theorem Th162:
theorem
:: deftheorem Def14 defines " RELAT_1:def 14 :
for
R being
Relation for
Y,
b3 being
set holds
(
b3 = R " Y iff for
x being
set holds
(
x in b3 iff ex
y being
set st
(
[x,y] in R &
y in Y ) ) );
theorem
canceled;
theorem
canceled;
theorem Th166:
theorem Th167:
theorem
theorem Th169:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th178:
theorem Th179:
theorem
theorem
theorem Th182:
theorem
begin
:: deftheorem Def15 defines empty-yielding RELAT_1:def 15 :
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Im RELAT_1:def 16 :
scheme
ExtensionalityR{
F1()
-> Relation,
F2()
-> Relation,
P1[
set ,
set ] } :
provided
A1:
for
a,
b being
set holds
(
[a,b] in F1() iff
P1[
a,
b] )
and A2:
for
a,
b being
set holds
(
[a,b] in F2() iff
P1[
a,
b] )
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
:: deftheorem defines Coim RELAT_1:def 17 :
theorem
theorem
:: deftheorem Def18 defines -defined RELAT_1:def 18 :
:: deftheorem Def19 defines -valued RELAT_1:def 19 :
LmX:
for X, Y being set holds
( {} is X -defined & {} is Y -valued )
theorem
theorem
theorem Th204:
theorem
theorem