A2:
for d being Element of F2() ex A being Ordinal st P1[d,A]
proof
let d be
Element of
F2();
ex A being Ordinal st P1[d,A]
consider a being
Ordinal of
F1()
such that A3:
P1[
d,
a]
by A1;
reconsider a =
a as
Ordinal ;
take
a
;
P1[d,a]
thus
P1[
d,
a]
by A3;
verum
end;
consider F being Function such that
A4:
dom F = F2()
and
A5:
for d being Element of F2() ex A being Ordinal st
( A = F . d & P1[d,A] & ( for B being Ordinal st P1[d,B] holds
A c= B ) )
from ORDINAL1:sch 6(A2);
take
F
; ( dom F = F2() & ( for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) ) ) )
thus
dom F = F2()
by A4; for d being Element of F2() ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
let d be Element of F2(); ex a being Ordinal of F1() st
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
consider A being Ordinal such that
A6:
( A = F . d & P1[d,A] )
and
A7:
for B being Ordinal st P1[d,B] holds
A c= B
by A5;
consider a being Ordinal of F1() such that
A8:
P1[d,a]
by A1;
A c= a
by A7, A8;
then reconsider a = A as Ordinal of F1() by CLASSES1:def 1;
take
a
; ( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
thus
( a = F . d & P1[d,a] & ( for b being Ordinal of F1() st P1[d,b] holds
a c= b ) )
by A6, A7; verum