set D = [:F1(),F2():];
defpred S1[ set , set ] means for x, y being set st $1 = [x,y] holds
P1[x,y,$2];
A3:
for p, y1, y2 being set st p in [:F1(),F2():] & S1[p,y1] & S1[p,y2] holds
y1 = y2
proof
let p,
y1,
y2 be
set ;
:: thesis: ( p in [:F1(),F2():] & S1[p,y1] & S1[p,y2] implies y1 = y2 )
assume
p in [:F1(),F2():]
;
:: thesis: ( not S1[p,y1] or not S1[p,y2] or y1 = y2 )
then consider x1,
x2 being
set such that A4:
(
x1 in F1() &
x2 in F2() )
and A5:
p = [x1,x2]
by ZFMISC_1:def 2;
assume
( ( for
x,
y being
set st
p = [x,y] holds
P1[
x,
y,
y1] ) & ( for
x,
y being
set st
p = [x,y] holds
P1[
x,
y,
y2] ) )
;
:: thesis: y1 = y2
then
(
P1[
x1,
x2,
y1] &
P1[
x1,
x2,
y2] )
by A5;
hence
y1 = y2
by A1, A4;
:: thesis: verum
end;
A6:
for p being set st p in [:F1(),F2():] holds
ex z being set st S1[p,z]
proof
let p be
set ;
:: thesis: ( p in [:F1(),F2():] implies ex z being set st S1[p,z] )
assume
p in [:F1(),F2():]
;
:: thesis: ex z being set st S1[p,z]
then consider x1,
y1 being
set such that A7:
(
x1 in F1() &
y1 in F2() )
and A8:
p = [x1,y1]
by ZFMISC_1:def 2;
consider z being
set such that A9:
P1[
x1,
y1,
z]
by A2, A7;
take
z
;
:: thesis: S1[p,z]
let x,
y be
set ;
:: thesis: ( p = [x,y] implies P1[x,y,z] )
assume
p = [x,y]
;
:: thesis: P1[x,y,z]
then
(
x = x1 &
y = y1 )
by A8, ZFMISC_1:33;
hence
P1[
x,
y,
z]
by A9;
:: thesis: verum
end;
consider f being Function such that
A10:
dom f = [:F1(),F2():]
and
A11:
for p being set st p in [:F1(),F2():] holds
S1[p,f . p]
from FUNCT_1:sch 2(A3, A6);
take
f
; :: thesis: ( dom f = [:F1(),F2():] & ( for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . x,y] ) )
thus
dom f = [:F1(),F2():]
by A10; :: thesis: for x, y being set st x in F1() & y in F2() holds
P1[x,y,f . x,y]
let x, y be set ; :: thesis: ( x in F1() & y in F2() implies P1[x,y,f . x,y] )
assume
( x in F1() & y in F2() )
; :: thesis: P1[x,y,f . x,y]
then
[x,y] in [:F1(),F2():]
by ZFMISC_1:def 2;
hence
P1[x,y,f . x,y]
by A11; :: thesis: verum