defpred S1[ object ] means ex f being Function st
( $1 = f & dom f c= X & rng f c= Y );
consider F being set such that
A1:
for z being object holds
( z in F iff ( z in bool [:X,Y:] & S1[z] ) )
from XBOOLE_0:sch 1();
take
F
; for x being object holds
( x in F iff ex f being Function st
( x = f & dom f c= X & rng f c= Y ) )
let z be object ; ( z in F iff ex f being Function st
( z = f & dom f c= X & rng f c= Y ) )
thus
( z in F implies ex f being Function st
( z = f & dom f c= X & rng f c= Y ) )
by A1; ( ex f being Function st
( z = f & dom f c= X & rng f c= Y ) implies z in F )
given f being Function such that A2:
z = f
and
A3:
( dom f c= X & rng f c= Y )
; z in F
f c= [:X,Y:]
proof
let x,
y be
object ;
RELAT_1:def 3 ( not [x,y] in f or [x,y] in [:X,Y:] )
assume A4:
[x,y] in f
;
[x,y] in [:X,Y:]
reconsider y =
y as
set by TARSKI:1;
A5:
x in dom f
by XTUPLE_0:def 12, A4;
then
y = f . x
by A4, FUNCT_1:def 2;
then
y in rng f
by A5, FUNCT_1:def 3;
hence
[x,y] in [:X,Y:]
by A3, A5, ZFMISC_1:def 2;
verum
end;
hence
z in F
by A1, A2, A3; verum