let Lp, Lr be Sequence; :: thesis: ( 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 ) ) ) ) implies ( 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):] ) ) ) ) )
assume that
A1: dom Lp = dom Lr and
A2: 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 ) ) ) ; :: thesis: ( 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):] ) ) ) )
union (rng Lr) is Relation-like
proof
let y be object ; :: according to RELAT_1:def 1 :: thesis: ( not y in union (rng Lr) or ex b1, b2 being object st y = [b1,b2] )
assume A3: y in union (rng Lr) ; :: thesis: ex b1, b2 being object st y = [b1,b2]
consider Y being set such that
A4: ( y in Y & Y in rng Lr ) by A3, TARSKI:def 4;
consider A being object such that
A5: ( A in dom Lr & Lr . A = Y ) by A4, FUNCT_1:def 3;
reconsider A = A as Ordinal by A5;
ex a, b being Ordinal ex R being Relation st
( R = Lr . A & Lp . A = ClosedProd (R,a,b) ) by A5, A2, A1;
hence ex b1, b2 being object st y = [b1,b2] by A4, A5, RELAT_1:def 1; :: thesis: verum
end;
hence union (rng Lr) is Relation ; :: thesis: 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):] ) )
let R be Relation; :: thesis: ( R = union (rng Lr) implies ( 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):] ) ) )
assume A6: R = union (rng Lr) ; :: thesis: ( 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):] ) )
A7: R c= union (rng Lp)
proof
let y, z be object ; :: according to RELAT_1:def 3 :: thesis: ( not [y,z] in R or [y,z] in union (rng Lp) )
assume A8: [y,z] in R ; :: thesis: [y,z] in union (rng Lp)
consider Y being set such that
A9: ( [y,z] in Y & Y in rng Lr ) by A6, A8, TARSKI:def 4;
consider A being object such that
A10: ( A in dom Lr & Lr . A = Y ) by A9, FUNCT_1:def 3;
reconsider A = A as Ordinal by A10;
reconsider R = Lr . A as Relation by A10, A1, A2;
( R c= Lp . A & Lp . A in rng Lp ) by A10, A1, A2, FUNCT_1:def 3;
hence [y,z] in union (rng Lp) by A9, A10, TARSKI:def 4; :: thesis: verum
end;
R preserves_No_Comparison_on union (rng Lp)
proof
let x, y be object ; :: according to SURREAL0:def 11 :: thesis: ( [x,y] in union (rng Lp) implies ( x <= R,y iff ( L_ x << R,{y} & {x} << R, R_ y ) ) )
assume A11: [x,y] in union (rng Lp) ; :: thesis: ( x <= R,y iff ( L_ x << R,{y} & {x} << R, R_ y ) )
consider Y being set such that
A12: ( [x,y] in Y & Y in rng Lp ) by A11, TARSKI:def 4;
consider A being object such that
A13: ( A in dom Lp & Lp . A = Y ) by A12, FUNCT_1:def 3;
consider a, b being Ordinal, T being Relation such that
A14: ( T = Lr . A & Lp . A = ClosedProd (T,a,b) ) by A13, A2;
A15: ( T preserves_No_Comparison_on Lp . A & T c= Lp . A ) by A13, A14, A2;
thus ( x <= R,y implies ( L_ x << R,{y} & {x} << R, R_ y ) ) :: thesis: ( L_ x << R,{y} & {x} << R, R_ y implies x <= R,y )
proof
assume x <= R,y ; :: thesis: ( L_ x << R,{y} & {x} << R, R_ y )
then consider Y being set such that
A16: ( [x,y] in Y & Y in rng Lr ) by A6, TARSKI:def 4;
consider A being object such that
A17: ( A in dom Lr & Lr . A = Y ) by A16, FUNCT_1:def 3;
consider a, b being Ordinal, S being Relation such that
A18: ( S = Lr . A & Lp . A = ClosedProd (S,a,b) ) by A17, A2, A1;
A19: ( S preserves_No_Comparison_on ClosedProd (S,a,b) & S c= ClosedProd (S,a,b) ) by A17, A18, A1, A2;
then A20: S is almost-No-order by XBOOLE_1:1;
x <= S,y by A16, A17, A18;
then A21: ( L_ x << S,{y} & {x} << S, R_ y ) by A19;
A22: L_ x << R,{y}
proof
given l, r being object such that A23: ( l in L_ x & r in {y} & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A24: not l >= S,r by A21, A23;
consider Z being set such that
A25: ( [r,l] in Z & Z in rng Lr ) by A23, A6, TARSKI:def 4;
consider B being object such that
A26: ( B in dom Lr & Lr . B = Z ) by A25, FUNCT_1:def 3;
consider a1, b1 being Ordinal, W being Relation such that
A27: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A26, A2, A1;
A28: ( W preserves_No_Comparison_on ClosedProd (W,a1,b1) & W c= ClosedProd (W,a1,b1) ) by A26, A27, A1, A2;
then A29: W is almost-No-order by XBOOLE_1:1;
per cases ( a1 in a or ( a1 = a & b1 c= b ) or ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ) ;
suppose ( a1 in a or ( a1 = a & b1 c= b ) ) ; :: thesis: contradiction
then ClosedProd (S,a1,b1) c= ClosedProd (S,a,b) by Th17;
then S preserves_No_Comparison_on ClosedProd (S,a1,b1) by A19;
then A30: S /\ (ClosedProd (S,a1,b1)) = W /\ (ClosedProd (W,a1,b1)) by A28, A20, A29, Th23;
[r,l] in W /\ (ClosedProd (W,a1,b1)) by A25, A26, A27, A28, XBOOLE_0:def 4;
hence contradiction by A24, A30, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A31: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis: contradiction
then A32: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )
proof
assume A33: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis: contradiction
then a1 c= a by ORDINAL1:16;
hence contradiction by A33, A31, A32, XBOOLE_0:def 10; :: thesis: verum
end;
then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A28;
then A34: S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A19, A20, A29, Th23;
[x,y] in W /\ (ClosedProd (W,a,b)) by A34, A16, A17, A18, A19, XBOOLE_0:def 4;
then [x,y] in W by XBOOLE_0:def 4;
then ( x <= W,y & [x,y] in ClosedProd (W,a1,b1) ) by A28;
then L_ x << W,{y} by A28;
then not l >= W,r by A23;
hence contradiction by A25, A26, A27; :: thesis: verum
end;
end;
end;
{x} << R, R_ y
proof
given l, r being object such that A35: ( l in {x} & r in R_ y & l >= R,r ) ; :: according to SURREAL0:def 3 :: thesis: contradiction
A36: not l >= S,r by A21, A35;
consider Z being set such that
A37: ( [r,l] in Z & Z in rng Lr ) by A35, A6, TARSKI:def 4;
consider B being object such that
A38: ( B in dom Lr & Lr . B = Z ) by A37, FUNCT_1:def 3;
consider a1, b1 being Ordinal, W being Relation such that
A39: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A38, A2, A1;
A40: ( W preserves_No_Comparison_on ClosedProd (W,a1,b1) & W c= ClosedProd (W,a1,b1) ) by A38, A39, A1, A2;
then A41: W is almost-No-order by XBOOLE_1:1;
per cases ( a1 in a or ( a1 = a & b1 c= b ) or ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ) ;
suppose ( a1 in a or ( a1 = a & b1 c= b ) ) ; :: thesis: contradiction
then ClosedProd (S,a1,b1) c= ClosedProd (S,a,b) by Th17;
then S preserves_No_Comparison_on ClosedProd (S,a1,b1) by A19;
then A42: S /\ (ClosedProd (S,a1,b1)) = W /\ (ClosedProd (W,a1,b1)) by A40, A20, A41, Th23;
[r,l] in W /\ (ClosedProd (W,a1,b1)) by A37, A38, A39, A40, XBOOLE_0:def 4;
hence contradiction by A36, A42, XBOOLE_0:def 4; :: thesis: verum
end;
suppose A43: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis: contradiction
then A44: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )
proof
assume A45: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis: contradiction
then a1 c= a by ORDINAL1:16;
hence contradiction by A45, A43, A44, XBOOLE_0:def 10; :: thesis: verum
end;
then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A40;
then S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A19, A20, A41, Th23;
then [x,y] in W /\ (ClosedProd (W,a,b)) by A16, A17, A18, A19, XBOOLE_0:def 4;
then [x,y] in W by XBOOLE_0:def 4;
then ( x <= W,y & [x,y] in ClosedProd (W,a1,b1) ) by A40;
then {x} << W, R_ y by A40;
then not l >= W,r by A35;
hence contradiction by A37, A38, A39; :: thesis: verum
end;
end;
end;
hence ( L_ x << R,{y} & {x} << R, R_ y ) by A22; :: thesis: verum
end;
assume A46: ( L_ x << R,{y} & {x} << R, R_ y ) ; :: thesis: x <= R,y
assume A47: not x <= R,y ; :: thesis: contradiction
A48: not x <= T,y
proof
assume A49: x <= T,y ; :: thesis: contradiction
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
hence contradiction by A47, A49, A6, TARSKI:def 4; :: thesis: verum
end;
per cases ( not L_ x << T,{y} or not {x} << T, R_ y ) by A48, A15, A12, A13;
suppose not L_ x << T,{y} ; :: thesis: contradiction
then consider l, r being object such that
A50: ( l in L_ x & r in {y} & l >= T,r ) ;
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
then r <= R,l by A50, A6, TARSKI:def 4;
hence contradiction by A46, A50; :: thesis: verum
end;
suppose not {x} << T, R_ y ; :: thesis: contradiction
then consider l, r being object such that
A51: ( l in {x} & r in R_ y & l >= T,r ) ;
T in rng Lr by A13, A14, A1, FUNCT_1:def 3;
then r <= R,l by A51, A6, TARSKI:def 4;
hence contradiction by A46, A51; :: thesis: verum
end;
end;
end;
hence ( R preserves_No_Comparison_on union (rng Lp) & R c= union (rng Lp) ) by A7; :: thesis: 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):]
let A, a, b be Ordinal; :: thesis: 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):]
let S be Relation; :: thesis: ( A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) implies R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] )
assume A52: ( A in dom Lp & S = Lr . A & Lp . A = ClosedProd (S,a,b) ) ; :: thesis: R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):]
A53: R /\ [:(BeforeGames a),(BeforeGames a):] c= S /\ [:(BeforeGames a),(BeforeGames a):]
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] or [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] )
assume A54: [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] ; :: thesis: [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):]
A55: [x,y] in [:(BeforeGames a),(BeforeGames a):] by A54, XBOOLE_0:def 4;
[x,y] in R by A54, XBOOLE_0:def 4;
then consider Y being set such that
A56: ( [x,y] in Y & Y in rng Lr ) by A6, TARSKI:def 4;
consider B being object such that
A57: ( B in dom Lr & Lr . B = Y ) by A56, FUNCT_1:def 3;
reconsider B = B as Ordinal by A57;
consider a1, b1 being Ordinal, W being Relation such that
A58: ( W = Lr . B & Lp . B = ClosedProd (W,a1,b1) ) by A57, A1, A2;
reconsider W = Lr . B as Relation by A57, A1, A2;
A59: ( S preserves_No_Comparison_on Lp . A & S c= Lp . A ) by A52, A2;
then A60: S is almost-No-order by A52, XBOOLE_1:1;
A61: ( W preserves_No_Comparison_on Lp . B & W c= Lp . B ) by A57, A1, A2;
then A62: W is almost-No-order by A58, XBOOLE_1:1;
per cases ( ( not a1 in a & ( not a1 = a or not b1 c= b ) ) or a1 in a or ( a1 = a & b1 c= b ) ) ;
suppose A63: ( not a1 in a & ( not a1 = a or not b1 c= b ) ) ; :: thesis: [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):]
then A64: a c= a1 by ORDINAL1:16;
( a in a1 or ( a = a1 & b c= b1 ) )
proof
assume A65: ( not a in a1 & ( not a = a1 or not b c= b1 ) ) ; :: thesis: contradiction
then a1 c= a by ORDINAL1:16;
hence contradiction by A65, A63, A64, XBOOLE_0:def 10; :: thesis: verum
end;
then ClosedProd (W,a,b) c= ClosedProd (W,a1,b1) by Th17;
then W preserves_No_Comparison_on ClosedProd (W,a,b) by A61, A58;
then A66: S /\ (ClosedProd (S,a,b)) = W /\ (ClosedProd (W,a,b)) by A62, A60, A52, A59, Th23;
[x,y] in ClosedProd (W,a1,b1) by A56, A57, A61, A58;
then A67: ( x in Day (W,a1) & y in Day (W,a1) ) by ZFMISC_1:87;
A68: ( x in BeforeGames a & y in BeforeGames a ) by A55, ZFMISC_1:87;
then consider Ox being Ordinal such that
A69: ( Ox in a & x in Games Ox ) by Def5;
consider Oy being Ordinal such that
A70: ( Oy in a & y in Games Oy ) by A68, Def5;
A71: Day (W,Ox) c= Day (W,a) by Th9, A69, ORDINAL1:def 2;
A72: x in Day (W,Ox) by A67, A69, Th12;
then born (W,x) c= Ox by Def8;
then A73: ( born (W,x) in a & x in Day (W,a) ) by A69, A71, A72, ORDINAL1:12;
A74: Day (W,Oy) c= Day (W,a) by A70, ORDINAL1:def 2, Th9;
A75: y in Day (W,Oy) by A67, A70, Th12;
then born (W,y) c= Oy by Def8;
then ( born (W,y) in a & y in Day (W,a) ) by A70, A74, A75, ORDINAL1:12;
then [x,y] in ClosedProd (W,a,b) by A73, Def10;
then [x,y] in W /\ (ClosedProd (W,a,b)) by A56, A57, XBOOLE_0:def 4;
then [x,y] in S by A66, XBOOLE_0:def 4;
hence [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] by A55, XBOOLE_0:def 4; :: thesis: verum
end;
end;
end;
S /\ [:(BeforeGames a),(BeforeGames a):] c= R /\ [:(BeforeGames a),(BeforeGames a):]
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] or [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] )
assume A77: [x,y] in S /\ [:(BeforeGames a),(BeforeGames a):] ; :: thesis: [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):]
A78: [x,y] in [:(BeforeGames a),(BeforeGames a):] by A77, XBOOLE_0:def 4;
A79: [x,y] in S by A77, XBOOLE_0:def 4;
S in rng Lr by A52, A1, FUNCT_1:def 3;
then [x,y] in R by A79, A6, TARSKI:def 4;
hence [x,y] in R /\ [:(BeforeGames a),(BeforeGames a):] by A78, XBOOLE_0:def 4; :: thesis: verum
end;
hence R /\ [:(BeforeGames a),(BeforeGames a):] = S /\ [:(BeforeGames a),(BeforeGames a):] by A53, XBOOLE_0:def 10; :: thesis: verum