let S, T be surreal-membered desc_ordering set ; :: thesis: Unique_No (S ++ T) is desc_ordering
per cases ( S = {} or T = {} or ( S <> {} & T <> {} ) ) ;
suppose ( S = {} or T = {} ) ; :: thesis: Unique_No (S ++ T) is desc_ordering
hence Unique_No (S ++ T) is desc_ordering by Th39, SURREALR:27; :: thesis: verum
end;
suppose A1: ( S <> {} & T <> {} ) ; :: thesis: Unique_No (S ++ T) is desc_ordering
set US = Unique_No S;
set UT = Unique_No T;
Unique_No S <> {} by A1, Th39;
then reconsider U = ((Unique_No S) \/ (Unique_No T)) \/ (Unique_No ((Unique_No S) ++ (Unique_No T))) as non empty uniq-surreal-membered set ;
set R = RevSurrStr U;
set I = the InternalRel of (RevSurrStr U);
A2: field the InternalRel of (RevSurrStr U) = U by Th41;
A3: the carrier of (RevSurrStr U) = U by Def10;
A4: Unique_No ((Unique_No S) ++ (Unique_No T)) = Unique_No (S ++ T) by Th38;
( Unique_No S c= (Unique_No S) \/ (Unique_No T) & Unique_No T c= (Unique_No S) \/ (Unique_No T) & (Unique_No S) \/ (Unique_No T) c= U ) by XBOOLE_1:7;
then reconsider RA = Unique_No S, RB = Unique_No T, UR = Unique_No ((Unique_No S) ++ (Unique_No T)) as Subset of (RevSurrStr U) by A3, XBOOLE_1:1, XBOOLE_1:7;
set IU = the InternalRel of (RevSurrStr U) |_2 UR;
assume not Unique_No (S ++ T) is desc_ordering ; :: thesis: contradiction
then A5: not UR is well-ordering by A4, Th43;
not UR is well_founded
proof
A6: the InternalRel of (RevSurrStr U) is_connected_in UR
proof
let x, y be object ; :: according to RELAT_2:def 6 :: thesis: ( not x in UR or not y in UR or x = y or [x,y] in the InternalRel of (RevSurrStr U) or [y,x] in the InternalRel of (RevSurrStr U) )
assume A7: ( x in UR & y in UR & x <> y ) ; :: thesis: ( [x,y] in the InternalRel of (RevSurrStr U) or [y,x] in the InternalRel of (RevSurrStr U) )
reconsider a = x, b = y as Surreal by A7, SURREAL0:def 16;
( a <= b or b <= a ) ;
hence ( [x,y] in the InternalRel of (RevSurrStr U) or [y,x] in the InternalRel of (RevSurrStr U) ) by A3, A7, Def10; :: thesis: verum
end;
( the InternalRel of (RevSurrStr U) is_reflexive_in UR & the InternalRel of (RevSurrStr U) is_transitive_in UR & the InternalRel of (RevSurrStr U) is_antisymmetric_in UR & the InternalRel of (RevSurrStr U) is_connected_in UR ) by A3, A6, A2, RELAT_2:def 9, RELAT_2:def 12, RELAT_2:def 16, ORDERS_1:8, ORDERS_1:9, ORDERS_1:10;
hence not UR is well_founded by WELLFND1:def 3, A5, WELLORD1:def 5; :: thesis: verum
end;
then consider d being sequence of (RevSurrStr U) such that
A8: ( rng d c= UR & d is descending ) by Th12;
A9: dom d = NAT by FUNCT_2:def 1;
rng d is surreal-membered ;
then reconsider D = d as surreal-valued Function by SURREALC:def 9;
defpred S1[ object , object ] means ( $2 in Unique_No S & ( for sa being Surreal st $2 = sa holds
ex sb being Surreal st
( sb in Unique_No T & D . $1 = Unique_No (sa + sb) ) ) );
A10: for e being object st e in dom D holds
ex u being object st S1[e,u]
proof
let e be object ; :: thesis: ( e in dom D implies ex u being object st S1[e,u] )
assume A11: e in dom D ; :: thesis: ex u being object st S1[e,u]
A12: ( d . e in rng d & D .. e = D . e ) by Def5, A11, FUNCT_1:def 3;
then consider x being Surreal such that
A13: ( x in (Unique_No S) ++ (Unique_No T) & D .. e = Unique_No x ) by A8, Def8;
consider a, b being Surreal such that
A14: ( a in Unique_No S & b in Unique_No T & x = a + b ) by A13, SURREALR:def 8;
take a ; :: thesis: S1[e,a]
thus S1[e,a] by A12, A13, A14; :: thesis: verum
end;
consider a being Function such that
A15: ( dom a = dom D & ( for e being object st e in dom D holds
S1[e,a . e] ) ) from CLASSES1:sch 1(A10);
A16: rng a c= RA
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng a or y in RA )
assume y in rng a ; :: thesis: y in RA
then ex x being object st
( x in dom a & a . x = y ) by FUNCT_1:def 3;
hence y in RA by A15; :: thesis: verum
end;
then reconsider a = a as sequence of (RevSurrStr U) by XBOOLE_1:1, A9, A15, FUNCT_2:2;
reconsider Aa = a as surreal-valued Function by A16, SURREALC:def 9;
defpred S2[ object , object ] means ( $2 in Unique_No T & ( for sb being Surreal st $2 = sb holds
D . $1 = Unique_No ((Aa .. $1) + sb) ) );
A17: for e being object st e in dom D holds
ex u being object st S2[e,u]
proof
let e be object ; :: thesis: ( e in dom D implies ex u being object st S2[e,u] )
assume A18: e in dom D ; :: thesis: ex u being object st S2[e,u]
a . e = Aa .. e by A18, A15, Def5;
then consider sb being Surreal such that
A19: ( sb in Unique_No T & D . e = Unique_No ((Aa .. e) + sb) ) by A18, A15;
take sb ; :: thesis: S2[e,sb]
thus S2[e,sb] by A19; :: thesis: verum
end;
consider b being Function such that
A20: ( dom b = dom D & ( for e being object st e in dom D holds
S2[e,b . e] ) ) from CLASSES1:sch 1(A17);
A21: rng b c= RB
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng b or y in RB )
assume y in rng b ; :: thesis: y in RB
then ex x being object st
( x in dom b & b . x = y ) by FUNCT_1:def 3;
hence y in RB by A20; :: thesis: verum
end;
then reconsider b = b as sequence of (RevSurrStr U) by XBOOLE_1:1, A9, A20, FUNCT_2:2;
reconsider Bb = b as surreal-valued Function by A21, SURREALC:def 9;
RA is desc_ordering by Th46;
then RA is well-ordering by Th43;
then the InternalRel of (RevSurrStr U) is_well_founded_in RA by WELLORD1:def 5;
then consider sA being subsequence of a such that
A22: sA is non-descending by A16, Th19, WELLFND1:def 3;
consider NA being increasing sequence of NAT such that
A23: sA = a * NA by VALUED_0:def 17;
reconsider bN = b * NA as subsequence of b ;
rng bN c= rng b by RELAT_1:26;
then A24: rng bN c= RB by A21;
RB is desc_ordering by Th46;
then RB is well-ordering by Th43;
then the InternalRel of (RevSurrStr U) is_well_founded_in RB by WELLORD1:def 5;
then consider sB being subsequence of bN such that
A25: sB is non-descending by A24, Th19, WELLFND1:def 3;
consider NB being increasing sequence of NAT such that
A26: sB = bN * NB by VALUED_0:def 17;
reconsider sAN = sA * NB as subsequence of sA ;
reconsider dNA = d * NA as subsequence of d ;
reconsider dNANB = dNA * NB as subsequence of dNA ;
reconsider d1 = dNANB . (0 + 1), d0 = dNANB . 0 as uSurreal by A3, SURREALO:def 12;
dNA is descending by A8, Th13;
then A27: dNANB is descending by Th13;
then A28: ( d1 <> d0 & [d1,d0] in the InternalRel of (RevSurrStr U) ) by WELLFND1:def 6;
reconsider sA1 = sAN . (0 + 1), sA0 = sAN . 0 as uSurreal by A3, SURREALO:def 12;
sAN is non-descending by A22, Th20;
then [sA0,sA1] in the InternalRel of (RevSurrStr U) ;
then A29: sA1 <= sA0 by A3, Def10;
reconsider sB1 = sB . (0 + 1), sB0 = sB . 0 as uSurreal by A3, SURREALO:def 12;
[sB0,sB1] in the InternalRel of (RevSurrStr U) by A25;
then A30: sB1 <= sB0 by A3, Def10;
set N0 = NA . (NB . 0);
set N1 = NA . (NB . 1);
A31: sA0 = sA . (NB . 0) by FUNCT_2:15
.= a . (NA . (NB . 0)) by A23, FUNCT_2:15 ;
A32: sA1 = sA . (NB . 1) by FUNCT_2:15
.= a . (NA . (NB . 1)) by A23, FUNCT_2:15 ;
A33: sB0 = bN . (NB . 0) by A26, FUNCT_2:15
.= b . (NA . (NB . 0)) by FUNCT_2:15 ;
A34: sB1 = bN . (NB . 1) by A26, FUNCT_2:15
.= b . (NA . (NB . 1)) by FUNCT_2:15 ;
A35: d0 = dNA . (NB . 0) by FUNCT_2:15
.= d . (NA . (NB . 0)) by FUNCT_2:15 ;
A36: d1 = dNA . (NB . 1) by FUNCT_2:15
.= d . (NA . (NB . 1)) by FUNCT_2:15 ;
( sA1 = Aa .. (NA . (NB . 1)) & sA0 = Aa .. (NA . (NB . 0)) ) by A31, A32, A9, A15, Def5;
then ( d1 = Unique_No (sA1 + sB1) & d0 = Unique_No (sA0 + sB0) ) by A33, A34, A35, A36, A9, A20;
then A37: ( d1 == sA1 + sB1 & sA1 + sB1 <= sA0 + sB0 & d0 == sA0 + sB0 ) by A30, A29, SURREALO:def 10, SURREALR:43;
then d1 <= sA0 + sB0 by SURREALO:4;
then d1 == d0 by A3, Def10, A28, A37, SURREALO:4;
hence contradiction by A27, WELLFND1:def 6, SURREALO:50; :: thesis: verum
end;
end;