consider Y being set such that
A2:
for y being set holds
( y in Y iff ex x being set st
( x in F1() & P1[x,y] ) )
from TARSKI:sch 1(A1);
defpred S1[ set ] means ex x, y being set st
( [x,y] = $1 & P1[x,y] );
consider F being set such that
A3:
for p being set holds
( p in F iff ( p in [:F1(),Y:] & S1[p] ) )
from XBOOLE_0:sch 1();
now thus
for
p being
set st
p in F holds
ex
x,
y being
set st
[x,y] = p
for x, y1, y2 being set st [x,y1] in F & [x,y2] in F holds
y1 = y2proof
let p be
set ;
( p in F implies ex x, y being set st [x,y] = p )
(
p in F implies ex
x,
y being
set st
(
[x,y] = p &
P1[
x,
y] ) )
by A3;
hence
(
p in F implies ex
x,
y being
set st
[x,y] = p )
;
verum
end; let x,
y1,
y2 be
set ;
( [x,y1] in F & [x,y2] in F implies y1 = y2 )assume
[x,y1] in F
;
( [x,y2] in F implies y1 = y2 )then consider x1,
z1 being
set such that A4:
[x1,z1] = [x,y1]
and A5:
P1[
x1,
z1]
by A3;
A6:
(
x = x1 &
z1 = y1 )
by A4, ZFMISC_1:33;
assume
[x,y2] in F
;
y1 = y2then consider x2,
z2 being
set such that A7:
[x2,z2] = [x,y2]
and A8:
P1[
x2,
z2]
by A3;
(
x = x2 &
z2 = y2 )
by A7, ZFMISC_1:33;
hence
y1 = y2
by A1, A5, A8, A6;
verum end;
then reconsider f = F as Function by Def1, RELAT_1:def 1;
take
f
; for x, y being set holds
( [x,y] in f iff ( x in F1() & P1[x,y] ) )
let x, y be set ; ( [x,y] in f iff ( x in F1() & P1[x,y] ) )
thus
( [x,y] in f implies ( x in F1() & P1[x,y] ) )
( x in F1() & P1[x,y] implies [x,y] in f )proof
assume A9:
[x,y] in f
;
( x in F1() & P1[x,y] )
then consider x1,
y1 being
set such that A10:
[x1,y1] = [x,y]
and A11:
P1[
x1,
y1]
by A3;
[x,y] in [:F1(),Y:]
by A3, A9;
hence
x in F1()
by ZFMISC_1:106;
P1[x,y]
x1 = x
by A10, ZFMISC_1:33;
hence
P1[
x,
y]
by A10, A11, ZFMISC_1:33;
verum
end;
assume that
A12:
x in F1()
and
A13:
P1[x,y]
; [x,y] in f
y in Y
by A2, A12, A13;
then
[x,y] in [:F1(),Y:]
by A12, ZFMISC_1:106;
hence
[x,y] in f
by A3, A13; verum