defpred S1[ Ordinal] means for z being Surreal st born_eq z = $1 holds
ex y being Surreal st
( y == z & y in (unique_No_op (born_eq z)) . (born_eq z) );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S1[C] ) holds
S1[D]
proof
let B be Ordinal; :: thesis: ( ( for C being Ordinal st C in B holds
S1[C] ) implies S1[B] )
assume A2: for C being Ordinal st C in B holds
S1[C] ; :: thesis: S1[B]
let z be Surreal; :: thesis: ( born_eq z = B implies ex y being Surreal st
( y == z & y in (unique_No_op (born_eq z)) . (born_eq z) ) )
assume A3: born_eq z = B ; :: thesis: ex y being Surreal st
( y == z & y in (unique_No_op (born_eq z)) . (born_eq z) )
set M = unique_No_op B;
consider X being Surreal such that
A4: ( born X = B & X == z ) by A3, Def5;
A5: born_eq X = born_eq z by A4, Th33;
defpred S2[ object , object ] means ( $1 is Surreal & $2 is Surreal & ( for a, b being Surreal st a = $1 & b = $2 holds
( b == a & b in (unique_No_op B) . (born_eq a) ) ) );
A6: for e being object st e in (L_ X) \/ (R_ X) holds
ex u being object st S2[e,u]
proof
let e1 be object ; :: thesis: ( e1 in (L_ X) \/ (R_ X) implies ex u being object st S2[e1,u] )
assume A7: e1 in (L_ X) \/ (R_ X) ; :: thesis: ex u being object st S2[e1,u]
then reconsider e = e1 as Surreal by SURREAL0:def 16;
A8: born e in born X by A7, Th1;
A9: born e in B by A4, A7, Th1;
consider E being Surreal such that
A10: ( born E = born_eq e & E == e ) by Def5;
born E in B by A9, ORDINAL1:12, A10, Def5;
then consider y being Surreal such that
A11: ( y == E & y in (unique_No_op (born_eq E)) . (born_eq E) ) by A2, A10, Th33;
take y ; :: thesis: S2[e1,y]
thus ( e1 is Surreal & y is Surreal ) by A7, SURREAL0:def 16; :: thesis: for a, b being Surreal st a = e1 & b = y holds
( b == a & b in (unique_No_op B) . (born_eq a) )
let a, b be Surreal; :: thesis: ( a = e1 & b = y implies ( b == a & b in (unique_No_op B) . (born_eq a) ) )
assume A12: ( a = e1 & b = y ) ; :: thesis: ( b == a & b in (unique_No_op B) . (born_eq a) )
hence b == a by A10, A11, Th4; :: thesis: b in (unique_No_op B) . (born_eq a)
A13: born_eq E = born E by Th33, A10;
born E in born_eq z by A8, A4, A3, A10, Def5, ORDINAL1:12;
then born E c= born_eq z by ORDINAL1:def 2;
hence b in (unique_No_op B) . (born_eq a) by A3, A11, A12, A10, A13, Th39; :: thesis: verum
end;
consider f being Function such that
A14: dom f = (L_ X) \/ (R_ X) and
A15: for e being object st e in (L_ X) \/ (R_ X) holds
S2[e,f . e] from CLASSES1:sch 1(A6);
 set fX1 = f .: (L_ X);
set fX2 = f .: (R_ X);
A16: f .: (L_ X) << f .: (R_ X)
proof
let l, r be Surreal; :: according to SURREAL0:def 20 :: thesis: ( not l in f .: (L_ X) or not r in f .: (R_ X) or not l >= r )
assume A17: ( l in f .: (L_ X) & r in f .: (R_ X) ) ; :: thesis: not l >= r
consider xL being object such that
A18: ( xL in dom f & xL in L_ X & l = f . xL ) by A17, FUNCT_1:def 6;
reconsider xL = xL as Surreal by A18, SURREAL0:def 16;
consider xR being object such that
A19: ( xR in dom f & xR in R_ X & r = f . xR ) by A17, FUNCT_1:def 6;
reconsider xR = xR as Surreal by A19, SURREAL0:def 16;
L_ X << R_ X by SURREAL0:45;
then ( l == xL & xL < xR ) by A19, A18, A14, A15;
then ( l < xR & xR == r ) by Th4, A19, A14, A15;
hence l < r by Th4; :: thesis: verum
end;
for o being object st o in (f .: (L_ X)) \/ (f .: (R_ X)) holds
ex O being Ordinal st
( O in B & o in Day O )
proof
let o be object ; :: thesis: ( o in (f .: (L_ X)) \/ (f .: (R_ X)) implies ex O being Ordinal st
( O in B & o in Day O ) )
assume o in (f .: (L_ X)) \/ (f .: (R_ X)) ; :: thesis: ex O being Ordinal st
( O in B & o in Day O )
then o in f .: ((L_ X) \/ (R_ X)) by RELAT_1:120;
then consider a being object such that
A20: ( a in dom f & a in (L_ X) \/ (R_ X) & o = f . a ) by FUNCT_1:def 6;
reconsider a = a as Surreal by A20, SURREAL0:def 16;
reconsider fa = f . a as Surreal by A20, A15;
take O = born_eq a; :: thesis: ( O in B & o in Day O )
fa in (unique_No_op B) . (born_eq a) by A20, A15;
then ( born_eq fa = born fa & born fa c= born_eq a ) by Th38;
then A21: ( fa in Day (born fa) & Day (born fa) c= Day (born_eq a) ) by SURREAL0:35, SURREAL0:def 18;
( born_eq a c= born a & born a in B ) by A4, A20, Th1, Def5;
hence ( O in B & o in Day O ) by A20, A21, ORDINAL1:12; :: thesis: verum
end;
then A22: [(f .: (L_ X)),(f .: (R_ X))] in Day B by A16, SURREAL0:46;
then reconsider fX = [(f .: (L_ X)),(f .: (R_ X))] as Surreal ;
A23: X = [(L_ X),(R_ X)] ;
A24: L_ X <=_ f .: (L_ X)
proof
let o be Surreal; :: according to SURREALO:def 3 :: thesis: ( o in L_ X implies ex y1, y2 being Surreal st
( y1 in f .: (L_ X) & y2 in f .: (L_ X) & y1 <= o & o <= y2 ) )
assume A25: o in L_ X ; :: thesis: ex y1, y2 being Surreal st
( y1 in f .: (L_ X) & y2 in f .: (L_ X) & y1 <= o & o <= y2 )
then A26: o in (L_ X) \/ (R_ X) by XBOOLE_0:def 3;
then reconsider fo = f . o as Surreal by A15;
take fo ; :: thesis: ex y2 being Surreal st
( fo in f .: (L_ X) & y2 in f .: (L_ X) & fo <= o & o <= y2 )
take fo ; :: thesis: ( fo in f .: (L_ X) & fo in f .: (L_ X) & fo <= o & o <= fo )
o == fo by A26, A15;
hence ( fo in f .: (L_ X) & fo in f .: (L_ X) & fo <= o & o <= fo ) by A25, A26, A14, FUNCT_1:def 6; :: thesis: verum
end;
A27: R_ X <=_ f .: (R_ X)
proof
let o be Surreal; :: according to SURREALO:def 3 :: thesis: ( o in R_ X implies ex y1, y2 being Surreal st
( y1 in f .: (R_ X) & y2 in f .: (R_ X) & y1 <= o & o <= y2 ) )
assume A28: o in R_ X ; :: thesis: ex y1, y2 being Surreal st
( y1 in f .: (R_ X) & y2 in f .: (R_ X) & y1 <= o & o <= y2 )
then A29: o in (L_ X) \/ (R_ X) by XBOOLE_0:def 3;
then reconsider fo = f . o as Surreal by A15;
take fo ; :: thesis: ex y2 being Surreal st
( fo in f .: (R_ X) & y2 in f .: (R_ X) & fo <= o & o <= y2 )
take fo ; :: thesis: ( fo in f .: (R_ X) & fo in f .: (R_ X) & fo <= o & o <= fo )
o == fo by A29, A15;
hence ( fo in f .: (R_ X) & fo in f .: (R_ X) & fo <= o & o <= fo ) by A28, A29, A14, FUNCT_1:def 6; :: thesis: verum
end;
A30: f .: (L_ X) <=_ L_ X
proof
let o be Surreal; :: according to SURREALO:def 3 :: thesis: ( o in f .: (L_ X) implies ex y1, y2 being Surreal st
( y1 in L_ X & y2 in L_ X & y1 <= o & o <= y2 ) )
assume o in f .: (L_ X) ; :: thesis: ex y1, y2 being Surreal st
( y1 in L_ X & y2 in L_ X & y1 <= o & o <= y2 )
then consider a being object such that
A31: ( a in dom f & a in L_ X & o = f . a ) by FUNCT_1:def 6;
reconsider a = a as Surreal by A31, SURREAL0:def 16;
take a ; :: thesis: ex y2 being Surreal st
( a in L_ X & y2 in L_ X & a <= o & o <= y2 )
take a ; :: thesis: ( a in L_ X & a in L_ X & a <= o & o <= a )
a == o by A31, A14, A15;
hence ( a in L_ X & a in L_ X & a <= o & o <= a ) by A31; :: thesis: verum
end;
A32: f .: (R_ X) <=_ R_ X
proof
let o be Surreal; :: according to SURREALO:def 3 :: thesis: ( o in f .: (R_ X) implies ex y1, y2 being Surreal st
( y1 in R_ X & y2 in R_ X & y1 <= o & o <= y2 ) )
assume o in f .: (R_ X) ; :: thesis: ex y1, y2 being Surreal st
( y1 in R_ X & y2 in R_ X & y1 <= o & o <= y2 )
then consider a being object such that
A33: ( a in dom f & a in R_ X & o = f . a ) by FUNCT_1:def 6;
reconsider a = a as Surreal by A33, SURREAL0:def 16;
take a ; :: thesis: ex y2 being Surreal st
( a in R_ X & y2 in R_ X & a <= o & o <= y2 )
take a ; :: thesis: ( a in R_ X & a in R_ X & a <= o & o <= a )
a == o by A33, A14, A15;
hence ( a in R_ X & a in R_ X & a <= o & o <= a ) by A33; :: thesis: verum
end;
( f .: (L_ X) <==> L_ X & f .: (R_ X) <==> R_ X ) by A30, A32, A24, A27;
then fX == X by A23, Th29;
then A34: fX in born_eq_set X by A22, A3, A5, Def6;
(L_ fX) \/ (R_ fX) c= union (rng ((unique_No_op B) | B))
proof
let o be object ; :: according to TARSKI:def 3 :: thesis: ( not o in (L_ fX) \/ (R_ fX) or o in union (rng ((unique_No_op B) | B)) )
assume o in (L_ fX) \/ (R_ fX) ; :: thesis: o in union (rng ((unique_No_op B) | B))
then o in f .: ((L_ X) \/ (R_ X)) by RELAT_1:120;
then consider a being object such that
A35: ( a in dom f & a in (L_ X) \/ (R_ X) & o = f . a ) by FUNCT_1:def 6;
reconsider a = a as Surreal by A35, SURREAL0:def 16;
reconsider fa = f . a as Surreal by A35, A15;
succ B = dom (unique_No_op B) by Def9;
then B c= dom (unique_No_op B) by ORDINAL1:def 2, ORDINAL1:6;
then A36: dom ((unique_No_op B) | B) = B by RELAT_1:62;
A37: fa in (unique_No_op B) . (born_eq a) by A35, A15;
A38: ( born_eq a c= born a & born a in B ) by A4, A35, Th1, Def5;
then A39: born_eq a in B by ORDINAL1:12;
(unique_No_op B) . (born_eq a) = ((unique_No_op B) | B) . (born_eq a) by A38, ORDINAL1:12, FUNCT_1:49;
then (unique_No_op B) . (born_eq a) in rng ((unique_No_op B) | B) by A39, A36, FUNCT_1:def 3;
hence o in union (rng ((unique_No_op B) | B)) by A35, A37, TARSKI:def 4; :: thesis: verum
end;
then fX in made_of (union (rng ((unique_No_op B) | B))) by Def8;
then reconsider Y = (born_eq_set X) /\ (made_of (union (rng ((unique_No_op B) | B)))) as non empty surreal-membered set by A34, XBOOLE_0:def 4;
set xx = the Y -smallest Surreal;
take the Y -smallest Surreal ; :: thesis: ( the Y -smallest Surreal == z & the Y -smallest Surreal in (unique_No_op (born_eq z)) . (born_eq z) )
the Y -smallest Surreal in Y by Def7;
then the Y -smallest Surreal in born_eq_set X by XBOOLE_0:def 4;
then A40: the Y -smallest Surreal == X by Def6;
A41: born_eq z = born_eq the Y -smallest Surreal by A40, Th33, A5;
A42: Y = (born_eq_set the Y -smallest Surreal) /\ (made_of (union (rng ((unique_No_op B) | B)))) by Th34, A40;
( B in succ B & succ B = dom (unique_No_op B) ) by Def9, ORDINAL1:6;
hence ( the Y -smallest Surreal == z & the Y -smallest Surreal in (unique_No_op (born_eq z)) . (born_eq z) ) by A40, A4, Th4, A3, A41, A42, Def9; :: thesis: verum
end;
for D being Ordinal holds S1[D] from ORDINAL1:sch 2(A1);
 hence ex b1 being Surreal st
( b1 == x & b1 in (unique_No_op (born_eq x)) . (born_eq x) ) ; :: thesis: verum