set M = { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } ;
defpred S1[ object , object ] means ( P1[$1,$2] & $1 in F3() & $2 in F2() );
A3:
for x, y being object st x in F1() & S1[x,y] holds
y in F2()
;
A4:
for x, y1, y2 being object st x in F1() & S1[x,y1] & S1[x,y2] holds
y1 = y2
by A2;
consider f being PartFunc of F1(),F2() such that
A5:
for x being object holds
( x in dom f iff ( x in F1() & ex y being object st S1[x,y] ) )
and
A6:
for x being object st x in dom f holds
S1[x,f . x]
from PARTFUN1:sch 2(A3, A4);
{ x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } = f .: F3()
proof
thus
{ x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } c= f .: F3()
XBOOLE_0:def 10 f .: F3() c= { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } proof
let x be
object ;
TARSKI:def 3 ( not x in { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } or x in f .: F3() )
assume
x in { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) }
;
x in f .: F3()
then consider u being
Element of
F2()
such that A7:
x = u
and A8:
ex
w being
Element of
F1() st
(
P1[
w,
u] &
w in F3() )
;
consider w being
Element of
F1()
such that A9:
P1[
w,
u]
and A10:
w in F3()
by A8;
A11:
w in dom f
by A5, A9, A10;
then
S1[
w,
f . w]
by A6;
then
f . w = x
by A2, A7, A9;
hence
x in f .: F3()
by A10, A11, FUNCT_1:def 6;
verum
end;
let x be
object ;
TARSKI:def 3 ( not x in f .: F3() or x in { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } )
assume
x in f .: F3()
;
x in { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) }
then consider y being
object such that A12:
y in dom f
and A13:
y in F3()
and A14:
x = f . y
by FUNCT_1:def 6;
reconsider x =
x as
Element of
F2()
by A6, A12, A14;
P1[
y,
x]
by A6, A12, A14;
hence
x in { x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) }
by A12, A13;
verum
end;
hence
{ x where x is Element of F2() : ex w being Element of F1() st
( P1[w,x] & w in F3() ) } is finite
by A1; verum