deffunc H1( Ordinal) -> Subset of [:(Day $1),(Day $1):] = Triangle $1;
deffunc H2( object , Function-yielding c=-monotone Sequence) -> object = [( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xL,yL]))) where xL is Element of L_ (L_ $1), yL is Element of L_ (R_ $1) : ( xL in L_ (L_ $1) & yL in L_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xR,yR]))) where xR is Element of R_ (L_ $1), yR is Element of R_ (R_ $1) : ( xR in R_ (L_ $1) & yR in R_ (R_ $1) ) } ),( { ((((union (rng $2)) . [xL,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yR])) +' (-' ((union (rng $2)) . [xL,yR]))) where xL is Element of L_ (L_ $1), yR is Element of R_ (R_ $1) : ( xL in L_ (L_ $1) & yR in R_ (R_ $1) ) } \/ { ((((union (rng $2)) . [xR,(R_ $1)]) +' ((union (rng $2)) . [(L_ $1),yL])) +' (-' ((union (rng $2)) . [xR,yL]))) where xR is Element of R_ (L_ $1), yL is Element of L_ (R_ $1) : ( xR in R_ (L_ $1) & yL in L_ (R_ $1) ) } )];
A1:
for A, B being Ordinal st A c= B holds
H1(A) c= H1(B)
by Th25;
A2:
for S being Function-yielding c=-monotone Sequence st ( for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ) holds
for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S)
proof
let S be
Function-yielding c=-monotone Sequence;
( ( for A being Ordinal st A in dom S holds
dom (S . A) = H1(A) ) implies for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S) )
assume A3:
for
A being
Ordinal st
A in dom S holds
dom (S . A) = H1(
A)
;
for A being Ordinal
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S)
let A be
Ordinal;
for x being object st x in dom (S . A) holds
H2(x,S | A) = H2(x,S)let a be
object ;
( a in dom (S . A) implies H2(a,S | A) = H2(a,S) )
assume A4:
a in dom (S . A)
;
H2(a,S | A) = H2(a,S)
S . A <> {}
by A4;
then A5:
A in dom S
by FUNCT_1:def 2;
then A6:
dom (S . A) = H1(
A)
by A3;
then consider x,
y being
object such that A7:
(
x in Day A &
y in Day A &
a = [x,y] )
by A4, ZFMISC_1:def 2;
reconsider x =
x,
y =
y as
Surreal by A7;
A8:
(born x) (+) (born y) c= A
by A7, A6, A4, Def5;
A9:
for
X,
Y being
surreal-membered set st
X c= (L_ x) \/ (R_ x) &
Y c= (L_ y) \/ (R_ y) holds
{ ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
proof
let X,
Y be
surreal-membered set ;
( X c= (L_ x) \/ (R_ x) & Y c= (L_ y) \/ (R_ y) implies { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } )
assume A10:
(
X c= (L_ x) \/ (R_ x) &
Y c= (L_ y) \/ (R_ y) )
;
{ ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } = { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
thus
{ ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } c= { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
XBOOLE_0:def 10 { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } c= { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } proof
let z be
object ;
TARSKI:def 3 ( not z in { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } or z in { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } )
assume
z in { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
;
z in { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
then consider xL being
Element of
X,
yL being
Element of
Y such that A11:
(
z = (((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL])) &
xL in X &
yL in Y )
;
reconsider xxL =
xL,
yyL =
yL as
Surreal by SURREAL0:def 16, A11;
set Lx =
(born xxL) (+) (born y);
A12:
(born xxL) (+) (born y) in (born x) (+) (born y)
by ORDINAL7:94, SURREALO:1, A10, A11;
then A13:
dom (S . ((born xxL) (+) (born y))) = H1(
(born xxL) (+) (born y))
by A8, A3, A5, ORDINAL1:10;
[xL,y] in H1(
(born xxL) (+) (born y))
by Def5;
then A14:
(union (rng (S | A))) . [xL,y] = (union (rng S)) . [xL,y]
by Th6, A13, A12, A8;
set Ly =
(born x) (+) (born yyL);
A15:
(born x) (+) (born yyL) in (born x) (+) (born y)
by A10, A11, ORDINAL7:94, SURREALO:1;
then A16:
dom (S . ((born x) (+) (born yyL))) = H1(
(born x) (+) (born yyL))
by A8, A3, A5, ORDINAL1:10;
[x,yL] in H1(
(born x) (+) (born yyL))
by Def5;
then A17:
(union (rng (S | A))) . [x,yL] = (union (rng S)) . [x,yL]
by Th6, A16, A15, A8;
set Lxy =
(born xxL) (+) (born yyL);
A18:
(born xxL) (+) (born yyL) in (born x) (+) (born yyL)
by A10, A11, ORDINAL7:94, SURREALO:1;
then
(born xxL) (+) (born yyL) in (born x) (+) (born y)
by A15, ORDINAL1:10;
then A19:
dom (S . ((born xxL) (+) (born yyL))) = H1(
(born xxL) (+) (born yyL))
by A8, A3, A5, ORDINAL1:10;
[xL,yL] in H1(
(born xxL) (+) (born yyL))
by Def5;
then
(union (rng (S | A))) . [xL,yL] = (union (rng S)) . [xL,yL]
by Th6, A19, A18, A8, A15, ORDINAL1:10;
hence
z in { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
by A14, A17, A11;
verum
end;
let z be
object ;
TARSKI:def 3 ( not z in { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } or z in { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) } )
assume
z in { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
;
z in { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
then consider xL being
Element of
X,
yL being
Element of
Y such that A20:
(
z = (((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL])) &
xL in X &
yL in Y )
;
reconsider xxL =
xL,
yyL =
yL as
Surreal by SURREAL0:def 16, A20;
set Lx =
(born xxL) (+) (born y);
A21:
(born xxL) (+) (born y) in (born x) (+) (born y)
by A10, A20, ORDINAL7:94, SURREALO:1;
then A22:
dom (S . ((born xxL) (+) (born y))) = H1(
(born xxL) (+) (born y))
by A8, A3, A5, ORDINAL1:10;
[xL,y] in H1(
(born xxL) (+) (born y))
by Def5;
then A23:
(union (rng (S | A))) . [xL,y] = (union (rng S)) . [xL,y]
by Th6, A22, A21, A8;
set Ly =
(born x) (+) (born yyL);
A24:
(born x) (+) (born yyL) in (born x) (+) (born y)
by A10, A20, ORDINAL7:94, SURREALO:1;
then A25:
dom (S . ((born x) (+) (born yyL))) = H1(
(born x) (+) (born yyL))
by A8, A3, A5, ORDINAL1:10;
[x,yL] in H1(
(born x) (+) (born yyL))
by Def5;
then A26:
(union (rng (S | A))) . [x,yL] = (union (rng S)) . [x,yL]
by Th6, A25, A24, A8;
set Lxy =
(born xxL) (+) (born yyL);
A27:
(born xxL) (+) (born yyL) in (born x) (+) (born yyL)
by A10, A20, ORDINAL7:94, SURREALO:1;
then
(born xxL) (+) (born yyL) in (born x) (+) (born y)
by A24, ORDINAL1:10;
then A28:
dom (S . ((born xxL) (+) (born yyL))) = H1(
(born xxL) (+) (born yyL))
by A8, A3, A5, ORDINAL1:10;
[xL,yL] in H1(
(born xxL) (+) (born yyL))
by Def5;
then
(union (rng (S | A))) . [xL,yL] = (union (rng S)) . [xL,yL]
by Th6, A28, A27, A8, A24, ORDINAL1:10;
hence
z in { ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of X, yL is Element of Y : ( xL in X & yL in Y ) }
by A23, A26, A20;
verum
end;
A29:
(
L_ x c= (L_ x) \/ (R_ x) &
R_ x c= (L_ x) \/ (R_ x) &
L_ y c= (L_ y) \/ (R_ y) &
R_ y c= (L_ y) \/ (R_ y) )
by XBOOLE_1:7;
then A30:
{ ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yL])) +' (-' ((union (rng (S | A))) . [xL,yL]))) where xL is Element of L_ x, yL is Element of L_ y : ( xL in L_ x & yL in L_ y ) } = { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yL])) +' (-' ((union (rng S)) . [xL,yL]))) where xL is Element of L_ x, yL is Element of L_ y : ( xL in L_ x & yL in L_ y ) }
by A9;
A31:
{ ((((union (rng (S | A))) . [xR,y]) +' ((union (rng (S | A))) . [x,yR])) +' (-' ((union (rng (S | A))) . [xR,yR]))) where xR is Element of R_ x, yR is Element of R_ y : ( xR in R_ x & yR in R_ y ) } = { ((((union (rng S)) . [xR,y]) +' ((union (rng S)) . [x,yR])) +' (-' ((union (rng S)) . [xR,yR]))) where xR is Element of R_ x, yR is Element of R_ y : ( xR in R_ x & yR in R_ y ) }
by A29, A9;
{ ((((union (rng (S | A))) . [xL,y]) +' ((union (rng (S | A))) . [x,yR])) +' (-' ((union (rng (S | A))) . [xL,yR]))) where xL is Element of L_ x, yR is Element of R_ y : ( xL in L_ x & yR in R_ y ) } = { ((((union (rng S)) . [xL,y]) +' ((union (rng S)) . [x,yR])) +' (-' ((union (rng S)) . [xL,yR]))) where xL is Element of L_ x, yR is Element of R_ y : ( xL in L_ x & yR in R_ y ) }
by A29, A9;
hence
H2(
a,
S | A)
= H2(
a,
S)
by A7, A30, A31, A29, A9;
verum
end;
consider S being Function-yielding c=-monotone Sequence such that
A32:
dom S = succ A
and
A33:
for A1 being Ordinal st A1 in succ A holds
ex SA1 being ManySortedSet of H1(A1) st
( S . A1 = SA1 & ( for x being object st x in H1(A1) holds
SA1 . x = H2(x,S | A1) ) )
from SURREALR:sch 1(A2, A1);
consider SA being ManySortedSet of H1(A) such that
A34:
S . A = SA
and
for x being object st x in H1(A) holds
SA . x = H2(x,S | A)
by A33, ORDINAL1:6;
take
SA
; ex S being Function-yielding c=-monotone Sequence st
( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) )
take
S
; ( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) )
thus
( dom S = succ A & SA = S . A & ( for B being Ordinal st B in succ A holds
ex SB being ManySortedSet of Triangle B st
( S . B = SB & ( for x being object st x in Triangle B holds
SB . x = [( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xL,yL]))) where xL is Element of L_ (L_ x), yL is Element of L_ (R_ x) : ( xL in L_ (L_ x) & yL in L_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xR,yR]))) where xR is Element of R_ (L_ x), yR is Element of R_ (R_ x) : ( xR in R_ (L_ x) & yR in R_ (R_ x) ) } ),( { ((((union (rng (S | B))) . [xL,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yR])) +' (-' ((union (rng (S | B))) . [xL,yR]))) where xL is Element of L_ (L_ x), yR is Element of R_ (R_ x) : ( xL in L_ (L_ x) & yR in R_ (R_ x) ) } \/ { ((((union (rng (S | B))) . [xR,(R_ x)]) +' ((union (rng (S | B))) . [(L_ x),yL])) +' (-' ((union (rng (S | B))) . [xR,yL]))) where xR is Element of R_ (L_ x), yL is Element of L_ (R_ x) : ( xR in R_ (L_ x) & yL in L_ (R_ x) ) } )] ) ) ) )
by A32, A34, A33; verum