defpred S1[ object , object ] means ex A being Ordinal st
( A = $2 & P1[$1,A] & ( for B being Ordinal st P1[$1,B] holds
A c= B ) );
A2:
for x being object st x in F1() holds
ex y being object st S1[x,y]
proof
let x be
object ;
( x in F1() implies ex y being object st S1[x,y] )
assume
x in F1()
;
ex y being object st S1[x,y]
then reconsider d =
x as
Element of
F1() ;
defpred S2[
Ordinal]
means P1[
d,$1];
A3:
ex
A being
Ordinal st
S2[
A]
by A1;
consider A being
Ordinal such that A4:
(
S2[
A] & ( for
B being
Ordinal st
S2[
B] holds
A c= B ) )
from ORDINAL1:sch 1(A3);
reconsider y =
A as
set ;
take
y
;
S1[x,y]
take
A
;
( A = y & P1[x,A] & ( for B being Ordinal st P1[x,B] holds
A c= B ) )
thus
(
A = y &
P1[
x,
A] & ( for
B being
Ordinal st
P1[
x,
B] holds
A c= B ) )
by A4;
verum
end;
A5:
for x, y, z being object st x in F1() & S1[x,y] & S1[x,z] holds
y = z
proof
let x,
y,
z be
object ;
( x in F1() & S1[x,y] & S1[x,z] implies y = z )
assume
x in F1()
;
( not S1[x,y] or not S1[x,z] or y = z )
given A1 being
Ordinal such that A6:
A1 = y
and A7:
(
P1[
x,
A1] & ( for
B being
Ordinal st
P1[
x,
B] holds
A1 c= B ) )
;
( not S1[x,z] or y = z )
given A2 being
Ordinal such that A8:
A2 = z
and A9:
(
P1[
x,
A2] & ( for
B being
Ordinal st
P1[
x,
B] holds
A2 c= B ) )
;
y = z
(
A1 c= A2 &
A2 c= A1 )
by A7, A9;
hence
y = z
by A6, A8, XBOOLE_0:def 10;
verum
end;
consider F being Function such that
A10:
( dom F = F1() & ( for x being object st x in F1() holds
S1[x,F . x] ) )
from FUNCT_1:sch 2(A5, A2);
take
F
; ( dom F = F1() & ( for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) ) ) )
thus
dom F = F1()
by A10; for d being Element of F1() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
let d be Element of F1(); ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
thus
ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
by A10; verum