let Y be set ; for R being Relation holds Y |` R = R /\ [:(dom R),Y:]
let R be Relation; Y |` R = R /\ [:(dom R),Y:]
set P = R /\ [:(dom R),Y:];
let x be object ; RELAT_1:def 2 for b being object holds
( [x,b] in Y |` R iff [x,b] in R /\ [:(dom R),Y:] )
let y be object ; ( [x,y] in Y |` R iff [x,y] in R /\ [:(dom R),Y:] )
thus
( [x,y] in Y |` R implies [x,y] in R /\ [:(dom R),Y:] )
( [x,y] in R /\ [:(dom R),Y:] implies [x,y] in Y |` R )proof
assume A1:
[x,y] in Y |` R
;
[x,y] in R /\ [:(dom R),Y:]
then A2:
y in Y
by Def10;
A3:
[x,y] in R
by A1, Def10;
then
x in dom R
by XTUPLE_0:def 12;
then
[x,y] in [:(dom R),Y:]
by A2, ZFMISC_1:def 2;
hence
[x,y] in R /\ [:(dom R),Y:]
by A3, XBOOLE_0:def 4;
verum
end;
assume A4:
[x,y] in R /\ [:(dom R),Y:]
; [x,y] in Y |` R
then
[x,y] in [:(dom R),Y:]
by XBOOLE_0:def 4;
then A5:
y in Y
by ZFMISC_1:87;
[x,y] in R
by A4, XBOOLE_0:def 4;
hence
[x,y] in Y |` R
by A5, Def10; verum