let X be set ; :: thesis: ( X is surreal-membered implies ex M being Ordinal st
for o being object st o in X holds
ex A being Ordinal st
( A in M & o in Day A ) )
assume A1: X is surreal-membered ; :: thesis: ex M being Ordinal st
for o being object st o in X holds
ex A being Ordinal st
( A in M & o in Day A )
defpred S₁[ object , object ] means ( $1 is Surreal & ( for z being Surreal st z = $1 holds
$2 = born z ) );
A2: for x, y, z being object st S₁[x,y] & S₁[x,z] holds
y = z

proof

let x, y, z be object ; :: thesis: ( S₁[x,y] & S₁[x,z] implies y = z )
assume A3: ( S₁[x,y] & S₁[x,z] ) ; :: thesis: y = z
reconsider x = x as Surreal by A3;
thus y = born x by A3
.= z by A3 ; :: thesis: verum

end;

consider OO being set such that
A4: for z being object holds
( z in OO iff ex y being object st
( y in X & S₁[y,z] ) ) from TARSKI_0:sch 1(A2);
for x being set st x in OO holds
x is ordinal

proof

let x be set ; :: thesis: ( x in OO implies x is ordinal )
assume x in OO ; :: thesis: x is ordinal
then consider y being object such that
A5: ( y in X & S₁[y,x] ) by A4;
reconsider y = y as Surreal by A5;
x = born y by A5;
hence x is ordinal ; :: thesis: verum

end;

then OO is ordinal-membered by ORDINAL6:1;
then reconsider U = union OO as Ordinal ;
take succ U ; :: thesis: for o being object st o in X holds
ex A being Ordinal st
( A in succ U & o in Day A )
let o be object ; :: thesis: ( o in X implies ex A being Ordinal st
( A in succ U & o in Day A ) )
assume A6: o in X ; :: thesis: ex A being Ordinal st
( A in succ U & o in Day A )
reconsider o = o as Surreal by A1, A6;
S₁[o, born o] ;
then born o c= U by A4, A6, ZFMISC_1:74;
then A7: born o in succ U by ORDINAL1:6, ORDINAL1:12;
o in Day (born o) by Def18;
hence ex A being Ordinal st
( A in succ U & o in Day A ) by A7; :: thesis: verum