let a, b, x, y be set ; :: thesis: for R being Relation st R = {[a,b],[x,y]} holds
( dom R = {a,x} & rng R = {b,y} )
let R be Relation; :: thesis: ( R = {[a,b],[x,y]} implies ( dom R = {a,x} & rng R = {b,y} ) )
assume A1: R = {[a,b],[x,y]} ; :: thesis: ( dom R = {a,x} & rng R = {b,y} )
for z being set holds
( z in dom R iff z in {a,x} )

proof

let z be set ; :: thesis: ( z in dom R iff z in {a,x} )
thus ( z in dom R implies z in {a,x} ) :: thesis: ( z in {a,x} implies z in dom R )

proof

assume z in dom R ; :: thesis: z in {a,x}
then consider c being set such that
A2: [z,c] in R by Def4;
( [z,c] = [a,b] or [z,c] = [x,y] ) by A1, A2, TARSKI:def 2;
then ( z = a or z = x ) by ZFMISC_1:33;
hence z in {a,x} by TARSKI:def 2; :: thesis: verum

end;

A3: now

assume z = a ; :: thesis: ( z in {a,x} implies z in dom R )
then [z,b] in R by A1, TARSKI:def 2;
hence ( z in {a,x} implies z in dom R ) by Def4; :: thesis: verum

end;

A4: now

assume z = x ; :: thesis: ( z in {a,x} implies z in dom R )
then [z,y] in R by A1, TARSKI:def 2;
hence ( z in {a,x} implies z in dom R ) by Def4; :: thesis: verum

end;

assume z in {a,x} ; :: thesis: z in dom R
hence z in dom R by A3, A4, TARSKI:def 2; :: thesis: verum

end;

hence dom R = {a,x} by TARSKI:2; :: thesis: rng R = {b,y}
for z being set holds
( z in rng R iff z in {b,y} )

proof

let z be set ; :: thesis: ( z in rng R iff z in {b,y} )
thus ( z in rng R implies z in {b,y} ) :: thesis: ( z in {b,y} implies z in rng R )

proof

assume z in rng R ; :: thesis: z in {b,y}
then consider d being set such that
A5: [d,z] in R by Def5;
( [d,z] = [a,b] or [d,z] = [x,y] ) by A1, A5, TARSKI:def 2;
then ( z = b or z = y ) by ZFMISC_1:33;
hence z in {b,y} by TARSKI:def 2; :: thesis: verum

end;

A6: now

assume z = b ; :: thesis: ( z in {b,y} implies z in rng R )
then [a,z] in R by A1, TARSKI:def 2;
hence ( z in {b,y} implies z in rng R ) by Def5; :: thesis: verum

end;

A7: now

assume z = y ; :: thesis: ( z in {b,y} implies z in rng R )
then [x,z] in R by A1, TARSKI:def 2;
hence ( z in {b,y} implies z in rng R ) by Def5; :: thesis: verum

end;

assume z in {b,y} ; :: thesis: z in rng R
hence z in rng R by A6, A7, TARSKI:def 2; :: thesis: verum

end;

hence rng R = {b,y} by TARSKI:2; :: thesis: verum