defpred S2[ object , object ] means ex A being set st
( A = $2 & ( for y being object holds
( y in A iff ( y in F2($1) & P1[$1,y] ) ) ) );
A1:
for x being object st x in F1() holds
ex y being object st S2[x,y]
proof
let x be
object ;
( x in F1() implies ex y being object st S2[x,y] )
assume
x in F1()
;
ex y being object st S2[x,y]
defpred S3[
object ]
means P1[
x,$1];
consider Y being
set such that A2:
for
y being
object holds
(
y in Y iff (
y in F2(
x) &
S3[
y] ) )
from XBOOLE_0:sch 1();
take
Y
;
S2[x,Y]
reconsider A =
Y as
set ;
take
A
;
( A = Y & ( for y being object holds
( y in A iff ( y in F2(x) & P1[x,y] ) ) ) )
thus
(
A = Y & ( for
y being
object holds
(
y in A iff (
y in F2(
x) &
P1[
x,
y] ) ) ) )
by A2;
verum
end;
consider f being Function such that
A3:
dom f = F1()
and
A4:
for x being object st x in F1() holds
S2[x,f . x]
from CLASSES1:sch 1(A1);
take
f
; ( dom f = F1() & ( for x being object st x in F1() holds
for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) ) )
thus
dom f = F1()
by A3; for x being object st x in F1() holds
for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) )
let x be object ; ( x in F1() implies for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) ) )
assume
x in F1()
; for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) )
then consider A being set such that
A5:
A = f . x
and
A6:
for y being object holds
( y in A iff ( y in F2(x) & P1[x,y] ) )
by A4;
thus
for y being object holds
( y in f . x iff ( y in F2(x) & P1[x,y] ) )
by A5, A6; verum