A3: now :: thesis: ( F2() <> {} implies ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) ) )
defpred S1[ object ] means ex y being object st P1[$1,y];
set y1 = the set ;
assume F2() <> {} ; :: thesis: ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) )
defpred S2[ object , object ] means ( ( ex y being object st P1[$1,y] implies P1[$1,$2] ) & ( ( for y being object holds P1[$1,y] ) implies $2 = the set ) );
A4: for x being object st x in F1() holds
ex z being object st S2[x,z]
proof
let x be object ; :: thesis: ( x in F1() implies ex z being object st S2[x,z] )
assume x in F1() ; :: thesis: ex z being object st S2[x,z]
( ( for y being object holds P1[x,y] ) implies ( ( ex y being object st P1[x,y] implies P1[x, the set ] ) & ( ( for y being object holds P1[x,y] ) implies the set = the set ) ) ) ;
hence ex z being object st S2[x,z] ; :: thesis: verum
end;
A5: for x, z1, z2 being object st x in F1() & S2[x,z1] & S2[x,z2] holds
z1 = z2 by A2;
consider g being Function such that
A6: dom g = F1() and
A7: for x being object st x in F1() holds
S2[x,g . x] from FUNCT_1:sch 2(A5, A4);
consider X being set such that
A8: for x being object holds
( x in X iff ( x in F1() & S1[x] ) ) from XBOOLE_0:sch 1();
set f = g | X;
A9: dom (g | X) c= F1() by A6, RELAT_1:60;
rng (g | X) c= F2()
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (g | X) or y in F2() )
assume y in rng (g | X) ; :: thesis: y in F2()
then consider x being object such that
A10: x in dom (g | X) and
A11: y = (g | X) . x by FUNCT_1:def 3;
A12: dom (g | X) c= X by RELAT_1:58;
then ( x in F1() & ex y being object st P1[x,y] ) by A8, A10;
then P1[x,g . x] by A7;
then A13: P1[x,y] by A10, A11, FUNCT_1:47;
x in F1() by A8, A10, A12;
hence y in F2() by A1, A13; :: thesis: verum
end;
then reconsider f = g | X as PartFunc of F1(),F2() by A9, RELSET_1:4;
take f = f; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) )
thus for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) :: thesis: for x being object st x in dom f holds
P1[x,f . x]
proof
let x be object ; :: thesis: ( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) )
dom f c= X by RELAT_1:58;
hence ( x in dom f implies ( x in F1() & ex y being object st P1[x,y] ) ) by A8; :: thesis: ( x in F1() & ex y being object st P1[x,y] implies x in dom f )
assume that
A14: x in F1() and
A15: ex y being object st P1[x,y] ; :: thesis: x in dom f
x in X by A8, A14, A15;
then x in (dom g) /\ X by A6, A14, XBOOLE_0:def 4;
hence x in dom f by RELAT_1:61; :: thesis: verum
end;
let x be object ; :: thesis: ( x in dom f implies P1[x,f . x] )
assume A16: x in dom f ; :: thesis: P1[x,f . x]
dom f c= X by RELAT_1:58;
then ex y being object st P1[x,y] by A8, A16;
then P1[x,g . x] by A7, A16;
hence P1[x,f . x] by A16, FUNCT_1:47; :: thesis: verum
end;
now :: thesis: ( F2() = {} implies ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) ) )
consider f being Function such that
A17: ( dom f c= F1() & rng f c= F2() ) by Lm1;
reconsider f = f as PartFunc of F1(),F2() by A17, RELSET_1:4;
assume A18: F2() = {} ; :: thesis: ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) )
take f = f; :: thesis: ( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) )
thus for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) by A1, A18; :: thesis: for x being object st x in dom f holds
P1[x,f . x]
thus for x being object st x in dom f holds
P1[x,f . x] by A18; :: thesis: verum
end;
hence ex f being PartFunc of F1(),F2() st
( ( for x being object holds
( x in dom f iff ( x in F1() & ex y being object st P1[x,y] ) ) ) & ( for x being object st x in dom f holds
P1[x,f . x] ) ) by A3; :: thesis: verum