:: Conway Numbers -- Formal Introduction
:: by Karol P\kak
::
:: Received December 12, 2023
:: Copyright (c) 2023-2025 Association of Mizar Users

notation

let x be object ;
synonym L_ x for x `1 ;
synonym R_ x for x `2 ;

end;

definition

let x be object ;
:: original: L_
redefine func L_ x -> set ;
coherence
L_ x is set by TARSKI:1;

end;

definition

let x be object ;
:: original: R_
redefine func R_ x -> set ;
correctness
coherence
R_ x is set ;
by TARSKI:1;

end;

definition

let a, b be object ;
let O be set ;

pred a <= O,b means :: SURREAL0:def 1
[a,b] in O;

end;

:: deftheorem defines <= SURREAL0:def 1 :
for a, b being object
for O being set holds
( a <= O,b iff [a,b] in O );

notation

let a, b be object ;
let O be set ;
synonym b >= O,a for a <= O,b;

end;

definition

let L, R be set ;
let O be set ;

pred L >>= O,R means :: SURREAL0:def 2
for l, r being object st l in L & r in R holds
l >= O,r;

end;

:: deftheorem defines >>= SURREAL0:def 2 :
for L, R, O being set holds
( L >>= O,R iff for l, r being object st l in L & r in R holds
l >= O,r );

definition

let L, R be set ;
let O be set ;

pred L << O,R means :: SURREAL0:def 3
for l, r being object st l in L & r in R holds
not l >= O,r;

end;

:: deftheorem defines << SURREAL0:def 3 :
for L, R, O being set holds
( L << O,R iff for l, r being object st l in L & r in R holds
not l >= O,r );

definition

let A be Ordinal;

func Games A -> set means :Def4: :: SURREAL0:def 4
ex L being Sequence st
( it = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) );

correctness
existence
ex b₁ being set ex L being Sequence st
( b₁ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) );
uniqueness
for b₁, b₂ being set st ex L being Sequence st
( b₁ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) & ex L being Sequence st
( b₂ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) holds
b₁ = b₂;

proof end;

end;

:: deftheorem Def4 defines Games SURREAL0:def 4 :
for A being Ordinal
for b₂ being set holds
( b₂ = Games A iff ex L being Sequence st
( b₂ = L . A & dom L = succ A & ( for O being Ordinal st O in succ A holds
L . O = [:(bool (union (rng (L | O)))),(bool (union (rng (L | O)))):] ) ) );

registration

let A be Ordinal;

cluster Games A -> non empty Relation-like ;

coherence
( not Games A is empty & Games A is Relation-like )

proof end;

end;

theorem Th1: :: SURREAL0:1

for A, B being Ordinal st A c= B holds
Games A c= Games B

proof end;

theorem Th2: :: SURREAL0:2

Games 0 = {[{},{}]}

proof end;

theorem Th3: :: SURREAL0:3

for L being Sequence
for O being Ordinal st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = [:(bool (union (rng (L | A)))),(bool (union (rng (L | A)))):] ) holds
for A being Ordinal st A in succ O holds
L . A = Games A

proof end;

theorem Th4: :: SURREAL0:4

for O being Ordinal
for o being object holds
( o in Games O iff ( o is pair & ( for a being object st a in (L_ o) \/ (R_ o) holds
ex A being Ordinal st
( A in O & a in Games A ) ) ) )

proof end;

definition

let A be Ordinal;

func BeforeGames A -> Subset of (Games A) means :Def5: :: SURREAL0:def 5
for a being object holds
( a in it iff ex O being Ordinal st
( O in A & a in Games O ) );

existence
ex b₁ being Subset of (Games A) st
for a being object holds
( a in b₁ iff ex O being Ordinal st
( O in A & a in Games O ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Games A) st ( for a being object holds
( a in b₁ iff ex O being Ordinal st
( O in A & a in Games O ) ) ) & ( for a being object holds
( a in b₂ iff ex O being Ordinal st
( O in A & a in Games O ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def5 defines BeforeGames SURREAL0:def 5 :
for A being Ordinal
for b₂ being Subset of (Games A) holds
( b₂ = BeforeGames A iff for a being object holds
( a in b₂ iff ex O being Ordinal st
( O in A & a in Games O ) ) );

theorem Th5: :: SURREAL0:5

for A, B being Ordinal st A c= B holds
BeforeGames A c= BeforeGames B

proof end;

definition

let O be Ordinal;
let R be Relation;

func Day (R,O) -> Subset of (Games O) means :Def6: :: SURREAL0:def 6
ex L being Sequence st
( it = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) );

existence
ex b₁ being Subset of (Games O) ex L being Sequence st
( b₁ = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) )

proof end;

uniqueness
for b₁, b₂ being Subset of (Games O) st ex L being Sequence st
( b₁ = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) & ex L being Sequence st
( b₂ = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def6 defines Day SURREAL0:def 6 :
for O being Ordinal
for R being Relation
for b₃ being Subset of (Games O) holds
( b₃ = Day (R,O) iff ex L being Sequence st
( b₃ = L . O & dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) ) );

definition

let R be Relation;

attr R is almost-No-order means :: SURREAL0:def 7
ex O being Ordinal st R c= [:(Day (R,O)),(Day (R,O)):];

end;

:: deftheorem defines almost-No-order SURREAL0:def 7 :
for R being Relation holds
( R is almost-No-order iff ex O being Ordinal st R c= [:(Day (R,O)),(Day (R,O)):] );

theorem Th6: :: SURREAL0:6

for O being Ordinal
for R being Relation
for L being Sequence st dom L = succ O & ( for A being Ordinal st A in succ O holds
L . A = { x where x is Element of Games A : ( L_ x c= union (rng (L | A)) & R_ x c= union (rng (L | A)) & L_ x << R, R_ x ) } ) holds
for A being Ordinal st A in succ O holds
L . A = Day (R,A)

proof end;

theorem Th7: :: SURREAL0:7

for O being Ordinal
for R being Relation
for x being Element of Games O holds
( x in Day (R,O) iff ( L_ x << R, R_ x & ( for o being object st o in (L_ x) \/ (R_ x) holds
ex A being Ordinal st
( A in O & o in Day (R,A) ) ) ) )

proof end;

theorem Th8: :: SURREAL0:8

for R being Relation holds Day (R,0) = Games 0

proof end;

theorem Th9: :: SURREAL0:9

for A, B being Ordinal
for R being Relation st A c= B holds
Day (R,A) c= Day (R,B)

proof end;

registration

let R be Relation;
let A be Ordinal;

cluster Day (R,A) -> non empty ;

coherence
not Day (R,A) is empty

proof end;

end;

Lm1: for A being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,A) = Day (S,A)

proof end;

theorem Th10: :: SURREAL0:10

for A, B being Ordinal
for R, S being Relation st B c= A & R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
Day (R,B) = Day (S,B)

proof end;

definition

let R be Relation;
let o be object ;
assume A1: ex O being Ordinal st o in Day (R,O) ;

func born (R,o) -> Ordinal means :Def8: :: SURREAL0:def 8
( o in Day (R,it) & ( for O being Ordinal st o in Day (R,O) holds
it c= O ) );

existence
ex b₁ being Ordinal st
( o in Day (R,b₁) & ( for O being Ordinal st o in Day (R,O) holds
b₁ c= O ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal st o in Day (R,b₁) & ( for O being Ordinal st o in Day (R,O) holds
b₁ c= O ) & o in Day (R,b₂) & ( for O being Ordinal st o in Day (R,O) holds
b₂ c= O ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def8 defines born SURREAL0:def 8 :
for R being Relation
for o being object st ex O being Ordinal st o in Day (R,O) holds
for b₃ being Ordinal holds
( b₃ = born (R,o) iff ( o in Day (R,b₃) & ( for O being Ordinal st o in Day (R,O) holds
b₃ c= O ) ) );

theorem Th11: :: SURREAL0:11

for A being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
for a being object st a in Day (R,A) holds
born (R,a) = born (S,a)

proof end;

theorem Th12: :: SURREAL0:12

for A, O being Ordinal
for R being Relation
for o being object st o in Games O & not o in Day (R,O) holds
not o in Day (R,A)

proof end;

definition

let R be Relation;
let A, B be Ordinal;

func OpenProd (R,A,B) -> Relation of (Day (R,A)) means :Def9: :: SURREAL0:def 9
for x, y being Element of Day (R,A) holds
( [x,y] in it iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) );

existence
ex b₁ being Relation of (Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (Day (R,A)) st ( for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) ) & ( for x, y being Element of Day (R,A) holds
( [x,y] in b₂ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def9 defines OpenProd SURREAL0:def 9 :
for R being Relation
for A, B being Ordinal
for b₄ being Relation of (Day (R,A)) holds
( b₄ = OpenProd (R,A,B) iff for x, y being Element of Day (R,A) holds
( [x,y] in b₄ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) in B ) or ( born (R,x) in B & born (R,y) = A ) ) ) );

definition

let R be Relation;
let A, B be Ordinal;

func ClosedProd (R,A,B) -> Relation of (Day (R,A)) means :Def10: :: SURREAL0:def 10
for x, y being Element of Day (R,A) holds
( [x,y] in it iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) );

existence
ex b₁ being Relation of (Day (R,A)) st
for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) )

proof end;

uniqueness
for b₁, b₂ being Relation of (Day (R,A)) st ( for x, y being Element of Day (R,A) holds
( [x,y] in b₁ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) ) ) & ( for x, y being Element of Day (R,A) holds
( [x,y] in b₂ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def10 defines ClosedProd SURREAL0:def 10 :
for R being Relation
for A, B being Ordinal
for b₄ being Relation of (Day (R,A)) holds
( b₄ = ClosedProd (R,A,B) iff for x, y being Element of Day (R,A) holds
( [x,y] in b₄ iff ( ( born (R,x) in A & born (R,y) in A ) or ( born (R,x) = A & born (R,y) c= B ) or ( born (R,x) c= B & born (R,y) = A ) ) ) );

theorem :: SURREAL0:13

for A1, A2, B1, B2 being Ordinal
for R being Relation st ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) holds
OpenProd (R,A1,B1) c= OpenProd (R,A2,B2)

proof end;

theorem :: SURREAL0:14

for A, B being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
OpenProd (R,A,B) = OpenProd (S,A,B)

proof end;

theorem Th15: :: SURREAL0:15

for A, B being Ordinal
for R, S being Relation st R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):] holds
ClosedProd (R,A,B) = ClosedProd (S,A,B)

proof end;

theorem Th16: :: SURREAL0:16

for A, B being Ordinal
for R being Relation holds OpenProd (R,A,B) c= ClosedProd (R,A,B)

proof end;

theorem Th17: :: SURREAL0:17

for A1, A2, B1, B2 being Ordinal
for R being Relation st ( A1 in A2 or ( A1 = A2 & B1 c= B2 ) ) holds
ClosedProd (R,A1,B1) c= ClosedProd (R,A2,B2)

proof end;

theorem Th18: :: SURREAL0:18

for A, B, C being Ordinal
for R being Relation st B in C holds
ClosedProd (R,A,B) c= OpenProd (R,A,C)

proof end;

theorem Th19: :: SURREAL0:19

for A, B being Ordinal
for R being Relation st A in B holds
ClosedProd (R,A,B) c= OpenProd (R,A,B)

proof end;

definition

let X, R be set ;

pred R preserves_No_Comparison_on X means :: SURREAL0:def 11
for a, b being object st [a,b] in X holds
( a <= R,b iff ( L_ a << R,{b} & {a} << R, R_ b ) );

end;

:: deftheorem defines preserves_No_Comparison_on SURREAL0:def 11 :
for X, R being set holds
( R preserves_No_Comparison_on X iff for a, b being object st [a,b] in X holds
( a <= R,b iff ( L_ a << R,{b} & {a} << R, R_ b ) ) );

theorem Th20: :: SURREAL0:20

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) holds
R /\ [:(BeforeGames A),(BeforeGames A):] = S /\ [:(BeforeGames A),(BeforeGames A):]

proof end;

Lm2: for A, B being Ordinal st B c= A holds
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) c= S /\ (ClosedProd (S,A,B))

proof end;

theorem Th21: :: SURREAL0:21

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,B)) = S /\ (OpenProd (S,A,B)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

proof end;

theorem Th22: :: SURREAL0:22

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R /\ (OpenProd (R,A,0)) = S /\ (OpenProd (S,A,0)) & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

proof end;

theorem Th23: :: SURREAL0:23

for A, B being Ordinal
for R, S being Relation st R is almost-No-order & S is almost-No-order & R preserves_No_Comparison_on ClosedProd (R,A,B) & S preserves_No_Comparison_on ClosedProd (S,A,B) holds
R /\ (ClosedProd (R,A,B)) = S /\ (ClosedProd (S,A,B))

proof end;

theorem Th24: :: SURREAL0:24

for Lp, Lr being Sequence st dom Lp = dom Lr & ( for A being Ordinal st A in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) & Lr . A is Relation & ( for R being Relation st R = Lr . A holds
( R preserves_No_Comparison_on Lp . A & R c= Lp . A ) ) ) ) holds
( union (rng Lr) is Relation & ( for R being Relation st R = union (rng Lr) holds
( R preserves_No_Comparison_on union (rng Lp) & R c= union (rng Lp) & ( for A, a, b being Ordinal
for S being Relation st A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) holds
R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] ) ) ) )

proof end;

theorem Th25: :: SURREAL0:25

for A, B being Ordinal
for R being Relation
for a, b being object holds
( [a,b] in (ClosedProd (R,A,B)) \ (OpenProd (R,A,B)) iff ( a in Day (R,A) & b in Day (R,A) & ( ( born (R,a) = A & born (R,b) = B ) or ( born (R,a) = B & born (R,b) = A ) ) ) )

proof end;

theorem Th26: :: SURREAL0:26

for A, B being Ordinal
for R being Relation st R preserves_No_Comparison_on OpenProd (R,A,B) & R c= OpenProd (R,A,B) holds
ex S being Relation st
( R c= S & S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )

proof end;

theorem Th27: :: SURREAL0:27

for A, B being Ordinal st ex R being Relation st
( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) holds
ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )

proof end;

theorem Th28: :: SURREAL0:28

for A, B being Ordinal ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) )

proof end;

theorem Th29: :: SURREAL0:29

for A, B being Ordinal
for R being Relation st A in B holds
ClosedProd (R,A,A) = OpenProd (R,A,B)

proof end;

theorem Th30: :: SURREAL0:30

for A, B being Ordinal
for R being Relation st A c= B holds
ClosedProd (R,A,A) c= ClosedProd (R,B,B)

proof end;

Lm3: for A being Ordinal
for R being Relation holds ClosedProd (R,A,A) = [:(Day (R,A)),(Day (R,A)):]

proof end;

definition

let A be Ordinal;

func No_Ord A -> Relation means :Def12: :: SURREAL0:def 12
( it preserves_No_Comparison_on [:(Day (it,A)),(Day (it,A)):] & it c= [:(Day (it,A)),(Day (it,A)):] );

existence
ex b₁ being Relation st
( b₁ preserves_No_Comparison_on [:(Day (b₁,A)),(Day (b₁,A)):] & b₁ c= [:(Day (b₁,A)),(Day (b₁,A)):] )

proof end;

uniqueness
for b₁, b₂ being Relation st b₁ preserves_No_Comparison_on [:(Day (b₁,A)),(Day (b₁,A)):] & b₁ c= [:(Day (b₁,A)),(Day (b₁,A)):] & b₂ preserves_No_Comparison_on [:(Day (b₂,A)),(Day (b₂,A)):] & b₂ c= [:(Day (b₂,A)),(Day (b₂,A)):] holds
b₁ = b₂

proof end;

end;

:: deftheorem Def12 defines No_Ord SURREAL0:def 12 :
for A being Ordinal
for b₂ being Relation holds
( b₂ = No_Ord A iff ( b₂ preserves_No_Comparison_on [:(Day (b₂,A)),(Day (b₂,A)):] & b₂ c= [:(Day (b₂,A)),(Day (b₂,A)):] ) );

registration

let A be Ordinal;

cluster No_Ord A -> almost-No-order ;

coherence
No_Ord A is almost-No-order

proof end;

end;

definition

let A be Ordinal;

func Day A -> non empty Subset of (Games A) equals :: SURREAL0:def 13
Day ((No_Ord A),A);

coherence
Day ((No_Ord A),A) is non empty Subset of (Games A) ;

end;

:: deftheorem defines Day SURREAL0:def 13 :
for A being Ordinal holds Day A = Day ((No_Ord A),A);

definition

let o be object ;

attr o is surreal means :Def14: :: SURREAL0:def 14
ex A being Ordinal st o in Day A;

end;

:: deftheorem Def14 defines surreal SURREAL0:def 14 :
for o being object holds
( o is surreal iff ex A being Ordinal st o in Day A );

registration

cluster [{},{}] -> surreal ;

coherence
[{},{}] is surreal

proof end;

cluster surreal for set ;

existence
ex b₁ being set st b₁ is surreal

proof end;

end;

registration

let A be Ordinal;

cluster -> surreal for Element of Day A;

coherence
for b₁ being Element of Day A holds b₁ is surreal ;

end;

definition

mode Surreal is surreal set ;

end;

definition

func 0_No -> Surreal equals :: SURREAL0:def 15
[{},{}];

coherence
[{},{}] is Surreal by TARSKI:1;

end;

:: deftheorem defines 0_No SURREAL0:def 15 :
0_No = [{},{}];

registration

cluster surreal -> pair for set ;

coherence
for b₁ being Surreal holds b₁ is pair

proof end;

end;

registration

cluster surreal -> non empty for set ;

coherence
for b₁ being set st b₁ is surreal holds
not b₁ is empty ;

end;

definition

let X be set ;

attr X is surreal-membered means :Def16: :: SURREAL0:def 16
for o being object st o in X holds
o is surreal ;

end;

:: deftheorem Def16 defines surreal-membered SURREAL0:def 16 :
for X being set holds
( X is surreal-membered iff for o being object st o in X holds
o is surreal );

registration

cluster surreal-membered for set ;

existence
ex b₁ being set st b₁ is surreal-membered

proof end;

end;

registration

let x be Surreal;

cluster {x} -> surreal-membered ;

coherence
{x} is surreal-membered by TARSKI:def 1;

cluster L_ x -> surreal-membered for set ;

coherence
for b₁ being set st b₁ = L_ x holds
b₁ is surreal-membered

proof end;

cluster R_ x -> surreal-membered for set ;

coherence
for b₁ being set st b₁ = R_ x holds
b₁ is surreal-membered

proof end;

end;

registration

let X, Y be surreal-membered set ;

cluster X \/ Y -> surreal-membered ;

coherence
X \/ Y is surreal-membered

proof end;

cluster X \ Y -> surreal-membered ;

coherence
X \ Y is surreal-membered by Def16;

cluster X /\ Y -> surreal-membered ;

coherence
X /\ Y is surreal-membered

proof end;

end;

registration

cluster non empty surreal-membered for set ;

existence
ex b₁ being set st
( not b₁ is empty & b₁ is surreal-membered )

proof end;

end;

definition

let x, y be Surreal;

pred x <= y means :: SURREAL0:def 17
ex A being Ordinal st x <= No_Ord A,y;

end;

:: deftheorem defines <= SURREAL0:def 17 :
for x, y being Surreal holds
( x <= y iff ex A being Ordinal st x <= No_Ord A,y );

theorem Th31: :: SURREAL0:31

for A, B, X being Ordinal st X c= A & X c= B holds
(No_Ord A) /\ [:(BeforeGames X),(BeforeGames X):] = (No_Ord B) /\ [:(BeforeGames X),(BeforeGames X):]

proof end;

theorem Th32: :: SURREAL0:32

for A, B being Ordinal st A c= B holds
ClosedProd ((No_Ord A),A,A) = ClosedProd ((No_Ord B),A,A)

proof end;

theorem Th33: :: SURREAL0:33

for A being Ordinal
for a, b being object holds
( [a,b] in ClosedProd ((No_Ord A),A,A) iff ( a in Day A & b in Day A ) )

proof end;

theorem Th34: :: SURREAL0:34

for A, B being Ordinal st A c= B holds
No_Ord A = (No_Ord B) /\ (ClosedProd ((No_Ord B),A,A))

proof end;

theorem Th35: :: SURREAL0:35

for A, B being Ordinal st A c= B holds
Day A c= Day B

proof end;

theorem Th36: :: SURREAL0:36

for A, B being Ordinal
for o being object st o in Day ((No_Ord A),B) & B c= A holds
o in Day B

proof end;

definition

let x be Surreal;

func born x -> Ordinal means :Def18: :: SURREAL0:def 18
( x in Day it & ( for O being Ordinal st x in Day O holds
it c= O ) );

existence
ex b₁ being Ordinal st
( x in Day b₁ & ( for O being Ordinal st x in Day O holds
b₁ c= O ) )

proof end;

uniqueness
for b₁, b₂ being Ordinal st x in Day b₁ & ( for O being Ordinal st x in Day O holds
b₁ c= O ) & x in Day b₂ & ( for O being Ordinal st x in Day O holds
b₂ c= O ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def18 defines born SURREAL0:def 18 :
for x being Surreal
for b₂ being Ordinal holds
( b₂ = born x iff ( x in Day b₂ & ( for O being Ordinal st x in Day O holds
b₂ c= O ) ) );

theorem :: SURREAL0:37

for x being Surreal holds
( born x = {} iff x = 0_No )

proof end;

theorem :: SURREAL0:38

for A being Ordinal
for x being Surreal st x in Day A holds
born x = born ((No_Ord A),x)

proof end;

theorem Th39: :: SURREAL0:39

for A, B being Ordinal
for a, b being object st a <= No_Ord A,b & a in Day B & b in Day B holds
a <= No_Ord B,b

proof end;

theorem Th40: :: SURREAL0:40

for x, y being Surreal holds
( x <= y iff for A being Ordinal st x in Day A & y in Day A holds
x <= No_Ord A,y )

proof end;

definition

let L, R be set ;

pred L >>= R means :: SURREAL0:def 19
for l, r being Surreal st l in L & r in R holds
r <= l;

end;

:: deftheorem defines >>= SURREAL0:def 19 :
for L, R being set holds
( L >>= R iff for l, r being Surreal st l in L & r in R holds
r <= l );

notation

let R, L be set ;
synonym L <<= R for R >>= L;

end;

definition

let L, R be set ;

pred L << R means :: SURREAL0:def 20
for l, r being Surreal st l in L & r in R holds
not r <= l;

end;

:: deftheorem defines << SURREAL0:def 20 :
for L, R being set holds
( L << R iff for l, r being Surreal st l in L & r in R holds
not r <= l );

notation

let L, R be set ;
synonym R >> L for L << R;

end;

theorem :: SURREAL0:41

for X1, X2, Y being set st X1 << Y & X2 << Y holds
X1 \/ X2 << Y

proof end;

theorem :: SURREAL0:42

for X, Y1, Y2 being set st X << Y1 & X << Y2 holds
X << Y1 \/ Y2

proof end;

theorem Th43: :: SURREAL0:43

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

proof end;

theorem :: SURREAL0:44

for x, y being Surreal
for X1, X2, Y1, Y2 being set st ( for x being Surreal st x in X1 holds
ex y being Surreal st
( y in X2 & x <= y ) ) & ( for x being Surreal st x in Y2 holds
ex y being Surreal st
( y in Y1 & y <= x ) ) & x = [X1,Y1] & y = [X2,Y2] holds
x <= y

proof end;

theorem Th45: :: SURREAL0:45

for x being Surreal holds L_ x << R_ x

proof end;

theorem :: SURREAL0:46

for X, Y being set
for A being Ordinal holds
( [X,Y] in Day A iff ( X << Y & ( for o being object st o in X \/ Y holds
ex O being Ordinal st
( O in A & o in Day O ) ) ) )

proof end;

theorem :: SURREAL0:47

for X being set st X is surreal-membered holds
ex M being Ordinal st
for o being object st o in X holds
ex A being Ordinal st
( A in M & o in Day A )

proof end;