let f be Function; :: thesis: ( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} )
( ( for y being object ex x being object st f " {y} c= {x} ) iff for y being object st y in rng f holds
ex x being object st f " {y} = {x} )
proof
thus ( ( for y being object ex x being object st f " {y} c= {x} ) implies for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) :: thesis: ( ( for y being object st y in rng f holds
ex x being object st f " {y} = {x} ) implies for y being object ex x being object st f " {y} c= {x} )
proof
assume A1: for y being object ex x being object st f " {y} c= {x} ; :: thesis: for y being object st y in rng f holds
ex x being object st f " {y} = {x}
let y be object ; :: thesis: ( y in rng f implies ex x being object st f " {y} = {x} )
consider x being object such that
A2: f " {y} c= {x} by A1;
assume y in rng f ; :: thesis: ex x being object st f " {y} = {x}
then consider x1 being object such that
A3: x1 in dom f and
A4: y = f . x1 by Def3;
take x ; :: thesis: f " {y} = {x}
f . x1 in {y} by A4, TARSKI:def 1;
then f " {y} <> {} by A3, Def7;
hence f " {y} = {x} by A2, ZFMISC_1:33; :: thesis: verum
end;
assume A5: for y being object st y in rng f holds
ex x being object st f " {y} = {x} ; :: thesis: for y being object ex x being object st f " {y} c= {x}
let y be object ; :: thesis: ex x being object st f " {y} c= {x}
A6: now :: thesis: ( not y in rng f implies ex x being set st f " {y} c= {x} )
set x = the set ;
assume A7: not y in rng f ; :: thesis: ex x being set st f " {y} c= {x}
take x = the set ; :: thesis: f " {y} c= {x}
rng f misses {y} by A7, ZFMISC_1:50;
then f " {y} = {} by RELAT_1:138;
hence f " {y} c= {x} ; :: thesis: verum
end;
now :: thesis: ( y in rng f implies ex x being object st f " {y} c= {x} )
assume y in rng f ; :: thesis: ex x being object st f " {y} c= {x}
then consider x being object such that
A8: f " {y} = {x} by A5;
take x = x; :: thesis: f " {y} c= {x}
thus f " {y} c= {x} by A8; :: thesis: verum
end;
hence ex x being object st f " {y} c= {x} by A6; :: thesis: verum
end;
hence ( f is one-to-one iff for y being object ex x being object st f " {y} c= {x} ) by Th73; :: thesis: verum