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