SURREALO

:: SURREALO semantic presentation

definition

func 1_No -> Surreal equals :: SURREALO:def 1
[{0_No},{}];

A1: {0_No} << {} ;
set b = born 0_No;
A2: 0_No in Day (born 0_No) by SURREAL0:def 18;
for o being object st o in {0_No} \/ {} holds
ex O being Ordinal st
( O in succ (born 0_No) & o in Day O )

proof

let o be object ; :: thesis:
assume o in {0_No} \/ {} ; :: thesis:
then o = 0_No by TARSKI:def 1;
hence ex O being Ordinal st
( O in succ (born 0_No) & o in Day O ) by A2, ORDINAL1:6; :: thesis:

end;

then [{0_No},{}] in Day (succ (born 0_No)) by A1, SURREAL0:46;
hence [{0_No},{}] is Surreal ; :: thesis:

end;

:: deftheorem defines 1_No SURREALO:def 1 :

theorem Th1: :: SURREALO:1

for x, y being Surreal st y in (L_ x) \/ (R_ x) holds
born y in born x

proof

let x, y be Surreal; :: thesis:
assume A1: y in (L_ x) \/ (R_ x) ; :: thesis:
A2: x = [(L_ x),(R_ x)] ;
x in Day (born x) by SURREAL0:def 18;
then consider O being Ordinal such that
A3: ( O in born x & y in Day O ) by SURREAL0:46, A1, A2;
born y c= O by A3, SURREAL0:def 18;
hence born y in born x by A3, ORDINAL1:12; :: thesis:

end;

theorem :: SURREALO:2

for x being Surreal holds
( L_ x <> {x} & {x} <> R_ x )

proof

let x be Surreal; :: thesis:
A1: x in {x} by TARSKI:def 1;
thus L_ x <> {x} :: thesis:

proof

assume L_ x = {x} ; :: thesis:
then x in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then born x in born x by Th1;
hence contradiction ; :: thesis:

end;

assume R_ x = {x} ; :: thesis:
then x in (L_ x) \/ (R_ x) by A1, XBOOLE_0:def 3;
then born x in born x by Th1;
hence contradiction ; :: thesis:

end;

theorem Th3: :: SURREALO:3

for x being Surreal holds x <= x

proof

let x be Surreal; :: thesis:
defpred S₁[ Ordinal] means for x being Surreal st x in Day $1 holds
x <= x;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x be Surreal; :: thesis:
assume A3: x in Day D ; :: thesis:
A4: x = [(L_ x),(R_ x)] ;
assume not x <= x ; :: thesis:

per cases by SURREAL0:43;

suppose not L_ x << {x} ; :: thesis:

then consider xl, r being Surreal such that
A5: ( xl in L_ x & r in {x} & r <= xl ) ;
xl in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then consider O being Ordinal such that
A6: ( O in D & xl in Day O ) by A4, A3, SURREAL0:46;
x <= xl by A5, TARSKI:def 1;
then A7: L_ x << {xl} by SURREAL0:43;
xl in {xl} by TARSKI:def 1;
hence contradiction by A6, A2, A5, A7; :: thesis:

end;

suppose not {x} << R_ x ; :: thesis:

then consider l, xr being Surreal such that
A8: ( l in {x} & xr in R_ x & xr <= l ) ;
xr in (L_ x) \/ (R_ x) by A8, XBOOLE_0:def 3;
then consider O being Ordinal such that
A9: ( O in D & xr in Day O ) by A4, A3, SURREAL0:46;
xr <= x by A8, TARSKI:def 1;
then A10: {xr} << R_ x by SURREAL0:43;
xr in {xr} by TARSKI:def 1;
hence contradiction by A9, A2, A8, A10; :: thesis:

end;

A11: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
ex A being Ordinal st x in Day A by SURREAL0:def 14;
hence x <= x by A11; :: thesis:

end;

theorem Th4: :: SURREALO:4

for x, y, z being Surreal st x <= y & y <= z holds
x <= z

proof

let x, y, z be Surreal; :: thesis:
defpred S₁[ Ordinal] means for x, y, z being Surreal st x <= y & y <= z & ((born x) (+) (born y)) (+) (born z) c= $1 holds
x <= z;
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x, y, z be Surreal; :: thesis:
assume that
A3: ( x <= y & y <= z ) and
A4: ((born x) (+) (born y)) (+) (born z) c= D ; :: thesis:

per cases by A4, ORDINAL1:11, XBOOLE_0:def 8;

suppose ((born x) (+) (born y)) (+) (born z) in D ; :: thesis:

hence x <= z by A2, A3; :: thesis:

end;

suppose A5: ((born x) (+) (born y)) (+) (born z) = D ; :: thesis:

assume not x <= z ; :: thesis:

per cases by SURREAL0:43;

suppose not L_ x << {z} ; :: thesis:

then consider xl, r being Surreal such that
A6: ( xl in L_ x & r in {z} & r <= xl ) ;
A7: z <= xl by A6, TARSKI:def 1;
xl in (L_ x) \/ (R_ x) by A6, XBOOLE_0:def 3;
then (born xl) (+) (born y) in (born x) (+) (born y) by Th1, ORDINAL7:94;
then ((born xl) (+) (born y)) (+) (born z) in D by A5, ORDINAL7:94;
then A8: ((born y) (+) (born z)) (+) (born xl) in D by ORDINAL7:68;
( L_ x << {y} & y in {y} ) by A3, SURREAL0:43, TARSKI:def 1;
hence contradiction by A6, A8, A7, A3, A2; :: thesis:

end;

suppose not {x} << R_ z ; :: thesis:

then consider l, zr being Surreal such that
A9: ( l in {x} & zr in R_ z & zr <= l ) ;
A10: zr <= x by A9, TARSKI:def 1;
zr in (L_ z) \/ (R_ z) by A9, XBOOLE_0:def 3;
then (born zr) (+) (born x) in (born z) (+) (born x) by Th1, ORDINAL7:94;
then ((born zr) (+) (born x)) (+) (born y) in ((born z) (+) (born x)) (+) (born y) by ORDINAL7:94;
then A11: ((born zr) (+) (born x)) (+) (born y) in D by A5, ORDINAL7:68;
( {y} << R_ z & y in {y} ) by A3, SURREAL0:43, TARSKI:def 1;
hence contradiction by A9, A11, A2, A3, A10; :: thesis:

end;

A12: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
S₁[((born x) (+) (born y)) (+) (born z)] by A12;
hence ( x <= y & y <= z implies x <= z ) ; :: thesis:

end;

theorem Th5: :: SURREALO:5

for x being Surreal holds
( L_ x <<= {x} & {x} <<= R_ x )

proof

defpred S₁[ Ordinal] means for x being Surreal st born x c= $1 holds
( L_ x <<= {x} & {x} <<= R_ x );
A1: for D being Ordinal st ( for C being Ordinal st C in D holds
S₁[C] ) holds
S₁[D]

proof

let D be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in D holds
S₁[C] ; :: thesis:
let x be Surreal; :: thesis:
assume A3: born x c= D ; :: thesis:

per cases by A3, ORDINAL1:11, XBOOLE_0:def 8;

suppose born x in D ; :: thesis:

hence ( L_ x <<= {x} & {x} <<= R_ x ) by A2; :: thesis:

end;

suppose A4: born x = D ; :: thesis:

thus L_ x <<= {x} :: thesis:

proof

given r, xl being Surreal such that A5: ( r in {x} & xl in L_ x & not xl <= r ) ; :: according to SURREAL0:def 19 :: thesis:
not xl <= x by A5, TARSKI:def 1;

per cases by SURREAL0:43;

suppose not L_ xl << {x} ; :: thesis:

then consider xll, X being Surreal such that
A6: ( xll in L_ xl & X in {x} & X <= xll ) ;
A7: x <= xll by A6, TARSKI:def 1;
A8: xl in {xl} by TARSKI:def 1;
xl in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then born xl in D by A4, Th1;
then L_ xl <<= {xl} by A2;
then xll <= xl by A8, A6;
then x <= xl by A7, Th4;
then L_ x << {xl} by SURREAL0:43;
hence contradiction by Th3, A5, A8; :: thesis:

end;

suppose not {xl} << R_ x ; :: thesis:

then consider X, xr being Surreal such that
A9: ( X in {xl} & xr in R_ x & xr <= X ) ;
A10: L_ x << R_ x by SURREAL0:45;
xr <= xl by A9, TARSKI:def 1;
hence contradiction by A10, A9, A5; :: thesis:

end;

thus {x} <<= R_ x :: thesis:

proof

given xr, l being Surreal such that A11: ( xr in R_ x & l in {x} & not l <= xr ) ; :: according to SURREAL0:def 19 :: thesis:
not x <= xr by A11, TARSKI:def 1;

per cases by SURREAL0:43;

suppose not {x} << R_ xr ; :: thesis:

then consider X, xrr being Surreal such that
A12: ( X in {x} & xrr in R_ xr & xrr <= X ) ;
A13: xrr <= x by A12, TARSKI:def 1;
A14: xr in {xr} by TARSKI:def 1;
xr in (L_ x) \/ (R_ x) by A11, XBOOLE_0:def 3;
then born xr in D by A4, Th1;
then {xr} <<= R_ xr by A2;
then xr <= xrr by A14, A12;
then xr <= x by A13, Th4;
then {xr} << R_ x by SURREAL0:43;
hence contradiction by A11, A14, Th3; :: thesis:

end;

suppose not L_ x << {xr} ; :: thesis:

then consider xl, X being Surreal such that
A15: ( xl in L_ x & X in {xr} & X <= xl ) ;
A16: L_ x << R_ x by SURREAL0:45;
xr <= xl by A15, TARSKI:def 1;
hence contradiction by A16, A15, A11; :: thesis:

end;

A17: for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
let x be Surreal; :: thesis:
S₁[ born x] by A17;
hence ( L_ x <<= {x} & {x} <<= R_ x ) ; :: thesis:

end;

theorem Th6: :: SURREALO:6

for x, y being Surreal st not y <= x holds
x <= y

proof

let x, y be Surreal; :: thesis:
assume A1: ( not y <= x & not x <= y ) ; :: thesis:

per cases by SURREAL0:43;

suppose not L_ x << {y} ; :: thesis:

then consider xl, Y being Surreal such that
A2: ( xl in L_ x & Y in {y} & Y <= xl ) ;
( L_ x <<= {x} & x in {x} ) by Th5, TARSKI:def 1;
then A3: xl <= x by A2;
y <= xl by A2, TARSKI:def 1;
hence contradiction by A1, A3, Th4; :: thesis:

end;

suppose not {x} << R_ y ; :: thesis:

then consider X, yr being Surreal such that
A4: ( X in {x} & yr in R_ y & yr <= X ) ;
( {y} <<= R_ y & y in {y} ) by Th5, TARSKI:def 1;
then A5: y <= yr by A4;
yr <= x by A4, TARSKI:def 1;
hence contradiction by A1, A5, Th4; :: thesis:

end;

theorem Th7: :: SURREALO:7

for A being Ordinal st A is finite holds
Day A is finite

proof

let A be Ordinal; :: thesis:
assume A1: A is finite ; :: thesis:
defpred S₁[ Nat] means Day $1 is finite ;
A2: S₁[ 0 ] by SURREAL0:2;
A3: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A4: S₁[n] ; :: thesis:
set n1 = n + 1;
Day (n + 1) c= [:(bool (Day n)),(bool (Day n)):]

proof

let o1, o2 be object ; :: according to RELAT_1:def 3 :: thesis:
assume A5: [o1,o2] in Day (n + 1) ; :: thesis:
reconsider o1 = o1, o2 = o2 as set by TARSKI:1;
A6: ( o1 c= o1 \/ o2 & o2 c= o1 \/ o2 ) by XBOOLE_1:7;
o1 \/ o2 c= Day n

proof

let a be object ; :: according to TARSKI:def 3 :: thesis:
assume a in o1 \/ o2 ; :: thesis:
then consider O being Ordinal such that
A7: ( O in n + 1 & a in Day O ) by A5, SURREAL0:46;
A8: O in Segm (n + 1) by A7;
then reconsider O = O as Nat ;
O < n + 1 by A8, NAT_1:44;
then O <= n by NAT_1:13;
then Segm O c= Segm n by NAT_1:39;
then Day O c= Day n by SURREAL0:35;
hence a in Day n by A7; :: thesis:

end;

then ( o1 c= Day n & o2 c= Day n ) by A6, XBOOLE_1:1;
hence [o1,o2] in [:(bool (Day n)),(bool (Day n)):] by ZFMISC_1:87; :: thesis:

end;

hence S₁[n + 1] by A4; :: thesis:

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A3);
hence Day A is finite by A1; :: thesis:

end;

theorem :: SURREALO:8

for x being Surreal st born x is finite holds
( L_ x is finite & R_ x is finite )

proof

let x be Surreal; :: thesis:
assume born x is finite ; :: thesis:
then A1: Day (born x) is finite by Th7;
A2: (L_ x) \/ (R_ x) c= Day (born x)

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A3: o in (L_ x) \/ (R_ x) ; :: thesis:
then reconsider y = o as Surreal by SURREAL0:def 16;
born y in born x by A3, Th1;
then ( y in Day (born y) & Day (born y) c= Day (born x) ) by SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
hence o in Day (born x) ; :: thesis:

end;

( L_ x c= (L_ x) \/ (R_ x) & R_ x c= (L_ x) \/ (R_ x) ) by XBOOLE_1:7;
hence ( L_ x is finite & R_ x is finite ) by A2, A1; :: thesis:

end;

definition

let x, y be Surreal;
:: original: >=
redefine pred x <= y;
reflexivity by Th3;
connectedness by Th6;

end;

notation

let x, y be Surreal;
synonym y >= x for x <= y;

end;

notation

let x, y be Surreal;
antonym y < x for x <= y;
antonym x > y for x <= y;

end;

definition

let x, y be Surreal;

pred x == y means :: SURREALO:def 2
( x <= y & y <= x );

reflexivity ;
symmetry ;

end;

:: deftheorem defines == SURREALO:def 2 :

theorem :: SURREALO:9

for x, y, z being Surreal st x <= y & y < z holds
x < z by Th4;

theorem :: SURREALO:10

for x, y, z being Surreal st x == y & y == z holds
x == z by Th4;

theorem Th11: :: SURREALO:11

for x being Surreal holds
( L_ x << {x} & {x} << R_ x )

proof

let x be Surreal; :: thesis:
thus L_ x << {x} :: thesis:

proof

let xl, X be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A1: ( xl in L_ x & X in {x} & xl >= X ) ; :: thesis:
xl >= x by A1, TARSKI:def 1;
then ( L_ x << {xl} & xl in {xl} ) by SURREAL0:43, TARSKI:def 1;
then not xl <= xl by A1;
hence contradiction ; :: thesis:

end;

let X, xr be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A2: ( X in {x} & xr in R_ x & X >= xr ) ; :: thesis:
xr <= x by A2, TARSKI:def 1;
then ( {xr} << R_ x & xr in {xr} ) by SURREAL0:43, TARSKI:def 1;
then not xr <= xr by A2;
hence contradiction ; :: thesis:

end;

theorem Th12: :: SURREALO:12

for S being non empty surreal-membered set st S is finite holds
ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) )

proof

defpred S₁[ Nat] means for S being non empty surreal-membered set st $1 = card S holds
ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) );
A1: S₁[ 0 ] ;
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis:
assume A3: S₁[n] ; :: thesis:
let S be non empty surreal-membered set ; :: thesis:
assume A4: n + 1 = card S ; :: thesis:
consider s being object such that
A5: s in S by XBOOLE_0:def 1;
reconsider s = s as Surreal by SURREAL0:def 16, A5;
set Ss = S \ {s};

per cases ;

suppose A6: S \ {s} is empty ; :: thesis:

take s ; :: thesis:
take s ; :: thesis:
thus ( s in S & s in S ) by A5; :: thesis:
let x be Surreal; :: thesis:
assume x in S ; :: thesis:
hence ( s <= x & x <= s ) by A6, ZFMISC_1:56; :: thesis:

end;

suppose A7: not S \ {s} is empty ; :: thesis:

card (S \ {s}) = n by A4, A5, STIRL2_1:55;
then consider Min, Max being Surreal such that
A8: ( Min in S \ {s} & Max in S \ {s} & ( for x being Surreal st x in S \ {s} holds
( Min <= x & x <= Max ) ) ) by A3, A7;
A9: Min <= Max by A8;

per cases ;

suppose A10: Max < s ; :: thesis:

take Min ; :: thesis:
take s ; :: thesis:
thus ( Min in S & s in S ) by A5, A8; :: thesis:
let x be Surreal; :: thesis:
assume x in S ; :: thesis:

per cases by ZFMISC_1:56;

suppose x in S \ {s} ; :: thesis:

then ( Min <= x & x <= Max ) by A8;
hence ( Min <= x & x <= s ) by A10, Th4; :: thesis:

end;

suppose x = s ; :: thesis:

hence ( Min <= x & x <= s ) by A9, A10, Th4; :: thesis:

end;

suppose A11: s < Min ; :: thesis:

take s ; :: thesis:
take Max ; :: thesis:
thus ( s in S & Max in S ) by A5, A8; :: thesis:
let x be Surreal; :: thesis:
assume x in S ; :: thesis:

per cases by ZFMISC_1:56;

suppose x in S \ {s} ; :: thesis:

then ( Min <= x & x <= Max ) by A8;
hence ( s <= x & x <= Max ) by A11, Th4; :: thesis:

end;

suppose x = s ; :: thesis:

hence ( s <= x & x <= Max ) by A9, A11, Th4; :: thesis:

end;

suppose A12: ( Min <= s & s <= Max ) ; :: thesis:

take Min ; :: thesis:
take Max ; :: thesis:
thus ( Min in S & Max in S ) by A8; :: thesis:
let x be Surreal; :: thesis:
assume x in S ; :: thesis:
then ( x in S \ {s} or x = s ) by ZFMISC_1:56;
hence ( Min <= x & x <= Max ) by A8, A12; :: thesis:

end;

A13: for n being Nat holds S₁[n] from NAT_1:sch 2(A1, A2);
let S be non empty surreal-membered set ; :: thesis:
assume S is finite ; :: thesis:
then card S is Nat ;
hence ex Min, Max being Surreal st
( Min in S & Max in S & ( for x being Surreal st x in S holds
( Min <= x & x <= Max ) ) ) by A13; :: thesis:

end;

theorem Th13: :: SURREALO:13

for x, y being Surreal holds
( not x < y or ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) )

proof

let x, y be Surreal; :: thesis:
assume x < y ; :: thesis:

per cases by SURREAL0:43;

suppose not L_ y << {x} ; :: thesis:

then consider l, r being Surreal such that
A1: ( l in L_ y & r in {x} & l >= r ) ;
( L_ y << {y} & y in {y} ) by Th11, TARSKI:def 1;
then ( x <= l & l < y ) by A1, TARSKI:def 1;
hence ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) ) by A1; :: thesis:

end;

suppose not {y} << R_ x ; :: thesis:

then consider l, r being Surreal such that
A2: ( l in {y} & r in R_ x & l >= r ) ;
( {x} << R_ x & x in {x} ) by Th11, TARSKI:def 1;
then ( x < r & r <= y ) by A2, TARSKI:def 1;
hence ( ex xR being Surreal st
( xR in R_ x & x < xR & xR <= y ) or ex yL being Surreal st
( yL in L_ y & x <= yL & yL < y ) ) by A2; :: thesis:

end;

theorem Th14: :: SURREALO:14

for x, y being Surreal st L_ y << {x} & {x} << R_ y holds
[((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal

proof

let x, y be Surreal; :: thesis:
assume A1: ( L_ y << {x} & {x} << R_ y ) ; :: thesis:
consider A being Ordinal such that
A2: x in Day A by SURREAL0:def 14;
consider B being Ordinal such that
A3: y in Day B by SURREAL0:def 14;
set X = (L_ x) \/ (L_ y);
set Y = (R_ x) \/ (R_ y);
A4: x = [(L_ x),(R_ x)] ;
then A5: L_ x << R_ x by A2, SURREAL0:46;
A6: y = [(L_ y),(R_ y)] ;
then A7: L_ y << R_ y by A3, SURREAL0:46;
A8: x in {x} by TARSKI:def 1;
A9: (L_ x) \/ (L_ y) << (R_ x) \/ (R_ y)

proof

let x1, y1 be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume ( x1 in (L_ x) \/ (L_ y) & y1 in (R_ x) \/ (R_ y) ) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose ( x1 in L_ x & y1 in R_ x ) ; :: thesis:

hence not x1 >= y1 by A5; :: thesis:

end;

suppose ( x1 in L_ y & y1 in R_ y ) ; :: thesis:

hence not x1 >= y1 by A7; :: thesis:

end;

suppose A10: ( x1 in L_ x & y1 in R_ y ) ; :: thesis:

then A11: ( x <= y1 & not x >= y1 ) by A8, A1;
L_ x << {x} by Th11;
hence not x1 >= y1 by A8, A10, A11, Th4; :: thesis:

end;

suppose A12: ( x1 in L_ y & y1 in R_ x ) ; :: thesis:

then A13: ( x1 <= x & not x1 >= x ) by A8, A1;
{x} << R_ x by Th11;
hence not x1 >= y1 by A8, A12, A13, Th4; :: thesis:

end;

for x being object st x in ((L_ x) \/ (L_ y)) \/ ((R_ x) \/ (R_ y)) holds
ex O being Ordinal st
( O in A \/ B & x in Day O )

proof

let z be object ; :: thesis:
assume z in ((L_ x) \/ (L_ y)) \/ ((R_ x) \/ (R_ y)) ; :: thesis:
then ( z in (L_ x) \/ (L_ y) or z in (R_ x) \/ (R_ y) ) by XBOOLE_0:def 3;

per cases by XBOOLE_0:def 3;

suppose ( z in L_ x or z in R_ x ) ; :: thesis:

then z in (L_ x) \/ (R_ x) by XBOOLE_0:def 3;
then consider O being Ordinal such that
A14: ( O in A & z in Day O ) by A4, A2, SURREAL0:46;
O in A \/ B by A14, XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in A \/ B & z in Day O ) by A14; :: thesis:

end;

suppose ( z in L_ y or z in R_ y ) ; :: thesis:

then z in (L_ y) \/ (R_ y) by XBOOLE_0:def 3;
then consider O being Ordinal such that
A15: ( O in B & z in Day O ) by A3, A6, SURREAL0:46;
O in A \/ B by A15, XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in A \/ B & z in Day O ) by A15; :: thesis:

end;

then [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] in Day (A \/ B) by SURREAL0:46, A9;
hence [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal ; :: thesis:

end;

theorem Th15: :: SURREALO:15

for x, y, z being Surreal st L_ y << {x} & {x} << R_ y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] holds
x == z

proof

let x, y, z be Surreal; :: thesis:
assume that
A1: ( L_ y << {x} & {x} << R_ y ) and
A2: z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] ; :: thesis:
A3: ( L_ x << {x} & {x} << R_ x ) by Th11;
A4: ( L_ z << {z} & {z} << R_ z ) by Th11;
A5: L_ z << {x}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A6: ( a in L_ z & b in {x} ) ; :: thesis:
then ( a in L_ x or a in L_ y ) by A2, XBOOLE_0:def 3;
hence a < b by A3, A6, A1; :: thesis:

end;

A7: {z} << R_ x

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A8: ( a in {z} & b in R_ x ) ; :: thesis:
then b in R_ z by A2, XBOOLE_0:def 3;
hence a < b by A8, A4; :: thesis:

end;

A9: L_ x << {z}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A10: ( a in L_ x & b in {z} ) ; :: thesis:
then a in L_ z by A2, XBOOLE_0:def 3;
hence a < b by A10, A4; :: thesis:

end;

{x} << R_ z

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A11: ( a in {x} & b in R_ z ) ; :: thesis:
then ( b in R_ x or b in R_ y ) by A2, XBOOLE_0:def 3;
hence a < b by A3, A11, A1; :: thesis:

end;

hence x == z by A7, A5, SURREAL0:43, A9; :: thesis:

end;

theorem Th16: :: SURREALO:16

for x, y being Surreal st L_ y << {x} & {x} << R_ y & ( for z being Surreal st L_ y << {z} & {z} << R_ y holds
born x c= born z ) holds
x == y

proof

let x, y be Surreal; :: thesis:
assume that
A1: ( L_ y << {x} & {x} << R_ y ) and
A2: for x1 being Surreal st L_ y << {x1} & {x1} << R_ y holds
born x c= born x1 ; :: thesis:
set X = (L_ x) \/ (L_ y);
set Y = (R_ x) \/ (R_ y);
A3: x in {x} by TARSKI:def 1;
reconsider z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] as Surreal by Th14, A1;
A4: ( L_ x << {x} & {x} << R_ x ) by Th11;
A5: ( L_ y << {y} & {y} << R_ y ) by Th11;
A6: ( L_ z << {z} & {z} << R_ z ) by Th11;
A7: L_ x << {z}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A8: ( a in L_ x & b in {z} ) ; :: thesis:
then a in L_ z by XBOOLE_0:def 3;
hence a < b by A8, A6; :: thesis:

end;

{x} << R_ z

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A9: ( a in {x} & b in R_ z ) ; :: thesis:
then ( b in R_ x or b in R_ y ) by XBOOLE_0:def 3;
hence a < b by A4, A9, A1; :: thesis:

end;

then A10: x <= z by A7, SURREAL0:43;
A11: L_ y << {z}

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A12: ( a in L_ y & b in {z} ) ; :: thesis:
then a < z by A1, A3, A10, Th4;
hence not a >= b by A12, TARSKI:def 1; :: thesis:

end;

A13: x == z by Th15, A1;
A14: {y} << R_ z

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A15: ( a in {y} & b in R_ z ) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose b in R_ y ; :: thesis:

hence not a >= b by A5, A15; :: thesis:

end;

suppose A16: b in R_ x ; :: thesis:

assume not a < b ; :: thesis:
then b <= y by A15, TARSKI:def 1;
then A17: {b} << R_ y by SURREAL0:43;
L_ y << {b}

proof

let c, d be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A18: ( c in L_ y & d in {b} ) ; :: thesis:
then c <= x by A3, A1;
then c < b by A4, A3, A16, Th4;
hence c < d by A18, TARSKI:def 1; :: thesis:

end;

then A19: born x c= born b by A17, A2;
A20: b in (L_ x) \/ (R_ x) by A16, XBOOLE_0:def 3;
then A21: born b in born x by Th1;
born b c= born x by A20, Th1, ORDINAL1:def 2;
then born b = born x by A19, XBOOLE_0:def 10;
hence contradiction by A21; :: thesis:

end;

A22: {z} << R_ y

proof

let a, b be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A23: ( a in {z} & b in R_ y ) ; :: thesis:
then z < b by A1, A3, A13, Th4;
hence not a >= b by A23, TARSKI:def 1; :: thesis:

end;

L_ z << {y}

proof

let b, a be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A24: ( b in L_ z & a in {y} ) ; :: thesis:

per cases by XBOOLE_0:def 3;

suppose b in L_ y ; :: thesis:

hence not b >= a by A5, A24; :: thesis:

end;

suppose A25: b in L_ x ; :: thesis:

assume not b < a ; :: thesis:
then y <= b by A24, TARSKI:def 1;
then A26: L_ y << {b} by SURREAL0:43;
{b} << R_ y

proof

let d, c be Surreal; :: according to SURREAL0:def 20 :: thesis:
assume A27: ( d in {b} & c in R_ y ) ; :: thesis:
then x <= c by A3, A1;
then b < c by A4, A3, A25, Th4;
hence d < c by A27, TARSKI:def 1; :: thesis:

end;

then A28: born x c= born b by A26, A2;
A29: b in (L_ x) \/ (R_ x) by A25, XBOOLE_0:def 3;
then A30: born b in born x by Th1;
born b c= born x by A29, Th1, ORDINAL1:def 2;
then born b = born x by A28, XBOOLE_0:def 10;
hence contradiction by A30; :: thesis:

end;

then z == y by A22, SURREAL0:43, A14, A11;
hence x == y by A13, Th4; :: thesis:

end;

theorem Th17: :: SURREALO:17

for X being set
for x, y being Surreal st X << {x} & x <= y holds
X << {y}

proof

let X be set ; :: thesis:
let x, y be Surreal; :: thesis:
assume A1: ( X << {x} & x <= y ) ; :: thesis:
let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A2: ( l in X & r in {y} ) ; :: thesis:
x in {x} by TARSKI:def 1;
then l < y by A1, Th4, A2;
hence not l >= r by A2, TARSKI:def 1; :: thesis:

end;

theorem Th18: :: SURREALO:18

for X being set
for x, y being Surreal st {x} << X & y <= x holds
{y} << X

proof

let X be set ; :: thesis:
let x, y be Surreal; :: thesis:
assume A1: ( {x} << X & y <= x ) ; :: thesis:
let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A2: ( l in {y} & r in X ) ; :: thesis:
x in {x} by TARSKI:def 1;
then y < r by A2, A1, Th4;
hence not l >= r by A2, TARSKI:def 1; :: thesis:

end;

theorem :: SURREALO:19

for x, y being Surreal st x == y holds
[((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal

proof

let x, y be Surreal; :: thesis:
assume A1: x == y ; :: thesis:
( L_ x << {x} & {x} << R_ x ) by Th11;
then ( L_ x << {y} & {y} << R_ x ) by A1, Th17, Th18;
hence [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] is Surreal by Th14; :: thesis:

end;

theorem :: SURREALO:20

for x, y, z being Surreal st x == y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] holds
x == z

proof

let x, y, z be Surreal; :: thesis:
assume A1: ( x == y & z = [((L_ x) \/ (L_ y)),((R_ x) \/ (R_ y))] ) ; :: thesis:
( L_ y << {y} & {y} << R_ y ) by Th11;
then ( L_ y << {x} & {x} << R_ y ) by A1, Th17, Th18;
hence x == z by A1, Th15; :: thesis:

end;

theorem Th21: :: SURREALO:21

for x, y being Surreal holds
( {x} << {y} iff x < y )

proof

let x, y be Surreal; :: thesis:

hereby :: thesis:

assume A1: {x} << {y} ; :: thesis:
( x in {x} & y in {y} ) by TARSKI:def 1;
hence x < y by A1; :: thesis:

end;

assume A2: x < y ; :: thesis:
let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume ( l in {x} & r in {y} ) ; :: thesis:
then ( l = x & r = y ) by TARSKI:def 1;
hence not l >= r by A2; :: thesis:

end;

theorem :: SURREALO:22

for x, y being Surreal holds
( [{x},{y}] is Surreal iff x < y )

proof

let x, y be Surreal; :: thesis:

hereby :: thesis:

assume [{x},{y}] is Surreal ; :: thesis:
then reconsider xy = [{x},{y}] as Surreal ;
( x in L_ xy & L_ xy << R_ xy & y in {y} ) by SURREAL0:45, TARSKI:def 1;
hence x < y ; :: thesis:

end;

assume A1: x < y ; :: thesis:
consider M being Ordinal such that
A2: for o being object st o in {x} \/ {y} holds
ex A being Ordinal st
( A in M & o in Day A ) by SURREAL0:47;
[{x},{y}] in Day M by A2, A1, Th21, SURREAL0:46;
hence [{x},{y}] is Surreal ; :: thesis:

end;

theorem Th23: :: SURREALO:23

for x, Max being Surreal st ( for y being Surreal st y in L_ x holds
y <= Max ) & Max in L_ x holds
( [{Max},(R_ x)] is Surreal & ( for y being Surreal st y = [{Max},(R_ x)] holds
( y == x & born y c= born x ) ) )

proof

let x, Max be Surreal; :: thesis:
assume that
A1: for y being Surreal st y in L_ x holds
y <= Max and
A2: Max in L_ x ; :: thesis:
A3: L_ x << R_ x by SURREAL0:45;
A4: {Max} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A5: ( l in {Max} & r in R_ x ) ; :: thesis:
l = Max by A5, TARSKI:def 1;
hence not l >= r by A3, A5, A2; :: thesis:

end;

for o being object st o in {Max} \/ (R_ x) holds
ex O being Ordinal st
( O in born x & o in Day O )

proof

let o be object ; :: thesis:
assume A6: o in {Max} \/ (R_ x) ; :: thesis:
( o = Max or o in R_ x ) by A6, ZFMISC_1:136;
then A7: o in (L_ x) \/ (R_ x) by A2, XBOOLE_0:def 3;
reconsider o = o as Surreal by SURREAL0:def 16, A6;
take born o ; :: thesis:
thus ( born o in born x & o in Day (born o) ) by SURREAL0:def 18, A7, Th1; :: thesis:

end;

then A8: [{Max},(R_ x)] in Day (born x) by A4, SURREAL0:46;
hence [{Max},(R_ x)] is Surreal ; :: thesis:
let y be Surreal; :: thesis:
assume A9: y = [{Max},(R_ x)] ; :: thesis:
A10: ( x = [(L_ x),(R_ x)] & y = [(L_ y),(R_ y)] ) ;
A11: for x1 being Surreal st x1 in L_ x holds
ex y1 being Surreal st
( y1 in L_ y & x1 <= y1 )

proof

let x1 be Surreal; :: thesis:
assume A12: x1 in L_ x ; :: thesis:
take Max ; :: thesis:
thus ( Max in L_ y & x1 <= Max ) by A12, A1, A9, TARSKI:def 1; :: thesis:

end;

A13: for x1 being Surreal st x1 in R_ y holds
ex y1 being Surreal st
( y1 in R_ x & y1 <= x1 ) by A9;
A14: for x1 being Surreal st x1 in L_ y holds
ex y1 being Surreal st
( y1 in L_ x & x1 <= y1 )

proof

let x1 be Surreal; :: thesis:
assume A15: x1 in L_ y ; :: thesis:
take Max ; :: thesis:
thus ( Max in L_ x & x1 <= Max ) by A15, A2, A9, TARSKI:def 1; :: thesis:

end;

for x1 being Surreal st x1 in R_ x holds
ex y1 being Surreal st
( y1 in R_ y & y1 <= x1 ) by A9;
hence ( y == x & born y c= born x ) by SURREAL0:def 18, A9, A8, A13, A10, A14, SURREAL0:44, A11; :: thesis:

end;

theorem Th24: :: SURREALO:24

for x, Min being Surreal st ( for y being Surreal st y in R_ x holds
Min <= y ) & Min in R_ x holds
( [(L_ x),{Min}] is Surreal & ( for y being Surreal st y = [(L_ x),{Min}] holds
( y == x & born y c= born x ) ) )

proof

let x, Min be Surreal; :: thesis:
assume that
A1: for y being Surreal st y in R_ x holds
Min <= y and
A2: Min in R_ x ; :: thesis:
A3: L_ x << R_ x by SURREAL0:45;
A4: L_ x << {Min}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A5: ( l in L_ x & r in {Min} ) ; :: thesis:
r = Min by A5, TARSKI:def 1;
hence not l >= r by A3, A5, A2; :: thesis:

end;

for o being object st o in (L_ x) \/ {Min} holds
ex O being Ordinal st
( O in born x & o in Day O )

proof

let o be object ; :: thesis:
assume A6: o in (L_ x) \/ {Min} ; :: thesis:
( o = Min or o in L_ x ) by A6, ZFMISC_1:136;
then A7: o in (L_ x) \/ (R_ x) by A2, XBOOLE_0:def 3;
reconsider o = o as Surreal by SURREAL0:def 16, A6;
take born o ; :: thesis:
thus ( born o in born x & o in Day (born o) ) by A7, Th1, SURREAL0:def 18; :: thesis:

end;

then A8: [(L_ x),{Min}] in Day (born x) by A4, SURREAL0:46;
hence [(L_ x),{Min}] is Surreal ; :: thesis:
let y be Surreal; :: thesis:
assume A9: y = [(L_ x),{Min}] ; :: thesis:
A10: ( x = [(L_ x),(R_ x)] & y = [(L_ y),(R_ y)] ) ;
A11: for x1 being Surreal st x1 in L_ x holds
ex y1 being Surreal st
( y1 in L_ y & x1 <= y1 ) by A9;
A12: for x1 being Surreal st x1 in R_ y holds
ex y1 being Surreal st
( y1 in R_ x & y1 <= x1 )

proof

let x1 be Surreal; :: thesis:
assume A13: x1 in R_ y ; :: thesis:
take Min ; :: thesis:
thus ( Min in R_ x & Min <= x1 ) by A9, A13, A2, TARSKI:def 1; :: thesis:

end;

A14: for x1 being Surreal st x1 in L_ y holds
ex y1 being Surreal st
( y1 in L_ x & x1 <= y1 ) by A9;
for x1 being Surreal st x1 in R_ x holds
ex y1 being Surreal st
( y1 in R_ y & y1 <= x1 )

proof

let x1 be Surreal; :: thesis:
assume A15: x1 in R_ x ; :: thesis:
take Min ; :: thesis:
thus ( Min in R_ y & Min <= x1 ) by A15, A1, A9, TARSKI:def 1; :: thesis:

end;

hence ( y == x & born y c= born x ) by A10, A14, SURREAL0:44, A12, A11, SURREAL0:def 18, A9, A8; :: thesis:

end;

theorem :: SURREALO:25

for X being set
for x, y, z, t being Surreal st x <= y & z = [{x,y},X] & t = [{y},X] holds
z == t

proof

let X be set ; :: thesis:
let x, y, z, t be Surreal; :: thesis:
assume A1: ( x <= y & z = [{x,y},X] & t = [{y},X] ) ; :: thesis:
A2: for s being Surreal st s in L_ z holds
s <= y by A1, TARSKI:def 2;
A3: y in L_ z by A1, TARSKI:def 2;
t = [{y},(R_ z)] by A1;
hence z == t by A2, A3, Th23; :: thesis:

end;

theorem :: SURREALO:26

for X being set
for x, y, z being Surreal st z = [{x,y},X] holds
[{x},X] is Surreal

proof

let X be set ; :: thesis:
let x, y, z be Surreal; :: thesis:
set b = born z;
assume A1: z = [{x,y},X] ; :: thesis:
A2: z in Day (born z) by SURREAL0:def 18;
then A3: ( {x,y} << X & ( for o being object st o in {x,y} \/ X holds
ex O being Ordinal st
( O in born z & o in Day O ) ) ) by A1, SURREAL0:46;
A4: {x} << X

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A5: ( l in {x} & r in X ) ; :: thesis:
then l = x by TARSKI:def 1;
then l in {x,y} by TARSKI:def 2;
hence not l >= r by A3, A5; :: thesis:

end;

for o being object st o in {x} \/ X holds
ex O being Ordinal st
( O in born z & o in Day O )

proof

let o be object ; :: thesis:
assume o in {x} \/ X ; :: thesis:
then ( o in {x} or o in X ) by XBOOLE_0:def 3;
then ( o = x or o in X ) by TARSKI:def 1;
then ( o in {x,y} or o in X ) by TARSKI:def 2;
then o in {x,y} \/ X by XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in born z & o in Day O ) by A2, A1, SURREAL0:46; :: thesis:

end;

then [{x},X] in Day (born z) by A4, SURREAL0:46;
hence [{x},X] is Surreal ; :: thesis:

end;

theorem :: SURREALO:27

for X being set
for x, y, z, t being Surreal st x <= y & z = [X,{x,y}] & t = [X,{x}] holds
z == t

proof

let X be set ; :: thesis:
let x, y, z, t be Surreal; :: thesis:
assume A1: ( x <= y & z = [X,{x,y}] & t = [X,{x}] ) ; :: thesis:
A2: for s being Surreal st s in R_ z holds
x <= s by A1, TARSKI:def 2;
A3: x in R_ z by A1, TARSKI:def 2;
t = [(L_ z),{x}] by A1;
hence z == t by A2, A3, Th24; :: thesis:

end;

theorem :: SURREALO:28

for X being set
for x, y, z being Surreal st z = [X,{x,y}] holds
[X,{x}] is Surreal

proof

let X be set ; :: thesis:
let x, y, z be Surreal; :: thesis:
set b = born z;
assume A1: z = [X,{x,y}] ; :: thesis:
A2: z in Day (born z) by SURREAL0:def 18;
then A3: ( X << {x,y} & ( for o being object st o in X \/ {x,y} holds
ex O being Ordinal st
( O in born z & o in Day O ) ) ) by A1, SURREAL0:46;
A4: X << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A5: ( l in X & r in {x} ) ; :: thesis:
then r = x by TARSKI:def 1;
then r in {x,y} by TARSKI:def 2;
hence not l >= r by A3, A5; :: thesis:

end;

for o being object st o in X \/ {x} holds
ex O being Ordinal st
( O in born z & o in Day O )

proof

let o be object ; :: thesis:
assume o in X \/ {x} ; :: thesis:
then ( o in {x} or o in X ) by XBOOLE_0:def 3;
then ( o = x or o in X ) by TARSKI:def 1;
then ( o in {x,y} or o in X ) by TARSKI:def 2;
then o in {x,y} \/ X by XBOOLE_0:def 3;
hence ex O being Ordinal st
( O in born z & o in Day O ) by A2, A1, SURREAL0:46; :: thesis:

end;

then [X,{x}] in Day (born z) by A4, SURREAL0:46;
hence [X,{x}] is Surreal ; :: thesis:

end;

definition

let X, Y be set ;

pred X <=_ Y means :Def3: :: SURREALO:def 3
for x being Surreal st x in X holds
ex y1, y2 being Surreal st
( y1 in Y & y2 in Y & y1 <= x & x <= y2 );

reflexivity ;

end;

:: deftheorem Def3 defines <=_ SURREALO:def 3 :

definition

let X, Y be set ;

pred X <==> Y means :: SURREALO:def 4
( X <=_ Y & Y <=_ X );

reflexivity ;
symmetry ;

end;

:: deftheorem defines <==> SURREALO:def 4 :

theorem Th29: :: SURREALO:29

for x, y being Surreal
for X1, X2, Y1, Y2 being set st X1 <==> X2 & Y1 <==> Y2 & x = [X1,Y1] & y = [X2,Y2] holds
x == y

proof

let x, y be Surreal; :: thesis:
let X1, X2, Y1, Y2 be set ; :: thesis:
assume A1: ( X1 <==> X2 & Y1 <==> Y2 & x = [X1,Y1] & y = [X2,Y2] ) ; :: thesis:

A2: now :: thesis:

let x be Surreal; :: thesis:
assume x in X1 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in X2 & y2 in X2 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in X2 & x <= y ) ; :: thesis:

end;

A3: now :: thesis:

let x be Surreal; :: thesis:
assume x in Y2 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in Y1 & y2 in Y1 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in Y1 & y <= x ) ; :: thesis:

end;

A4: now :: thesis:

let x be Surreal; :: thesis:
assume x in X2 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in X1 & y2 in X1 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in X1 & x <= y ) ; :: thesis:

end;

now :: thesis:

let x be Surreal; :: thesis:
assume x in Y1 ; :: thesis:
then ex y1, y2 being Surreal st
( y1 in Y2 & y2 in Y2 & y1 <= x & x <= y2 ) by A1, Def3;
hence ex y being Surreal st
( y in Y2 & y <= x ) ; :: thesis:

end;

hence x == y by SURREAL0:44, A1, A2, A3, A4; :: thesis:

end;

theorem :: SURREALO:30

for X, Y being set st X c= Y holds
X <=_ Y ;

theorem :: SURREALO:31

for X1, X2, Y1, Y2 being set st X1 <=_ X2 & Y1 <=_ Y2 holds
X1 \/ Y1 <=_ X2 \/ Y2

proof

let X1, X2, Y1, Y2 be set ; :: thesis:
assume A1: ( X1 <=_ X2 & Y1 <=_ Y2 ) ; :: thesis:
let x be Surreal; :: according to SURREALO:def 3 :: thesis:
assume A2: x in X1 \/ Y1 ; :: thesis:

per cases by A2, XBOOLE_0:def 3;

suppose x in X1 ; :: thesis:

then consider x2, x3 being Surreal such that
A3: ( x2 in X2 & x3 in X2 & x2 <= x & x <= x3 ) by A1;
take x2 ; :: thesis:
take x3 ; :: thesis:
thus ( x2 in X2 \/ Y2 & x3 in X2 \/ Y2 & x2 <= x & x <= x3 ) by A3, XBOOLE_0:def 3; :: thesis:

end;

suppose x in Y1 ; :: thesis:

then consider y2, y3 being Surreal such that
A4: ( y2 in Y2 & y3 in Y2 & y2 <= x & x <= y3 ) by A1;
take y2 ; :: thesis:
take y3 ; :: thesis:
thus ( y2 in X2 \/ Y2 & y3 in X2 \/ Y2 & y2 <= x & x <= y3 ) by A4, XBOOLE_0:def 3; :: thesis:

end;

theorem :: SURREALO:32

for x, y being Surreal st x == y holds
{x} <=_ {y}

proof

let x, y be Surreal; :: thesis:
assume A1: x == y ; :: thesis:
let z be Surreal; :: according to SURREALO:def 3 :: thesis:
assume A2: z in {x} ; :: thesis:
take y ; :: thesis:
take y ; :: thesis:
thus ( y in {y} & y in {y} & y <= z & z <= y ) by A1, A2, TARSKI:def 1; :: thesis:

end;

definition

let x be Surreal;

func born_eq x -> Ordinal means :Def5: :: SURREALO:def 5
( ex y being Surreal st
( born y = it & y == x ) & ( for y being Surreal st y == x holds
it c= born y ) );

existence

proof

defpred S₁[ Ordinal] means ex y being Surreal st
( born y = $1 & y == x );
S₁[ born x] ;
then A1: ex O being Ordinal st S₁[O] ;
consider A being Ordinal such that
A2: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A1);
take A ; :: thesis:
thus ex y being Surreal st
( born y = A & y == x ) by A2; :: thesis:
let y be Surreal; :: thesis:
assume y == x ; :: thesis:
hence A c= born y by A2; :: thesis:

end;

uniqueness

proof

let it1, it2 be Ordinal; :: thesis:
assume that
A3: ( ex y being Surreal st
( born y = it1 & y == x ) & ( for y being Surreal st y == x holds
it1 c= born y ) ) and
A4: ( ex y being Surreal st
( born y = it2 & y == x ) & ( for y being Surreal st y == x holds
it2 c= born y ) ) ; :: thesis:
( it1 c= it2 & it2 c= it1 ) by A3, A4;
hence it1 = it2 by XBOOLE_0:def 10; :: thesis:

end;

:: deftheorem Def5 defines born_eq SURREALO:def 5 :

definition

let x be Surreal;

func born_eq_set x -> surreal-membered set means :Def6: :: SURREALO:def 6
for y being Surreal holds
( y in it iff ( y == x & y in Day (born_eq x) ) );

existence

proof

defpred S₁[ object ] means for y being Surreal st y = $1 holds
x == y;
consider X being set such that
A1: for o being object holds
( o in X iff ( o in Day (born_eq x) & S₁[o] ) ) from XBOOLE_0:sch 1();
X is surreal-membered

proof

let o be object ; :: according to SURREAL0:def 16 :: thesis:
thus ( not o in X or o is surreal ) by A1; :: thesis:

end;

then reconsider X = X as surreal-membered set ;
take X ; :: thesis:
let y be Surreal; :: thesis:
thus ( y in X implies ( y == x & y in Day (born_eq x) ) ) by A1; :: thesis:
assume A2: ( y == x & y in Day (born_eq x) ) ; :: thesis:
then S₁[y] ;
hence y in X by A1, A2; :: thesis:

end;

uniqueness

proof

let IT1, IT2 be surreal-membered set ; :: thesis:
assume that
A3: for y being Surreal holds
( y in IT1 iff ( y == x & y in Day (born_eq x) ) ) and
A4: for y being Surreal holds
( y in IT2 iff ( y == x & y in Day (born_eq x) ) ) ; :: thesis:
thus IT1 c= IT2 :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A5: o in IT1 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o == x & o in Day (born_eq x) ) by A3, A5;
hence o in IT2 by A4; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A6: o in IT2 ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
( o == x & o in Day (born_eq x) ) by A4, A6;
hence o in IT1 by A3; :: thesis:

end;

:: deftheorem Def6 defines born_eq_set SURREALO:def 6 :

registration

let x be Surreal;

cluster born_eq_set x -> non empty surreal-membered ;

coherence

proof

consider y being Surreal such that
A1: ( born y = born_eq x & y == x ) by Def5;
y in Day (born y) by SURREAL0:def 18;
hence not born_eq_set x is empty by A1, Def6; :: thesis:

end;

definition

let A be non empty surreal-membered set ;
let x be Surreal;

attr x is A -smallest means :Def7: :: SURREALO:def 7
( x in A & ( for y being Surreal st y in A & y == x holds
(card (L_ x)) (+) (card (R_ x)) c= (card (L_ y)) (+) (card (R_ y)) ) );

end;

:: deftheorem Def7 defines -smallest SURREALO:def 7 :

registration

let A be non empty surreal-membered set ;

cluster non empty V9() surreal A -smallest for set ;

existence

proof

consider x being object such that
A1: x in A by XBOOLE_0:def 1;
reconsider x = x as Surreal by A1, SURREAL0:def 16;
defpred S₁[ Ordinal] means ex y being Surreal st
( y in A & y == x & (card (L_ y)) (+) (card (R_ y)) = A );
S₁[(card (L_ x)) (+) (card (R_ x))] by A1;
then A2: ex O being Ordinal st S₁[O] ;
consider O being Ordinal such that
A3: ( S₁[O] & ( for B being Ordinal st S₁[B] holds
O c= B ) ) from ORDINAL1:sch 1(A2);
consider y being Surreal such that
A4: ( y in A & y == x & (card (L_ y)) (+) (card (R_ y)) = O ) by A3;
for z being Surreal st z in A & z == y holds
(card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z))

proof

let z be Surreal; :: thesis:
assume A5: ( z in A & z == y ) ; :: thesis:
then z == x by A4, Th4;
hence (card (L_ y)) (+) (card (R_ y)) c= (card (L_ z)) (+) (card (R_ z)) by A5, A3, A4; :: thesis:

end;

hence ex b₁ being Surreal st b₁ is A -smallest by A4, Def7; :: thesis:

end;

theorem Th33: :: SURREALO:33

for x, y being Surreal st x == y holds
born_eq x = born_eq y

proof

let x, y be Surreal; :: thesis:
assume A1: x == y ; :: thesis:
consider z being Surreal such that
A2: ( born z = born_eq x & z == x ) by Def5;
z == y by A1, A2, Th4;
then A3: born_eq y c= born_eq x by A2, Def5;
consider t being Surreal such that
A4: ( born t = born_eq y & t == y ) by Def5;
t == x by A1, A4, Th4;
then born_eq x c= born_eq y by A4, Def5;
hence born_eq x = born_eq y by A3, XBOOLE_0:def 10; :: thesis:

end;

Lm1: for x, y being Surreal st x == y holds
born_eq_set x c= born_eq_set y

proof

let x, y be Surreal; :: thesis:
assume A1: x == y ; :: thesis:
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: o in born_eq_set x ; :: thesis:
then reconsider o = o as Surreal by SURREAL0:def 16;
A3: born_eq x = born_eq y by A1, Th33;
A4: ( o == x & o in Day (born_eq x) ) by A2, Def6;
then o == y by A1, Th4;
hence o in born_eq_set y by A3, A4, Def6; :: thesis:

end;

theorem Th34: :: SURREALO:34

for x, y being Surreal st x == y holds
born_eq_set x = born_eq_set y

proof

let x, y be Surreal; :: thesis:
assume x == y ; :: thesis:
then ( born_eq_set x c= born_eq_set y & born_eq_set y c= born_eq_set x ) by Lm1;
hence born_eq_set x = born_eq_set y by XBOOLE_0:def 10; :: thesis:

end;

theorem :: SURREALO:35

for x, y being Surreal st y in born_eq_set x holds
( born y = born_eq y & born_eq y = born_eq x )

proof

let x, y be Surreal; :: thesis:
assume A1: y in born_eq_set x ; :: thesis:
then y in Day (born_eq x) by Def6;
then A2: born y c= born_eq x by SURREAL0:def 18;
x == y by A1, Def6;
then A3: born_eq x = born_eq y by Th33;
born_eq y c= born y by Def5;
hence ( born y = born_eq y & born_eq y = born_eq x ) by A2, A3, XBOOLE_0:def 10; :: thesis:

end;

theorem :: SURREALO:36

for A being Ordinal holds
( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) )

proof

let A be Ordinal; :: thesis:
A1: ( {} << Day A & Day A << {} ) ;
for o being object st o in {} \/ (Day A) holds
ex O being Ordinal st
( O in succ A & o in Day O ) by ORDINAL1:6;
then A2: ( [{},(Day A)] in Day (succ A) & [(Day A),{}] in Day (succ A) ) by A1, SURREAL0:46;
then reconsider eD = [{},(Day A)], De = [(Day A),{}] as Surreal ;
A3: ( eD <= eD & De <= De ) ;
A4: ( eD in {eD} & De in {De} ) by TARSKI:def 1;
( L_ De << {De} & {eD} << R_ eD ) by Th11;
then ( not eD in Day A & not De in Day A ) by A3, A4;
hence ( [{},(Day A)] in (Day (succ A)) \ (Day A) & [(Day A),{}] in (Day (succ A)) \ (Day A) ) by A2, XBOOLE_0:def 5; :: thesis:

end;

definition

let A be set ;

func made_of A -> surreal-membered set means :Def8: :: SURREALO:def 8
for o being object holds
( o in it iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) );

existence

proof

defpred S₁[ object ] means $1 is surreal ;
consider X being set such that
A1: for x being object holds
( x in X iff ( x in [:(bool A),(bool A):] & S₁[x] ) ) from XBOOLE_0:sch 1();
X is surreal-membered by A1;
then reconsider X = X as surreal-membered set ;
take X ; :: thesis:
let o be object ; :: thesis:
thus ( o in X implies ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) :: thesis:

proof

assume A2: o in X ; :: thesis:
then ( o in [:(bool A),(bool A):] & S₁[o] ) by A1;
then consider a, b being object such that
A3: ( a in bool A & b in bool A & o = [a,b] ) by ZFMISC_1:def 2;
reconsider a = a, b = b as set by TARSKI:1;
thus ( o is surreal & (L_ o) \/ (R_ o) c= A ) by A1, A2, A3, XBOOLE_1:8; :: thesis:

end;

assume A4: ( o is surreal & (L_ o) \/ (R_ o) c= A ) ; :: thesis:
then reconsider O = o as Surreal ;
A5: O = [(L_ o),(R_ o)] ;
( L_ o c= (L_ o) \/ (R_ o) & R_ o c= (L_ o) \/ (R_ o) ) by XBOOLE_1:7;
then ( L_ o c= A & R_ o c= A ) by A4, XBOOLE_1:1;
then o in [:(bool A),(bool A):] by A5, ZFMISC_1:def 2;
hence o in X by A4, A1; :: thesis:

end;

uniqueness

proof

let C1, C2 be surreal-membered set ; :: thesis:
assume that
A6: for o being object holds
( o in C1 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) and
A7: for o being object holds
( o in C2 iff ( o is surreal & (L_ o) \/ (R_ o) c= A ) ) ; :: thesis:

now :: thesis:

let x be object ; :: thesis:
( x in C1 iff ( x is surreal & (L_ x) \/ (R_ x) c= A ) ) by A6;
hence ( x in C1 iff x in C2 ) by A7; :: thesis:

end;

hence C1 = C2 by TARSKI:2; :: thesis:

end;

:: deftheorem Def8 defines made_of SURREALO:def 8 :

definition

let A be Ordinal;

func unique_No_op A -> Sequence means :Def9: :: SURREALO:def 9
( dom it = succ A & ( for B being Ordinal st B in succ A holds
( it . B c= Day B & ( for x being Surreal holds
( x in it . B iff ( x in union (rng (it | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (it | B)))) & x = the b₃ -smallest Surreal ) ) ) ) ) ) ) );

existence

proof

defpred S₁[ Sequence, Surreal] means ( $2 in union (rng $1) or ( dom $1 = born_eq $2 & ex Y being non empty surreal-membered set st
( Y = (born_eq_set $2) /\ (made_of (union (rng $1))) & $2 = the b₁ -smallest Surreal ) ) );
deffunc H₁( Sequence) -> set = { e where e is Element of Day (dom $1) : for x being Surreal st x = e holds
S₁[$1,x] } ;
consider IT being Sequence such that
A1: dom IT = succ A and
A2: for B being Ordinal
for L1 being Sequence st B in succ A & L1 = IT | B holds
IT . B = H₁(L1) from ORDINAL1:sch 4();
take IT ; :: thesis:
thus dom IT = succ A by A1; :: thesis:
let B be Ordinal; :: thesis:
assume A3: B in succ A ; :: thesis:
set L1 = IT | B;
A4: dom (IT | B) = B by RELAT_1:62, A1, A3, ORDINAL1:def 2;
thus IT . B c= Day B :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in IT . B ; :: thesis:
then o in H₁(IT | B) by A3, A2;
then ex e being Element of Day (dom (IT | B)) st
( o = e & ( for x being Surreal st x = e holds
S₁[IT | B,x] ) ) ;
hence o in Day B by A4; :: thesis:

end;

let x be Surreal; :: thesis:
thus ( not x in IT . B or x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) :: thesis:

proof

assume A5: ( x in IT . B & not x in union (rng (IT | B)) ) ; :: thesis:
then x in H₁(IT | B) by A3, A2;
then consider e being Element of Day (dom (IT | B)) such that
A6: ( x = e & ( for y being Surreal st y = e holds
S₁[IT | B,y] ) ) ;
thus ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) by A4, A6, A5; :: thesis:

end;

assume ( x in union (rng (IT | B)) or ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ) ; :: thesis:

per cases ;

suppose A7: x in union (rng (IT | B)) ; :: thesis:

then consider Y being set such that
A8: ( x in Y & Y in rng (IT | B) ) by TARSKI:def 4;
consider C being object such that
A9: ( C in dom (IT | B) & (IT | B) . C = Y ) by A8, FUNCT_1:def 3;
reconsider C = C as Ordinal by A9;
defpred S₂[ Ordinal] means ( x in IT . $1 & $1 in B );
(IT | B) . C = IT . C by A9, FUNCT_1:47;
then A10: ex C being Ordinal st S₂[C] by A9, A8;
consider D being Ordinal such that
A11: ( S₂[D] & ( for E being Ordinal st S₂[E] holds
D c= E ) ) from ORDINAL1:sch 1(A10);
IT . D = H₁(IT | D) by A2, A11, A3, ORDINAL1:10;
then consider d being Element of Day (dom (IT | D)) such that
A12: ( x = d & ( for y being Surreal st y = d holds
S₁[IT | D,y] ) ) by A11;
D in succ A by A11, A3, ORDINAL1:10;
then A13: dom (IT | D) = D by RELAT_1:62, A1, ORDINAL1:def 2;
A14: x in Day D by A12, A13;
A15: Day D c= Day B by SURREAL0:35, A11, ORDINAL1:def 2;
for y being Surreal st y = x holds
S₁[IT | B,y] by A7;
then x in H₁(IT | B) by A15, A14, A4;
hence x in IT . B by A2, A3; :: thesis:

end;

suppose A16: ( B = born_eq x & ex Y being non empty surreal-membered set st
( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the b₁ -smallest Surreal ) ) ; :: thesis:

consider Y being non empty surreal-membered set such that
A17: ( Y = (born_eq_set x) /\ (made_of (union (rng (IT | B)))) & x = the Y -smallest Surreal ) by A16;
x in Y by A17, Def7;
then x in born_eq_set x by A17, XBOOLE_0:def 4;
then x in Day (born_eq x) by Def6;
then ( born_eq x c= born x & born x c= born_eq x ) by Def5, SURREAL0:def 18;
then A18: born_eq x = born x by XBOOLE_0:def 10;
A19: x in Day (dom (IT | B)) by A4, A16, A18, SURREAL0:def 18;
for y being Surreal st y = x holds
S₁[IT | B,y] by RELAT_1:62, A1, A3, ORDINAL1:def 2, A16;
then x in H₁(IT | B) by A19;
hence x in IT . B by A3, A2; :: thesis:

end;

uniqueness

proof

defpred S₁[ Sequence, Ordinal, Surreal] means ( $3 in union (rng $1) or ( $2 = born_eq $3 & ex Y being non empty surreal-membered set st
( Y = (born_eq_set $3) /\ (made_of (union (rng $1))) & $3 = the b₁ -smallest Surreal ) ) );
deffunc H₁( Sequence) -> set = { e where e is Element of Day (dom $1) : for x being Surreal st x = e holds
S₁[$1, dom $1,x] } ;
let S1, S2 be Sequence; :: thesis:
assume that
A20: dom S1 = succ A and
A21: for B being Ordinal st B in succ A holds
( S1 . B c= Day B & ( for x being Surreal holds
( x in S1 . B iff S₁[S1 | B,B,x] ) ) ) and
A22: dom S2 = succ A and
A23: for B being Ordinal st B in succ A holds
( S2 . B c= Day B & ( for x being Surreal holds
( x in S2 . B iff S₁[S2 | B,B,x] ) ) ) ; :: thesis:
A24: ( dom S1 = succ A & ( for B being Ordinal
for L1 being Sequence st B in succ A & L1 = S1 | B holds
S1 . B = H₁(L1) ) )

proof

thus dom S1 = succ A by A20; :: thesis:
let B be Ordinal; :: thesis:
let L1 be Sequence; :: thesis:
assume A25: ( B in succ A & L1 = S1 | B ) ; :: thesis:
A26: dom L1 = B by RELAT_1:62, A20, A25, ORDINAL1:def 2;
A27: S1 . B c= Day B by A21, A25;
thus S1 . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A28: o in S1 . B ; :: thesis:
then reconsider O = o as Surreal by A27;
for x being Surreal st x = o holds
S₁[S1 | B, dom (S1 | B),x] by A28, A21, A25, A26;
hence o in H₁(L1) by A25, A28, A27, A26; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in H₁(L1) ; :: thesis:
then consider e being Element of Day (dom L1) such that
A29: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[L1, dom L1,e] by A29;
hence o in S1 . B by A29, A21, A25, A26; :: thesis:

end;

A30: ( dom S2 = succ A & ( for B being Ordinal
for L2 being Sequence st B in succ A & L2 = S2 | B holds
S2 . B = H₁(L2) ) )

proof

thus dom S2 = succ A by A22; :: thesis:
let B be Ordinal; :: thesis:
let L1 be Sequence; :: thesis:
assume A31: ( B in succ A & L1 = S2 | B ) ; :: thesis:
A32: dom L1 = B by RELAT_1:62, A22, A31, ORDINAL1:def 2;
A33: S2 . B c= Day B by A23, A31;
thus S2 . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A34: o in S2 . B ; :: thesis:
then reconsider O = o as Surreal by A33;
for x being Surreal st x = o holds
S₁[S2 | B, dom (S2 | B),x] by A34, A23, A31, A32;
hence o in H₁(L1) by A31, A34, A33, A32; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in H₁(L1) ; :: thesis:
then consider e being Element of Day (dom L1) such that
A35: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[L1, dom L1,e] by A35;
hence o in S2 . B by A35, A23, A31, A32; :: thesis:

end;

S1 = S2 from ORDINAL1:sch 3(A24, A30);
hence S1 = S2 ; :: thesis:

end;

:: deftheorem Def9 defines unique_No_op SURREALO:def 9 :

registration

let A be Ordinal;
let o be object ;

cluster (unique_No_op A) . o -> surreal-membered ;

coherence

proof

let x be object ; :: according to SURREAL0:def 16 :: thesis:
assume A1: x in (unique_No_op A) . o ; :: thesis:
then A2: o in dom (unique_No_op A) by FUNCT_1:def 2;
then A3: o in succ A by Def9;
reconsider o = o as Ordinal by A2;
(unique_No_op A) . o c= Day o by A3, Def9;
hence x is surreal by A1; :: thesis:

end;

theorem Th37: :: SURREALO:37

for A, B being Ordinal st A c= B holds
(unique_No_op B) | (succ A) = unique_No_op A

proof

let A, B be Ordinal; :: thesis:
assume A c= B ; :: thesis:
then A1: A in succ B by ORDINAL1:22;
then A2: succ A c= succ B by ORDINAL1:21;
defpred S₁[ Sequence, Ordinal, Surreal] means ( $3 in union (rng $1) or ( $2 = born_eq $3 & ex Y being non empty surreal-membered set st
( Y = (born_eq_set $3) /\ (made_of (union (rng $1))) & $3 = the b₁ -smallest Surreal ) ) );
deffunc H₁( Sequence) -> set = { e where e is Element of Day (dom $1) : for x being Surreal st x = e holds
S₁[$1, dom $1,x] } ;
set S1 = unique_No_op A;
set S = unique_No_op B;
set S2 = (unique_No_op B) | (succ A);
A3: dom (unique_No_op A) = succ A by Def9;
A4: dom (unique_No_op B) = succ B by Def9;
then A5: dom ((unique_No_op B) | (succ A)) = succ A by A1, ORDINAL1:21, RELAT_1:62;
A6: ( dom (unique_No_op A) = succ A & ( for B being Ordinal
for L1 being Sequence st B in succ A & L1 = (unique_No_op A) | B holds
(unique_No_op A) . B = H₁(L1) ) )

proof

thus dom (unique_No_op A) = succ A by Def9; :: thesis:
let B be Ordinal; :: thesis:
let L1 be Sequence; :: thesis:
assume A7: ( B in succ A & L1 = (unique_No_op A) | B ) ; :: thesis:
A8: dom L1 = B by RELAT_1:62, A3, A7, ORDINAL1:def 2;
A9: (unique_No_op A) . B c= Day B by Def9, A7;
thus (unique_No_op A) . B c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A10: o in (unique_No_op A) . B ; :: thesis:
then reconsider O = o as Surreal by A9;
for x being Surreal st x = o holds
S₁[(unique_No_op A) | B, dom ((unique_No_op A) | B),x] by A10, Def9, A7, A8;
hence o in H₁(L1) by A10, A8, A9, A7; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in H₁(L1) ; :: thesis:
then consider e being Element of Day (dom L1) such that
A11: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[L1, dom L1,e] by A11;
hence o in (unique_No_op A) . B by A11, Def9, A7, A8; :: thesis:

end;

A12: ( dom ((unique_No_op B) | (succ A)) = succ A & ( for C being Ordinal
for L2 being Sequence st C in succ A & L2 = ((unique_No_op B) | (succ A)) | C holds
((unique_No_op B) | (succ A)) . C = H₁(L2) ) )

proof

thus dom ((unique_No_op B) | (succ A)) = succ A by A4, A1, ORDINAL1:21, RELAT_1:62; :: thesis:
let C be Ordinal; :: thesis:
let L1 be Sequence; :: thesis:
assume A13: ( C in succ A & L1 = ((unique_No_op B) | (succ A)) | C ) ; :: thesis:
A14: dom L1 = C by RELAT_1:62, A5, A13, ORDINAL1:def 2;
A15: dom ((unique_No_op B) | C) = C by A13, A2, A4, RELAT_1:62, ORDINAL1:def 2;
A16: (unique_No_op B) . C = ((unique_No_op B) | (succ A)) . C by A13, FUNCT_1:49;
A17: ( (unique_No_op B) . C c= Day C & ( for x being Surreal holds
( x in (unique_No_op B) . C iff S₁[(unique_No_op B) | C,C,x] ) ) ) by A13, A2, Def9;
A18: ( ((unique_No_op B) | (succ A)) | C = ((unique_No_op B) | (succ A)) | C & ((unique_No_op B) | (succ A)) | C = (unique_No_op B) | C ) by A13, ORDINAL1:def 2, RELAT_1:74;
thus ((unique_No_op B) | (succ A)) . C c= H₁(L1) :: according to XBOOLE_0:def 10 :: thesis:

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A19: o in ((unique_No_op B) | (succ A)) . C ; :: thesis:
then reconsider O = o as Surreal by A16, A17;
for x being Surreal st x = o holds
S₁[((unique_No_op B) | (succ A)) | C, dom (((unique_No_op B) | (succ A)) | C),x] by A18, A16, A19, A15, A13, A2, Def9;
hence o in H₁(L1) by A17, A19, A16, A13, A14; :: thesis:

end;

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume o in H₁(L1) ; :: thesis:
then consider e being Element of Day (dom L1) such that
A20: ( o = e & ( for x being Surreal st x = e holds
S₁[L1, dom L1,x] ) ) ;
S₁[(unique_No_op B) | C, dom ((unique_No_op B) | C),e] by A20, A13, A18;
hence o in ((unique_No_op B) | (succ A)) . C by A20, A16, A15, A13, A2, Def9; :: thesis:

end;

unique_No_op A = (unique_No_op B) | (succ A) from ORDINAL1:sch 3(A6, A12);
hence (unique_No_op B) | (succ A) = unique_No_op A ; :: thesis:

end;

theorem Th38: :: SURREALO:38

for A, B being Ordinal
for x being Surreal st x in (unique_No_op A) . B holds
( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) )

proof

let A, B be Ordinal; :: thesis:
let x be Surreal; :: thesis:
set M = unique_No_op A;
assume A1: x in (unique_No_op A) . B ; :: thesis:
then B in dom (unique_No_op A) by FUNCT_1:def 2;
then A2: B in succ A by Def9;
defpred S₁[ Ordinal] means ( x in (unique_No_op A) . $1 & $1 in succ A );
A3: ex C being Ordinal st S₁[C] by A1, A2;
consider D being Ordinal such that
A4: ( S₁[D] & ( for E being Ordinal st S₁[E] holds
D c= E ) ) from ORDINAL1:sch 1(A3);
A5: not x in union (rng ((unique_No_op A) | D))

proof

assume x in union (rng ((unique_No_op A) | D)) ; :: thesis:
then consider Z being set such that
A6: ( x in Z & Z in rng ((unique_No_op A) | D) ) by TARSKI:def 4;
consider E being object such that
A7: ( E in dom ((unique_No_op A) | D) & ((unique_No_op A) | D) . E = Z ) by A6, FUNCT_1:def 3;
reconsider E = E as Ordinal by A7;
S₁[E] by A4, A7, FUNCT_1:47, A6, ORDINAL1:10;
hence contradiction by A4, A7, ORDINAL1:5; :: thesis:

end;

then A8: D = born_eq x by A4, Def9;
consider Y being non empty surreal-membered set such that
A9: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op A) | D)))) & x = the Y -smallest Surreal ) by A5, A4, Def9;
x in (born_eq_set x) /\ (made_of (union (rng ((unique_No_op A) | D)))) by A9, Def7;
then x in born_eq_set x by XBOOLE_0:def 4;
then x in Day (born_eq x) by Def6;
then ( born x c= born_eq x & born_eq x c= born x ) by Def5, SURREAL0:def 18;
then born x = born_eq x by XBOOLE_0:def 10;
hence ( born_eq x = born x & born x c= B & x in (unique_No_op A) . (born x) & not x in union (rng ((unique_No_op A) | (born x))) ) by A1, A2, A4, A5, A8; :: thesis:

end;

theorem Th39: :: SURREALO:39

for A, B, O being Ordinal st O c= A & A c= B holds
(unique_No_op A) . O = (unique_No_op B) . O

proof

let A, B, O be Ordinal; :: thesis:
assume A1: ( O c= A & A c= B ) ; :: thesis:
O in succ A by A1, ORDINAL1:6, ORDINAL1:12;
then ((unique_No_op B) | (succ A)) . O = (unique_No_op B) . O by FUNCT_1:49;
hence (unique_No_op A) . O = (unique_No_op B) . O by A1, Th37; :: thesis:

end;

theorem :: SURREALO:40

for A, B, C being Ordinal st A c= B & B in succ C holds
(unique_No_op C) . A c= (unique_No_op C) . B

proof

let A, B, C be Ordinal; :: thesis:
assume A1: ( A c= B & B in succ C ) ; :: thesis:
set MC = unique_No_op C;
let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A2: o in (unique_No_op C) . A ; :: thesis:
then reconsider x = o as Surreal by SURREAL0:def 16;
set b = born x;
succ C = dom (unique_No_op C) by Def9;
then A3: dom ((unique_No_op C) | B) = B by RELAT_1:62, A1, ORDINAL1:def 2;

per cases ;

suppose A = B ; :: thesis:

hence o in (unique_No_op C) . B by A2; :: thesis:

end;

suppose A <> B ; :: thesis:

then A4: A in B by ORDINAL1:11, A1, XBOOLE_0:def 8;
then (unique_No_op C) . A = ((unique_No_op C) | B) . A by A3, FUNCT_1:47;
then (unique_No_op C) . A in rng ((unique_No_op C) | B) by A3, A4, FUNCT_1:def 3;
then o in union (rng ((unique_No_op C) | B)) by A2, TARSKI:def 4;
then x in (unique_No_op C) . B by A1, Def9;
hence o in (unique_No_op C) . B ; :: thesis:

end;

definition

let x be Surreal;

func Unique_No x -> Surreal means :Def10: :: SURREALO:def 10
( it == x & it in (unique_No_op (born_eq x)) . (born_eq x) );

existence

proof

defpred S₁[ 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
S₁[C] ) holds
S₁[D]

proof

let B be Ordinal; :: thesis:
assume A2: for C being Ordinal st C in B holds
S₁[C] ; :: thesis:
let z be Surreal; :: thesis:
assume A3: born_eq z = B ; :: thesis:
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 S₂[ 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 S₂[e,u]

proof

let e1 be object ; :: thesis:
assume A7: e1 in (L_ X) \/ (R_ X) ; :: thesis:
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:
thus ( e1 is Surreal & y is Surreal ) by A7, SURREAL0:def 16; :: thesis:
let a, b be Surreal; :: thesis:
assume A12: ( a = e1 & b = y ) ; :: thesis:
hence b == a by A10, A11, Th4; :: thesis:
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:

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
S₂[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:
assume A17: ( l in f .: (L_ X) & r in f .: (R_ X) ) ; :: thesis:
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:

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:
assume o in (f .: (L_ X)) \/ (f .: (R_ X)) ; :: thesis:
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:
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:

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:
assume A25: o in L_ X ; :: thesis:
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:
take fo ; :: thesis:
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:

end;

A27: R_ X <=_ f .: (R_ X)

proof

let o be Surreal; :: according to SURREALO:def 3 :: thesis:
assume A28: o in R_ X ; :: thesis:
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:
take fo ; :: thesis:
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:

end;

A30: f .: (L_ X) <=_ L_ X

proof

let o be Surreal; :: according to SURREALO:def 3 :: thesis:
assume o in f .: (L_ X) ; :: thesis:
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:
take a ; :: thesis:
a == o by A31, A14, A15;
hence ( a in L_ X & a in L_ X & a <= o & o <= a ) by A31; :: thesis:

end;

A32: f .: (R_ X) <=_ R_ X

proof

let o be Surreal; :: according to SURREALO:def 3 :: thesis:
assume o in f .: (R_ X) ; :: thesis:
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:
take a ; :: thesis:
a == o by A33, A14, A15;
hence ( a in R_ X & a in R_ X & a <= o & o <= a ) by A33; :: thesis:

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:
assume o in (L_ fX) \/ (R_ fX) ; :: thesis:
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:

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 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:

end;

for D being Ordinal holds S₁[D] from ORDINAL1:sch 2(A1);
hence ex b₁ being Surreal st
( b₁ == x & b₁ in (unique_No_op (born_eq x)) . (born_eq x) ) ; :: thesis:

end;

uniqueness

proof

set B = born_eq x;
set M = unique_No_op (born_eq x);
let s1, s2 be Surreal; :: thesis:
assume that
A43: ( s1 == x & s1 in (unique_No_op (born_eq x)) . (born_eq x) ) and
A44: ( s2 == x & s2 in (unique_No_op (born_eq x)) . (born_eq x) ) ; :: thesis:
( born s1 = born_eq s1 & born_eq s1 = born_eq x & born_eq x = born_eq s2 & born_eq s2 = born s2 ) by A43, A44, Th33, Th38;
then A45: ( not s1 in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) & not s2 in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) ) by A43, A44, Th38;
A46: born_eq x in succ (born_eq x) by ORDINAL1:6;
consider Y1 being non empty surreal-membered set such that
A47: ( Y1 = (born_eq_set s1) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & s1 = the Y1 -smallest Surreal ) by A43, A45, A46, Def9;
consider Y2 being non empty surreal-membered set such that
A48: ( Y2 = (born_eq_set s2) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & s2 = the Y2 -smallest Surreal ) by A44, A45, A46, Def9;
s1 == s2 by A43, A44, Th4;
then Y1 = Y2 by A47, A48, Th34;
hence s1 = s2 by A47, A48; :: thesis:

end;

:: deftheorem Def10 defines Unique_No SURREALO:def 10 :

theorem Th41: :: SURREALO:41

for x, y being Surreal st x == y holds
Unique_No x = Unique_No y

proof

let x, y be Surreal; :: thesis:
assume A1: x == y ; :: thesis:
then A2: born_eq x = born_eq y by Th33;
Unique_No y == y by Def10;
then ( Unique_No y == x & Unique_No y in (unique_No_op (born_eq x)) . (born_eq x) ) by A2, Def10, A1, Th4;
hence Unique_No x = Unique_No y by Def10; :: thesis:

end;

theorem Th42: :: SURREALO:42

0_No = Unique_No 0_No

proof

set B = born_eq 0_No;
set C = Unique_No 0_No;
Unique_No 0_No in (unique_No_op (born_eq 0_No)) . (born_eq 0_No) by Def10;
then A1: born (Unique_No 0_No) c= born_eq 0_No by Th38;
( born_eq 0_No c= born 0_No & born 0_No = {} ) by Def5, SURREAL0:37;
then born (Unique_No 0_No) = {} by A1;
hence 0_No = Unique_No 0_No by SURREAL0:37; :: thesis:

end;

definition

let x be Surreal;

attr x is uniq-surreal means :Def11: :: SURREALO:def 11
x = Unique_No x;

end;

:: deftheorem Def11 defines uniq-surreal SURREALO:def 11 :

registration

cluster 0_No -> uniq-surreal ;

coherence by Th42;

cluster non empty V9() surreal uniq-surreal for set ;

existence by Th42;

end;

definition

mode uSurreal is uniq-surreal Surreal;

end;

theorem Th43: :: SURREALO:43

for o being object
for x being Surreal st x is uSurreal & o in (L_ x) \/ (R_ x) holds
o is uSurreal

proof

let o be object ; :: thesis:
let x be Surreal; :: thesis:
set B = born_eq x;
assume A1: ( x is uSurreal & o in (L_ x) \/ (R_ x) ) ; :: thesis:
then x = Unique_No x by Def11;
then A2: x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
(L_ x) \/ (R_ x) is surreal-membered ;
then reconsider y = o as Surreal by A1;
A3: born_eq x in succ (born_eq x) by ORDINAL1:6;
A4: born_eq x = born x by A2, Th38;
then not x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A2, Th38;
then consider Y being non empty surreal-membered set such that
A5: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & x = the Y -smallest Surreal ) by A2, A3, Def9;
x in Y by A5, Def7;
then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by A5, XBOOLE_0:def 4;
then (L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by Def8;
then consider Z being set such that
A6: ( y in Z & Z in rng ((unique_No_op (born_eq x)) | (born_eq x)) ) by A1, TARSKI:def 4;
consider o being object such that
A7: ( o in dom ((unique_No_op (born_eq x)) | (born_eq x)) & ((unique_No_op (born_eq x)) | (born_eq x)) . o = Z ) by A6, FUNCT_1:def 3;
reconsider o = o as Ordinal by A7;
y in (unique_No_op (born_eq x)) . o by A6, A7, FUNCT_1:47;
then A8: ( born_eq y = born y & born y c= o & y in (unique_No_op (born_eq x)) . (born y) ) by Th38;
born y c= born_eq x by A4, A1, Th1, ORDINAL1:def 2;
then y in (unique_No_op (born y)) . (born y) by A8, Th39;
then Unique_No y = y by Def10, A8;
hence o is uSurreal by Def11; :: thesis:

end;

theorem :: SURREALO:44

for x being Surreal st not L_ x is empty & L_ x is finite & x is uSurreal holds
card (L_ x) = 1

proof

let x be Surreal; :: thesis:
assume A1: ( not L_ x is empty & L_ x is finite & x is uSurreal ) ; :: thesis:
then consider Min, Max being Surreal such that
A2: ( Min in L_ x & Max in L_ x ) and
A3: for y being Surreal st y in L_ x holds
( Min <= y & y <= Max ) by Th12;
reconsider c = card (L_ x) as Nat by A1;
assume A4: card (L_ x) <> 1 ; :: thesis:
set B = born_eq x;
x = Unique_No x by Def11, A1;
then A5: x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
A6: born_eq x in succ (born_eq x) by ORDINAL1:6;
A7: born_eq x = born x by A5, Th38;
then not x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A5, Th38;
then consider Y being non empty surreal-membered set such that
A8: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & x = the Y -smallest Surreal ) by A5, A6, Def9;
A9: for y being Surreal st y in L_ x holds
y <= Max by A3;
then reconsider Mx = [{Max},(R_ x)] as Surreal by A2, Th23;
A10: ( Mx == x & born Mx c= born x ) by A9, A2, Th23;
x in Y by A8, Def7;
then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by A8, XBOOLE_0:def 4;
then A11: (L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by Def8;
(L_ Mx) \/ (R_ Mx) c= (L_ x) \/ (R_ x) by XBOOLE_1:9, A2, ZFMISC_1:31;
then (L_ Mx) \/ (R_ Mx) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A11, XBOOLE_1:1;
then A12: Mx in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by Def8;
( Mx in Day (born Mx) & Day (born Mx) c= Day (born x) ) by A9, A2, Th23, SURREAL0:def 18, SURREAL0:35;
then Mx in born_eq_set x by A7, A10, Def6;
then Mx in Y by A8, A12, XBOOLE_0:def 4;
then A13: (card (L_ x)) (+) (card (R_ x)) c= (card (L_ Mx)) (+) (card (R_ Mx)) by A10, A8, Def7;
A14: card (L_ Mx) = 1 by CARD_1:30;
1 in Segm c by A4, A1, NAT_1:25, NAT_1:44;
then (card (L_ Mx)) (+) (card (R_ Mx)) in (card (L_ x)) (+) (card (R_ x)) by A14, ORDINAL7:94;
hence contradiction by A13, ORDINAL1:12; :: thesis:

end;

theorem :: SURREALO:45

for x being Surreal st not R_ x is empty & R_ x is finite & x is uSurreal holds
card (R_ x) = 1

proof

let x be Surreal; :: thesis:
assume A1: ( not R_ x is empty & R_ x is finite & x is uSurreal ) ; :: thesis:
then consider Min, Max being Surreal such that
A2: ( Min in R_ x & Max in R_ x ) and
A3: for y being Surreal st y in R_ x holds
( Min <= y & y <= Max ) by Th12;
reconsider c = card (R_ x) as Nat by A1;
assume A4: card (R_ x) <> 1 ; :: thesis:
set B = born_eq x;
x = Unique_No x by Def11, A1;
then A5: x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
A6: born_eq x in succ (born_eq x) by ORDINAL1:6;
A7: born_eq x = born x by A5, Th38;
then not x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A5, Th38;
then consider Y being non empty surreal-membered set such that
A8: ( Y = (born_eq_set x) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & x = the Y -smallest Surreal ) by A5, A6, Def9;
A9: for y being Surreal st y in R_ x holds
Min <= y by A3;
then reconsider Mx = [(L_ x),{Min}] as Surreal by A2, Th24;
A10: ( Mx == x & born Mx c= born x ) by A9, A2, Th24;
x in Y by A8, Def7;
then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by A8, XBOOLE_0:def 4;
then A11: (L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by Def8;
(L_ Mx) \/ (R_ Mx) c= (L_ x) \/ (R_ x) by XBOOLE_1:9, A2, ZFMISC_1:31;
then (L_ Mx) \/ (R_ Mx) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A11, XBOOLE_1:1;
then A12: Mx in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by Def8;
( Mx in Day (born Mx) & Day (born Mx) c= Day (born x) ) by A9, A2, Th24, SURREAL0:def 18, SURREAL0:35;
then Mx in born_eq_set x by A7, A10, Def6;
then Mx in Y by A8, A12, XBOOLE_0:def 4;
then A13: (card (L_ x)) (+) (card (R_ x)) c= (card (L_ Mx)) (+) (card (R_ Mx)) by A10, A8, Def7;
A14: card (R_ Mx) = 1 by CARD_1:30;
1 in Segm c by A4, A1, NAT_1:25, NAT_1:44;
then (card (L_ Mx)) (+) (card (R_ Mx)) in (card (L_ x)) (+) (card (R_ x)) by A14, ORDINAL7:94;
hence contradiction by A13, ORDINAL1:12; :: thesis:

end;

theorem :: SURREALO:46

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 0 iff x = 0_No )

proof

let x be Surreal; :: thesis:

hereby :: thesis:

assume (card (L_ x)) (+) (card (R_ x)) = 0 ; :: thesis:
then ( L_ x = {} & R_ x = {} ) ;
hence x = 0_No ; :: thesis:

end;

thus ( x = 0_No implies (card (L_ x)) (+) (card (R_ x)) = 0 ) ; :: thesis:

end;

theorem :: SURREALO:47

for x being Surreal holds
( (card (L_ x)) (+) (card (R_ x)) = 1 iff ex y being Surreal st
( x = [{},{y}] or x = [{y},{}] ) )

proof

let x be Surreal; :: thesis:
thus ( (card (L_ x)) (+) (card (R_ x)) = 1 implies ex y being Surreal st
( x = [{},{y}] or x = [{y},{}] ) ) :: thesis:

proof

assume A1: (card (L_ x)) (+) (card (R_ x)) = 1 ; :: thesis:
then ( card (L_ x) c= 1 & card (R_ x) c= 1 ) by ORDINAL7:86;
then reconsider c1 = card (L_ x), c2 = card (R_ x) as Nat ;
A2: c1 + c2 = 1 by A1, ORDINAL7:76;

per cases by NAT_1:11, NAT_1:25;

suppose A3: c1 = 0 ; :: thesis:

then consider y being object such that
A4: {y} = R_ x by A2, CARD_2:42;
y in {y} by TARSKI:def 1;
then reconsider y = y as Surreal by A4, SURREAL0:def 16;
take y ; :: thesis:
L_ x = {} by A3;
hence ( x = [{},{y}] or x = [{y},{}] ) by A4; :: thesis:

end;

suppose A5: c1 = 1 ; :: thesis:

then consider y being object such that
A6: {y} = L_ x by CARD_2:42;
y in {y} by TARSKI:def 1;
then reconsider y = y as Surreal by A6, SURREAL0:def 16;
take y ; :: thesis:
R_ x = {} by A5, A2;
hence ( x = [{},{y}] or x = [{y},{}] ) by A6; :: thesis:

end;

given y being Surreal such that A7: ( x = [{},{y}] or x = [{y},{}] ) ; :: thesis:
( ( card (L_ x) = 0 & card (R_ x) = 1 ) or ( card (R_ x) = 0 & card (L_ x) = 1 ) ) by A7, CARD_1:30;
then (card (L_ x)) (+) (card (R_ x)) = 1 + 0 by ORDINAL7:76;
hence (card (L_ x)) (+) (card (R_ x)) = 1 ; :: thesis:

end;

definition

let X be set ;

attr X is uniq-surreal-membered means :Def12: :: SURREALO:def 12
for o being object st o in X holds
o is uSurreal;

end;

:: deftheorem Def12 defines uniq-surreal-membered SURREALO:def 12 :

registration

cluster empty -> uniq-surreal-membered for set ;

coherence ;
let x be uSurreal;

cluster (L_ x) \/ (R_ x) -> uniq-surreal-membered ;

coherence by Th43;

cluster {x} -> uniq-surreal-membered ;

coherence by TARSKI:def 1;

end;

registration

let X, Y be uniq-surreal-membered set ;

cluster X \/ Y -> uniq-surreal-membered ;

coherence

proof

let o be object ; :: according to SURREALO:def 12 :: thesis:
assume o in X \/ Y ; :: thesis:
then ( o in X or o in Y ) by XBOOLE_0:def 3;
hence o is uSurreal by Def12; :: thesis:

end;

registration

let x be Surreal;

cluster Unique_No x -> uniq-surreal ;

coherence

proof

set c = Unique_No x;
born_eq (Unique_No x) = born_eq x by Def10, Th33;
then Unique_No x in (unique_No_op (born_eq (Unique_No x))) . (born_eq (Unique_No x)) by Def10;
hence Unique_No x is uniq-surreal by Def10; :: thesis:

end;

theorem Th48: :: SURREALO:48

for x being Surreal st x is uSurreal holds
born x = born_eq x

proof

let x be Surreal; :: thesis:
set B = born_eq x;
assume x is uSurreal ; :: thesis:
then x = Unique_No x by Def11;
then x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
hence born x = born_eq x by Th38; :: thesis:

end;

theorem :: SURREALO:49

for x being Surreal st ( for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) ) & x in born_eq_set x & (L_ x) \/ (R_ x) is uniq-surreal-membered holds
x is uSurreal

proof

let x be Surreal; :: thesis:
assume that
A1: for z being Surreal st z in born_eq_set x & (L_ z) \/ (R_ z) is uniq-surreal-membered & x <> z holds
(card (L_ x)) (+) (card (R_ x)) in (card (L_ z)) (+) (card (R_ z)) and
A2: ( x in born_eq_set x & (L_ x) \/ (R_ x) is uniq-surreal-membered ) ; :: thesis:
set c = Unique_No x;
set B = born_eq x;
A3: Unique_No x in (unique_No_op (born_eq x)) . (born_eq x) by Def10;
A4: born_eq x in succ (born_eq x) by ORDINAL1:6;
x in Day (born_eq x) by A2, Def6;
then ( born x c= born_eq x & born_eq x c= born x ) by SURREAL0:def 18, Def5;
then A5: born x = born_eq x by XBOOLE_0:def 10;
A6: x == Unique_No x by Def10;
A7: ( born_eq (Unique_No x) = born_eq x & born_eq_set (Unique_No x) = born_eq_set x ) by Def10, Th33, Th34;
born_eq (Unique_No x) = born (Unique_No x) by A3, Th38;
then not Unique_No x in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A3, Th38, A7;
then consider Y being non empty surreal-membered set such that
A8: ( Y = (born_eq_set (Unique_No x)) /\ (made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x))))) & Unique_No x = the Y -smallest Surreal ) by A3, A4, Def9;
Unique_No x in Y by A8, Def7;
then A9: ( Unique_No x in born_eq_set x & (L_ (Unique_No x)) \/ (R_ (Unique_No x)) is uniq-surreal-membered ) by A7, A8, XBOOLE_0:def 4;
A10: x in born_eq_set (Unique_No x) by A2, Def10, Th34;
(L_ x) \/ (R_ x) c= union (rng ((unique_No_op (born_eq x)) | (born_eq x)))

proof

let o be object ; :: according to TARSKI:def 3 :: thesis:
assume A11: o in (L_ x) \/ (R_ x) ; :: thesis:
then reconsider y = o as uSurreal by A2;
set C = born_eq y;
A12: born y = born_eq y by Th48;
y = Unique_No y by Def11;
then A13: y in (unique_No_op (born_eq y)) . (born_eq y) by Def10;
A14: born_eq y in born_eq x by A5, A12, A11, Th1;
born_eq y c= born_eq x by A5, A12, A11, Th1, ORDINAL1:def 2;
then A15: (unique_No_op (born_eq y)) . (born_eq y) = (unique_No_op (born_eq x)) . (born_eq y) by Th39;
A16: ((unique_No_op (born_eq x)) | (born_eq x)) . (born_eq y) = (unique_No_op (born_eq x)) . (born_eq y) by A5, A12, A11, Th1, FUNCT_1:49;
dom (unique_No_op (born_eq x)) = succ (born_eq x) by Def9;
then dom ((unique_No_op (born_eq x)) | (born_eq x)) = born_eq x by A4, RELAT_1:62, ORDINAL1:def 2;
then (unique_No_op (born_eq y)) . (born_eq y) in rng ((unique_No_op (born_eq x)) | (born_eq x)) by A15, A14, A16, FUNCT_1:def 3;
hence o in union (rng ((unique_No_op (born_eq x)) | (born_eq x))) by A13, TARSKI:def 4; :: thesis:

end;

then x in made_of (union (rng ((unique_No_op (born_eq x)) | (born_eq x)))) by Def8;
then x in Y by A8, A10, XBOOLE_0:def 4;
then (card (L_ (Unique_No x))) (+) (card (R_ (Unique_No x))) c= (card (L_ x)) (+) (card (R_ x)) by A8, A6, Def7;
hence x is uSurreal by A9, A1, ORDINAL1:5; :: thesis:

end;

theorem Th50: :: SURREALO:50

for x, y being Surreal st x is uSurreal & y is uSurreal & x == y holds
x = y

proof

let x, y be Surreal; :: thesis:
assume A1: ( x is uSurreal & y is uSurreal & x == y ) ; :: thesis:
thus x = Unique_No x by A1, Def11
.= Unique_No y by A1, Th41
.= y by A1, Def11 ; :: thesis:

end;

theorem Th51: :: SURREALO:51

for x, c being Surreal st born c = born_eq c & L_ c << {x} & {x} << R_ c holds
born c c= born x

proof

let x, c be Surreal; :: thesis:
assume that
A1: ( born c = born_eq c & L_ c << {x} & {x} << R_ c ) and
A2: not born c c= born x ; :: thesis:
defpred S₁[ Ordinal] means ex y being Surreal st
( L_ c << {y} & {y} << R_ c & born y = $1 );
S₁[ born x] by A1;
then A3: ex A being Ordinal st S₁[A] ;
consider A being Ordinal such that
A4: ( S₁[A] & ( for B being Ordinal st S₁[B] holds
A c= B ) ) from ORDINAL1:sch 1(A3);
consider y being Surreal such that
A5: ( L_ c << {y} & {y} << R_ c & born y = A ) by A4;
( A c= born x & born x in born c ) by A1, A2, ORDINAL1:16, A4;
then A6: born y in born c by A5, ORDINAL1:12;
for z being Surreal st L_ c << {z} & {z} << R_ c holds
born y c= born z by A4, A5;
then born_eq c = born_eq y by A5, Th16, Th33;
hence contradiction by A1, ORDINAL1:5, A6, Def5; :: thesis:

end;

theorem :: SURREALO:52

for c, x being uSurreal st L_ c << {x} & {x} << R_ c & x <> c holds
born c in born x

proof

let c, x be uSurreal; :: thesis:
assume that
A1: ( L_ c << {x} & {x} << R_ c & x <> c ) and
A2: not born c in born x ; :: thesis:
A3: born c = born_eq c by Th48;
then ( born c c= born x & born x c= born c ) by A1, A2, Th51, ORDINAL1:16;
then A4: born c = born x by XBOOLE_0:def 10;
not x == c by A1, Th50;

per cases ;

suppose x < c ; :: thesis:

per cases by Th13;

suppose ex xR being Surreal st
( xR in R_ x & x < xR & xR <= c ) ; :: thesis:

then consider xR being Surreal such that
A5: ( xR in R_ x & x < xR & xR <= c ) ;
xR in (L_ x) \/ (R_ x) by A5, XBOOLE_0:def 3;
then A6: born xR in born x by Th1;
( {c} << R_ c & x <= xR ) by A5, Th11;
then ( L_ c << {xR} & {xR} << R_ c ) by A1, A5, Th17, Th18;
then born c in born x by A3, Th51, A6, ORDINAL1:12;
hence contradiction by A4; :: thesis:

end;

suppose ex cL being Surreal st
( cL in L_ c & x <= cL & cL < c ) ; :: thesis:

then consider cL being Surreal such that
A7: ( cL in L_ c & x <= cL & cL < c ) ;
( L_ c << {cL} & cL in {cL} ) by A1, TARSKI:def 1, A7, Th17;
hence contradiction by A7, Th3; :: thesis:

end;

suppose c < x ; :: thesis:

per cases by Th13;

suppose ex cR being Surreal st
( cR in R_ c & c < cR & cR <= x ) ; :: thesis:

then consider cR being Surreal such that
A8: ( cR in R_ c & c < cR & cR <= x ) ;
( cR in {cR} & {cR} << R_ c ) by A1, A8, Th18, TARSKI:def 1;
hence contradiction by A8, Th3; :: thesis:

end;

suppose ex xL being Surreal st
( xL in L_ x & c <= xL & xL < x ) ; :: thesis:

then consider xL being Surreal such that
A9: ( xL in L_ x & c <= xL & xL < x ) ;
xL in (L_ x) \/ (R_ x) by A9, XBOOLE_0:def 3;
then A10: born xL in born x by Th1;
( L_ c << {c} & xL <= x ) by A9, Th11;
then ( L_ c << {xL} & {xL} << R_ c ) by A1, A9, Th17, Th18;
then born c in born x by A3, Th51, A10, ORDINAL1:12;
hence contradiction by A4; :: thesis:

end;

theorem :: SURREALO:53

for x being Surreal st born x = born_eq x & not born x is limit_ordinal holds
ex y, z being Surreal st
( x == z & ( z = [((L_ y) \/ {y}),(R_ y)] or z = [(L_ y),((R_ y) \/ {y})] ) )

proof

let x be Surreal; :: thesis:
assume A1: ( born x = born_eq x & not born x is limit_ordinal ) ; :: thesis:
then consider B being Ordinal such that
A2: born x = succ B by ORDINAL1:29;
defpred S₁[ object ] means for z being Surreal st z = $1 holds
( born z in B & z < x );
consider L being set such that
A3: for o being object holds
( o in L iff ( o in Day B & S₁[o] ) ) from XBOOLE_0:sch 1();
defpred S₂[ object ] means for z being Surreal st z = $1 holds
( born z in B & x < z );
consider R being set such that
A4: for o being object holds
( o in R iff ( o in Day B & S₂[o] ) ) from XBOOLE_0:sch 1();
A5: L << R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A6: ( l in L & r in R ) ; :: thesis:
( l < x & x <= r ) by A3, A4, A6;
hence not l >= r by Th4; :: thesis:

end;

A7: for o being object st o in L \/ R holds
ex O being Ordinal st
( O in B & o in Day O )

proof

let o be object ; :: thesis:
assume A8: o in L \/ R ; :: thesis:
A9: ( o in L or o in R ) by A8, XBOOLE_0:def 3;
then o in Day B by A3, A4;
then reconsider o = o as Surreal ;
( born o in B & o in Day (born o) ) by A9, A3, A4, SURREAL0:def 18;
hence ex O being Ordinal st
( O in B & o in Day O ) ; :: thesis:

end;

then A10: [L,R] in Day B by A5, SURREAL0:46;
then reconsider LR = [L,R] as Surreal ;
A11: not LR == x

proof

assume LR == x ; :: thesis:
then ( born x = born_eq LR & born_eq LR c= born LR & born LR c= B ) by A1, A10, SURREAL0:def 18, Th33, Def5;
then ( succ B c= B & B c= succ B ) by A2, XBOOLE_1:1, XBOOLE_1:7;
then succ B = B by XBOOLE_0:def 10;
then B in B by ORDINAL1:6;
hence contradiction ; :: thesis:

end;

per cases by A11;

suppose A12: LR < x ; :: thesis:

A13: L \/ {LR} << R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A14: ( l in L \/ {LR} & r in R ) ; :: thesis:
( l in L or l = LR ) by A14, ZFMISC_1:136;
then ( l < x & x <= r ) by A12, A3, A4, A14;
hence not l >= r by Th4; :: thesis:

end;

for o being object st o in (L \/ {LR}) \/ R holds
ex O being Ordinal st
( O in succ B & o in Day O )

proof

let o be object ; :: thesis:
assume A15: o in (L \/ {LR}) \/ R ; :: thesis:
( o in L \/ {LR} or o in R ) by A15, XBOOLE_0:def 3;
then A16: ( o in L or o = LR or o in R ) by ZFMISC_1:136;
then ( o = LR or o in Day B ) by A3, A4;
then reconsider o = o as Surreal ;
( born o in B or born o c= B ) by A10, A16, A3, A4, SURREAL0:def 18;
then born o c= B by ORDINAL1:def 2;
then ( born o in succ B & o in Day (born o) ) by ORDINAL1:22, SURREAL0:def 18;
hence ex O being Ordinal st
( O in succ B & o in Day O ) ; :: thesis:

end;

then A17: [(L \/ {LR}),R] in Day (succ B) by A13, SURREAL0:46;
then reconsider L1R = [(L \/ {LR}),R] as Surreal ;
take LR ; :: thesis:
take L1R ; :: thesis:
not born L1R c= B

proof

assume A18: born L1R c= B ; :: thesis:
LR in L \/ {LR} by ZFMISC_1:136;
then LR in (L_ L1R) \/ (R_ L1R) by XBOOLE_0:def 3;
then born LR in born L1R by Th1;
then S₁[LR] by A12, A18;
then ( LR in L & L = L_ LR & L_ LR << {LR} & LR in {LR} ) by A3, A7, A5, SURREAL0:46, Th11, TARSKI:def 1;
hence contradiction by Th3; :: thesis:

end;

then A19: ( succ B c= born L1R & born L1R c= succ B ) by A17, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18;
for y being Surreal st y == L1R holds
succ B c= born y

proof

let y be Surreal; :: thesis:
assume A20: y == L1R ; :: thesis:
assume A21: not succ B c= born y ; :: thesis:
then A22: born y c= B by ORDINAL1:16, ORDINAL1:22;
A23: ( L_ L1R << {y} & {y} << R_ L1R ) by A20, SURREAL0:43;
( LR in L \/ {LR} & y in {y} ) by TARSKI:def 1, ZFMISC_1:136;

per cases by Th13, A23;

suppose ex xLR being Surreal st
( xLR in R_ LR & LR < xLR & xLR <= y ) ; :: thesis:

then consider xLR being Surreal such that
A24: ( xLR in R_ LR & LR < xLR & xLR <= y ) ;
xLR <= L1R by A20, A24, Th4;
then ( L_ xLR << {L1R} & {xLR} << R_ L1R ) by SURREAL0:43;
then ( xLR in {xLR} & {xLR} << R ) by TARSKI:def 1;
hence contradiction by Th3, A24; :: thesis:

end;

suppose ex yL being Surreal st
( yL in L_ y & LR <= yL & yL < y ) ; :: thesis:

then consider yL being Surreal such that
A25: ( yL in L_ y & LR <= yL & yL < y ) ;
yL in (L_ y) \/ (R_ y) by A25, XBOOLE_0:def 3;
then A26: born yL in born y by Th1;
then A27: ( yL in Day (born yL) & Day (born yL) c= Day B ) by A21, ORDINAL1:22, SURREAL0:def 18, SURREAL0:35;

per cases ;

suppose x == yL ; :: thesis:

then ( B in succ B & succ B in B ) by A2, A26, A22, A1, ORDINAL1:6, ORDINAL1:12, Def5;
hence contradiction ; :: thesis:

end;

suppose yL < x ; :: thesis:

then S₁[yL] by A26, A22;
then ( yL in L & L = L_ LR & L_ LR << {LR} & LR in {LR} ) by A3, A27, TARSKI:def 1, Th11;
hence contradiction by A25; :: thesis:

end;

suppose x < yL ; :: thesis:

then S₂[yL] by A26, A22;
then ( yL in R & L1R in {L1R} & {L1R} << R_ L1R ) by A4, A27, TARSKI:def 1, Th11;
then ( L1R <= yL & yL < L1R ) by A25, A20, Th4;
hence contradiction ; :: thesis:

end;

then A28: born_eq L1R = succ B by A19, XBOOLE_0:def 10, Def5;
A29: L_ L1R << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A30: ( l in L_ L1R & r in {x} ) ; :: thesis:
( l in L or l = LR ) by A30, ZFMISC_1:136;
then l < x by A12, A3;
hence not l >= r by A30, TARSKI:def 1; :: thesis:

end;

A31: {L1R} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A32: ( l in {L1R} & r in R_ x ) ; :: thesis:
A33: r in (L_ x) \/ (R_ x) by A32, XBOOLE_0:def 3;
then A34: born r c= B by Th1, A2, ORDINAL1:22;
A35: ( x in {x} & {x} << R_ x ) by Th11, TARSKI:def 1;
A36: l = L1R by A32, TARSKI:def 1;
assume A37: r <= l ; :: thesis:
not l <= r

proof

assume l <= r ; :: thesis:
then L1R == r by A37, A32, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A33, Th1, Th33, Def5;
hence contradiction by A28, ORDINAL1:12; :: thesis:

end;

per cases by A36, Th13;

suppose ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) ; :: thesis:

then consider xR being Surreal such that
A38: ( xR in R_ r & r < xR & xR <= L1R ) ;
xR in (L_ r) \/ (R_ r) by A38, XBOOLE_0:def 3;
then A39: born xR in born r by Th1;
then A40: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A34, SURREAL0:35, SURREAL0:def 18, ORDINAL1:def 2;
r <= xR by A38;
then S₂[xR] by A35, A32, Th4, A39, A34;
then ( xR in R & L1R in {L1R} & {L1R} << R_ L1R ) by TARSKI:def 1, Th11, A40, A4;
hence contradiction by A38; :: thesis:

end;

suppose ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ; :: thesis:

then consider yL being Surreal such that
A41: ( yL in L_ L1R & r <= yL & yL < L1R ) ;

per cases by A41, ZFMISC_1:136;

suppose yL in L ; :: thesis:

then yL <= x by A3;
hence contradiction by A35, A32, Th4, A41; :: thesis:

end;

suppose yL = LR ; :: thesis:

then ( LR <= x & x < LR ) by A12, A35, A32, A41, Th4;
hence contradiction ; :: thesis:

end;

A42: L_ x << {L1R}

proof

let r be Surreal; :: according to SURREAL0:def 20 :: thesis:
let l be Surreal; :: thesis:
assume A43: ( r in L_ x & l in {L1R} ) ; :: thesis:
A44: r in (L_ x) \/ (R_ x) by A43, XBOOLE_0:def 3;
then A45: born r c= B by Th1, A2, ORDINAL1:22;
A46: ( x in {x} & L_ x << {x} ) by Th11, TARSKI:def 1;
A47: l = L1R by A43, TARSKI:def 1;
assume A48: l <= r ; :: thesis:
not r <= l

proof

assume r <= l ; :: thesis:
then L1R == r by A48, A43, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A44, Th1, Th33, Def5;
hence contradiction by A28, ORDINAL1:12; :: thesis:

end;

per cases by A47, Th13;

suppose ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) ; :: thesis:

then consider xR being Surreal such that
A49: ( xR in L_ r & L1R <= xR & xR < r ) ;
xR in (L_ r) \/ (R_ r) by A49, XBOOLE_0:def 3;
then A50: born xR in born r by Th1;
then A51: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A45, ORDINAL1:def 2, SURREAL0:def 18, SURREAL0:35;
xR <= r by A49;
then S₁[xR] by A50, A45, A46, A43, Th4;
then xR in L by A51, A3;
then ( xR in L_ L1R & L1R in {L1R} & L_ L1R << {L1R} ) by XBOOLE_0:def 3, TARSKI:def 1, Th11;
hence contradiction by A49; :: thesis:

end;

suppose ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ; :: thesis:

then consider yL being Surreal such that
A52: ( yL in R_ L1R & L1R < yL & yL <= r ) ;
x <= yL by A4, A52;
hence contradiction by A52, A46, A43, Th4; :: thesis:

end;

{x} << R_ L1R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A53: ( l in {x} & r in R_ L1R ) ; :: thesis:
x < r by A4, A53;
hence not l >= r by A53, TARSKI:def 1; :: thesis:

end;

hence ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) ) by A31, SURREAL0:43, A29, A42; :: thesis:

end;

suppose A54: x < LR ; :: thesis:

A55: L << R \/ {LR}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A56: ( l in L & r in R \/ {LR} ) ; :: thesis:
( r in R or r = LR ) by A56, ZFMISC_1:136;
then ( l <= x & x < r ) by A54, A3, A4, A56;
hence not l >= r by Th4; :: thesis:

end;

for o being object st o in L \/ (R \/ {LR}) holds
ex O being Ordinal st
( O in succ B & o in Day O )

proof

let o be object ; :: thesis:
assume A57: o in L \/ (R \/ {LR}) ; :: thesis:
( o in L or o in R \/ {LR} ) by A57, XBOOLE_0:def 3;
then A58: ( o in L or o = LR or o in R ) by ZFMISC_1:136;
then ( o = LR or o in Day B ) by A3, A4;
then reconsider o = o as Surreal ;
( born o in B or born o c= B ) by A10, A58, A3, A4, SURREAL0:def 18;
then born o c= B by ORDINAL1:def 2;
then ( born o in succ B & o in Day (born o) ) by ORDINAL1:22, SURREAL0:def 18;
hence ex O being Ordinal st
( O in succ B & o in Day O ) ; :: thesis:

end;

then A59: [L,(R \/ {LR})] in Day (succ B) by A55, SURREAL0:46;
then reconsider L1R = [L,(R \/ {LR})] as Surreal ;
take LR ; :: thesis:
take L1R ; :: thesis:
not born L1R c= B

proof

assume A60: born L1R c= B ; :: thesis:
LR in R \/ {LR} by ZFMISC_1:136;
then LR in (L_ L1R) \/ (R_ L1R) by XBOOLE_0:def 3;
then born LR in born L1R by Th1;
then S₂[LR] by A54, A60;
then ( LR in R & R = R_ LR & {LR} << R_ LR & LR in {LR} ) by A4, A7, A5, SURREAL0:46, Th11, TARSKI:def 1;
hence contradiction by Th3; :: thesis:

end;

then A61: ( succ B c= born L1R & born L1R c= succ B ) by A59, ORDINAL1:16, ORDINAL1:21, SURREAL0:def 18;
for y being Surreal st y == L1R holds
succ B c= born y

proof

let y be Surreal; :: thesis:
assume A62: y == L1R ; :: thesis:
assume A63: not succ B c= born y ; :: thesis:
then A64: born y c= B by ORDINAL1:16, ORDINAL1:22;
A65: ( L_ L1R << {y} & {y} << R_ L1R ) by A62, SURREAL0:43;
( LR in R \/ {LR} & y in {y} ) by TARSKI:def 1, ZFMISC_1:136;

per cases by A65, Th13;

suppose ex xLR being Surreal st
( xLR in L_ LR & y <= xLR & xLR < LR ) ; :: thesis:

then consider xLR being Surreal such that
A66: ( xLR in L_ LR & y <= xLR & xLR < LR ) ;
L1R <= xLR by A62, A66, Th4;
then ( L_ L1R << {xLR} & {L1R} << R_ xLR ) by SURREAL0:43;
then ( L << {xLR} & xLR in {xLR} ) by TARSKI:def 1;
hence contradiction by Th3, A66; :: thesis:

end;

suppose ex yL being Surreal st
( yL in R_ y & y < yL & yL <= LR ) ; :: thesis:

then consider yL being Surreal such that
A67: ( yL in R_ y & y < yL & yL <= LR ) ;
yL in (L_ y) \/ (R_ y) by A67, XBOOLE_0:def 3;
then A68: born yL in born y by Th1;
then A69: ( yL in Day (born yL) & Day (born yL) c= Day B ) by A63, ORDINAL1:22, SURREAL0:def 18, SURREAL0:35;

per cases ;

suppose x == yL ; :: thesis:

then ( B in succ B & succ B in B ) by A2, A68, A64, A1, Def5, ORDINAL1:6, ORDINAL1:12;
hence contradiction ; :: thesis:

end;

suppose x < yL ; :: thesis:

then S₂[yL] by A68, A64;
then ( yL in R & R = R_ LR & {LR} << R_ LR & LR in {LR} ) by A4, A69, TARSKI:def 1, Th11;
hence contradiction by A67; :: thesis:

end;

suppose yL < x ; :: thesis:

then S₁[yL] by A68, A64;
then ( yL in L & L1R in {L1R} & L_ L1R << {L1R} ) by A3, A69, TARSKI:def 1, Th11;
then ( L1R <= yL & yL < L1R ) by A67, A62, Th4;
hence contradiction ; :: thesis:

end;

then A70: born_eq L1R = succ B by A61, XBOOLE_0:def 10, Def5;
A71: L_ L1R << {x}

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A72: ( l in L_ L1R & r in {x} ) ; :: thesis:
l < x by A3, A72;
hence not l >= r by A72, TARSKI:def 1; :: thesis:

end;

A73: {L1R} << R_ x

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A74: ( l in {L1R} & r in R_ x ) ; :: thesis:
A75: r in (L_ x) \/ (R_ x) by A74, XBOOLE_0:def 3;
then A76: born r c= B by A2, Th1, ORDINAL1:22;
A77: ( x in {x} & {x} << R_ x ) by Th11, TARSKI:def 1;
A78: l = L1R by A74, TARSKI:def 1;
assume A79: r <= l ; :: thesis:
not l <= r

proof

assume l <= r ; :: thesis:
then L1R == r by A79, A74, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A75, Th1, Th33, Def5;
hence contradiction by A70, ORDINAL1:12; :: thesis:

end;

per cases by A78, Th13;

suppose ex xR being Surreal st
( xR in R_ r & r < xR & xR <= L1R ) ; :: thesis:

then consider xR being Surreal such that
A80: ( xR in R_ r & r < xR & xR <= L1R ) ;
xR in (L_ r) \/ (R_ r) by A80, XBOOLE_0:def 3;
then A81: born xR in born r by Th1;
then A82: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A76, SURREAL0:def 18, SURREAL0:35, ORDINAL1:def 2;
r <= xR by A80;
then S₂[xR] by A81, A76, A77, A74, Th4;
then xR in R by A82, A4;
then ( xR in R \/ {LR} & L1R in {L1R} & {L1R} << R_ L1R ) by TARSKI:def 1, Th11, XBOOLE_0:def 3;
hence contradiction by A80; :: thesis:

end;

suppose ex yL being Surreal st
( yL in L_ L1R & r <= yL & yL < L1R ) ; :: thesis:

then consider yL being Surreal such that
A83: ( yL in L_ L1R & r <= yL & yL < L1R ) ;
yL <= x by A3, A83;
hence contradiction by A83, A77, A74, Th4; :: thesis:

end;

A84: L_ x << {L1R}

proof

let r be Surreal; :: according to SURREAL0:def 20 :: thesis:
let l be Surreal; :: thesis:
assume A85: ( r in L_ x & l in {L1R} ) ; :: thesis:
A86: r in (L_ x) \/ (R_ x) by A85, XBOOLE_0:def 3;
then A87: born r c= B by A2, Th1, ORDINAL1:22;
A88: ( x in {x} & L_ x << {x} ) by Th11, TARSKI:def 1;
A89: l = L1R by A85, TARSKI:def 1;
assume A90: l <= r ; :: thesis:
not r <= l

proof

assume r <= l ; :: thesis:
then L1R == r by A90, A85, TARSKI:def 1;
then ( born_eq L1R = born_eq r & born_eq r c= born r & born r in succ B ) by A2, A86, Th1, Th33, Def5;
hence contradiction by A70, ORDINAL1:12; :: thesis:

end;

per cases by A89, Th13;

suppose ex xR being Surreal st
( xR in L_ r & L1R <= xR & xR < r ) ; :: thesis:

then consider xR being Surreal such that
A91: ( xR in L_ r & L1R <= xR & xR < r ) ;
xR in (L_ r) \/ (R_ r) by A91, XBOOLE_0:def 3;
then A92: born xR in born r by Th1;
then A93: ( xR in Day (born xR) & Day (born xR) c= Day B ) by A87, ORDINAL1:def 2, SURREAL0:def 18, SURREAL0:35;
xR <= r by A91;
then S₁[xR] by A92, A87, A88, A85, Th4;
then ( xR in L_ L1R & L1R in {L1R} & L_ L1R << {L1R} ) by A93, A3, TARSKI:def 1, Th11;
hence contradiction by A91; :: thesis:

end;

suppose ex yL being Surreal st
( yL in R_ L1R & L1R < yL & yL <= r ) ; :: thesis:

then consider yL being Surreal such that
A94: ( yL in R_ L1R & L1R < yL & yL <= r ) ;

per cases by A94, ZFMISC_1:136;

suppose yL in R ; :: thesis:

then x <= yL by A4;
hence contradiction by A94, A88, A85, Th4; :: thesis:

end;

suppose yL = LR ; :: thesis:

then ( LR <= x & x < LR ) by A54, A88, A85, A94, Th4;
hence contradiction ; :: thesis:

end;

{x} << R_ L1R

proof

let l be Surreal; :: according to SURREAL0:def 20 :: thesis:
let r be Surreal; :: thesis:
assume A95: ( l in {x} & r in R_ L1R ) ; :: thesis:
( r in R or r = LR ) by A95, ZFMISC_1:136;
then x < r by A54, A4;
hence not l >= r by A95, TARSKI:def 1; :: thesis:

end;

hence ( x == L1R & ( L1R = [((L_ LR) \/ {LR}),(R_ LR)] or L1R = [(L_ LR),((R_ LR) \/ {LR})] ) ) by A73, SURREAL0:43, A71, A84; :: thesis:

end;