let A, B be Ordinal; :: thesis: ( ex R being Relation st
( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) implies ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) ) )
assume A1: ex R being Relation st
( R preserves_No_Comparison_on OpenProd (R,A,{}) & R c= OpenProd (R,A,{}) ) ; :: thesis: ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) )
defpred S1[ Ordinal] means ex R being Relation st
( R preserves_No_Comparison_on ClosedProd (R,A,$1) & R c= ClosedProd (R,A,$1) );
A2: for D being Ordinal st ( for C being Ordinal st C in D holds
S1[C] ) holds
S1[D]
proof
let D be Ordinal; :: thesis: ( ( for C being Ordinal st C in D holds
S1[C] ) implies S1[D] )
assume A3: for C being Ordinal st C in D holds
S1[C] ; :: thesis: S1[D]
per cases ( D = {} or D <> {} ) ;
suppose A6: D <> {} ; :: thesis: S1[D]
defpred S2[ object , object ] means for B being Ordinal st B = $1 holds
ex R being Relation st
( $2 = R & R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) );
A7: for e being object st e in D holds
ex u being object st S2[e,u]
proof
let e be object ; :: thesis: ( e in D implies ex u being object st S2[e,u] )
assume A8: e in D ; :: thesis: ex u being object st S2[e,u]
reconsider E = e as Ordinal by A8;
consider R being Relation such that
A9: ( R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A3, A8;
take R ; :: thesis: S2[e,R]
thus S2[e,R] by A9; :: thesis: verum
end;
consider Lr being Function such that
A10: ( dom Lr = D & ( for e being object st e in D holds
S2[e,Lr . e] ) ) from CLASSES1:sch 1(A7);
reconsider Lr = Lr as Sequence by A10, ORDINAL1:def 7;
defpred S3[ object , object ] means for B being Ordinal
for R being Relation st B = $1 & R = Lr . B holds
$2 = ClosedProd (R,A,B);
A11: for e being object st e in D holds
ex u being object st S3[e,u]
proof
let e be object ; :: thesis: ( e in D implies ex u being object st S3[e,u] )
assume A12: e in D ; :: thesis: ex u being object st S3[e,u]
reconsider E = e as Ordinal by A12;
consider R being Relation such that
A13: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A12, A10;
take ClosedProd (R,A,E) ; :: thesis: S3[e, ClosedProd (R,A,E)]
thus S3[e, ClosedProd (R,A,E)] by A13; :: thesis: verum
end;
consider Lp being Function such that
A14: ( dom Lp = D & ( for e being object st e in D holds
S3[e,Lp . e] ) ) from CLASSES1:sch 1(A11);
reconsider Lp = Lp as Sequence by A14, ORDINAL1:def 7;
A15: for E being Ordinal st E in dom Lp holds
( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )
proof
let E be Ordinal; :: thesis: ( E in dom Lp implies ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) )
assume A16: E in dom Lp ; :: thesis: ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) )
consider R being Relation such that
A17: ( Lr . E = R & R preserves_No_Comparison_on ClosedProd (R,A,E) & R c= ClosedProd (R,A,E) ) by A16, A10, A14;
thus ( ex a, b being Ordinal ex R being Relation st
( R = Lr . E & Lp . E = ClosedProd (R,a,b) ) & Lr . E is Relation & ( for R being Relation st R = Lr . E holds
( R preserves_No_Comparison_on Lp . E & R c= Lp . E ) ) ) by A17, A16, A14; :: thesis: verum
end;
then reconsider RR = union (rng Lr) as Relation by A14, A10, Th24;
A18: ( RR preserves_No_Comparison_on union (rng Lp) & RR c= union (rng Lp) ) by A15, A14, A10, Th24;
A19: union (rng Lp) c= OpenProd (RR,A,D)
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (rng Lp) or x in OpenProd (RR,A,D) )
assume x in union (rng Lp) ; :: thesis: x in OpenProd (RR,A,D)
then consider Y being set such that
A20: ( x in Y & Y in rng Lp ) by TARSKI:def 4;
consider E being object such that
A21: ( E in dom Lp & Y = Lp . E ) by A20, FUNCT_1:def 3;
reconsider E = E as Ordinal by A21;
reconsider R = Lr . E as Relation by A21, A15;
A22: Lp . E = ClosedProd (R,A,E) by A21, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A15, A14, A10, Th24, A21;
then A23: x in ClosedProd (RR,A,E) by A20, A21, A22, Th15;
ClosedProd (RR,A,E) c= OpenProd (RR,A,D) by Th18, A21, A14;
hence x in OpenProd (RR,A,D) by A23; :: thesis: verum
end;
OpenProd (RR,A,D) c= union (rng Lp)
proof
let x, y be object ; :: according to RELAT_1:def 3 :: thesis: ( not [x,y] in OpenProd (RR,A,D) or [x,y] in union (rng Lp) )
assume A24: [x,y] in OpenProd (RR,A,D) ; :: thesis: [x,y] in union (rng Lp)
A25: ( x in Day (RR,A) & y in Day (RR,A) ) by A24, ZFMISC_1:87;
per cases then ( ( born (RR,x) in A & born (RR,y) in A ) or ( born (RR,x) = A & born (RR,y) in D ) or ( born (RR,x) in D & born (RR,y) = A ) ) by A24, Def9;
suppose A26: ( born (RR,x) in A & born (RR,y) in A ) ; :: thesis: [x,y] in union (rng Lp)
consider B being object such that
A27: B in D by A6, XBOOLE_0:def 1;
reconsider B = B as Ordinal by A27;
consider R being Relation such that
A28: ( Lr . B = R & R preserves_No_Comparison_on ClosedProd (R,A,B) & R c= ClosedProd (R,A,B) ) by A27, A10;
A29: Lp . B = ClosedProd (R,A,B) by A27, A28, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A27, A28, A15, A14, A10, Th24;
then A30: ClosedProd (RR,A,B) = ClosedProd (R,A,B) by Th15;
A31: [x,y] in ClosedProd (RR,A,B) by A26, A25, Def10;
Lp . B in rng Lp by A27, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A30, A29, A31, TARSKI:def 4; :: thesis: verum
end;
suppose A32: ( born (RR,x) = A & born (RR,y) in D ) ; :: thesis: [x,y] in union (rng Lp)
set B = born (RR,y);
consider R being Relation such that
A33: ( Lr . (born (RR,y)) = R & R preserves_No_Comparison_on ClosedProd (R,A,(born (RR,y))) & R c= ClosedProd (R,A,(born (RR,y))) ) by A32, A10;
A34: Lp . (born (RR,y)) = ClosedProd (R,A,(born (RR,y))) by A33, A32, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A32, A33, A15, A14, A10, Th24;
then A35: ClosedProd (RR,A,(born (RR,y))) = ClosedProd (R,A,(born (RR,y))) by Th15;
A36: [x,y] in ClosedProd (RR,A,(born (RR,y))) by A32, A25, Def10;
Lp . (born (RR,y)) in rng Lp by A32, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A35, A34, A36, TARSKI:def 4; :: thesis: verum
end;
suppose A37: ( born (RR,x) in D & born (RR,y) = A ) ; :: thesis: [x,y] in union (rng Lp)
set B = born (RR,x);
consider R being Relation such that
A38: ( Lr . (born (RR,x)) = R & R preserves_No_Comparison_on ClosedProd (R,A,(born (RR,x))) & R c= ClosedProd (R,A,(born (RR,x))) ) by A37, A10;
A39: Lp . (born (RR,x)) = ClosedProd (R,A,(born (RR,x))) by A38, A37, A14;
then RR /\ [:(BeforeGames A),(BeforeGames A):] = R /\ [:(BeforeGames A),(BeforeGames A):] by A37, A38, A15, A14, A10, Th24;
then A40: ClosedProd (RR,A,(born (RR,x))) = ClosedProd (R,A,(born (RR,x))) by Th15;
A41: [x,y] in ClosedProd (RR,A,(born (RR,x))) by A37, A25, Def10;
Lp . (born (RR,x)) in rng Lp by A37, A14, FUNCT_1:def 3;
hence [x,y] in union (rng Lp) by A40, A39, A41, TARSKI:def 4; :: thesis: verum
end;
end;
end;
then OpenProd (RR,A,D) = union (rng Lp) by A19, XBOOLE_0:def 10;
then ex R being Relation st
( RR c= R & R preserves_No_Comparison_on ClosedProd (R,A,D) & R c= ClosedProd (R,A,D) ) by A18, Th26;
hence S1[D] ; :: thesis: verum
end;
end;
end;
for D being Ordinal holds S1[D] from ORDINAL1:sch 2(A2);
 hence ex S being Relation st
( S preserves_No_Comparison_on ClosedProd (S,A,B) & S c= ClosedProd (S,A,B) ) ; :: thesis: verum