let R, S be RelStr ; :: thesis: ( the carrier of R /\ the carrier of S is upper Subset of R & the carrier of R /\ the carrier of S is lower Subset of S & R tolerates S & R is transitive & S is transitive implies R [*] S is transitive )
set X = the carrier of (R [*] S);
set F = the InternalRel of (R [*] S);
assume that
A1: the carrier of R /\ the carrier of S is upper Subset of R and
A2: the carrier of R /\ the carrier of S is lower Subset of S and
A3: R tolerates S and
A4: R is transitive and
A5: S is transitive ; :: thesis: R [*] S is transitive
A6: the InternalRel of S is_transitive_in the carrier of S by A5, ORDERS_2:def 3;
A7: the InternalRel of R is_transitive_in the carrier of R by A4, ORDERS_2:def 3;
the InternalRel of (R [*] S) is_transitive_in the carrier of (R [*] S)
proof
let x, y, z be object ; :: according to RELAT_2:def 8 :: thesis: ( not x in the carrier of (R [*] S) or not y in the carrier of (R [*] S) or not z in the carrier of (R [*] S) or not [x,y] in the InternalRel of (R [*] S) or not [y,z] in the InternalRel of (R [*] S) or [x,z] in the InternalRel of (R [*] S) )
assume that
A8: ( x in the carrier of (R [*] S) & y in the carrier of (R [*] S) ) and
A9: z in the carrier of (R [*] S) and
A10: [x,y] in the InternalRel of (R [*] S) and
A11: [y,z] in the InternalRel of (R [*] S) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
A12: ( x in the carrier of R \/ the carrier of S & y in the carrier of R \/ the carrier of S ) by A8, Def2;
A13: z in the carrier of R \/ the carrier of S by A9, Def2;
per cases ( ( x in the carrier of R & y in the carrier of R & z in the carrier of R ) or ( x in the carrier of R & y in the carrier of R & z in the carrier of S ) or ( x in the carrier of R & y in the carrier of S & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of R & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of S & z in the carrier of R ) or ( x in the carrier of S & y in the carrier of S & z in the carrier of S ) or ( x in the carrier of R & y in the carrier of S & z in the carrier of S ) or ( x in the carrier of S & y in the carrier of R & z in the carrier of S ) ) by A12, A13, XBOOLE_0:def 3;
suppose A14: ( x in the carrier of R & y in the carrier of R & z in the carrier of R ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then ( [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) by A3, A4, A10, A11, Th4;
then [x,z] in the InternalRel of R by A7, A14;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose A15: ( x in the carrier of R & y in the carrier of R & z in the carrier of S ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A16: [x,y] in the InternalRel of R by A3, A4, A10, Th4;
[y,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A11, Def2;
then A17: ( [y,z] in the InternalRel of R \/ the InternalRel of S or [y,z] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def 3;
now :: thesis: [x,z] in the InternalRel of (R [*] S)
per cases ( [y,z] in the InternalRel of R or [y,z] in the InternalRel of S or [y,z] in the InternalRel of R * the InternalRel of S ) by A17, XBOOLE_0:def 3;
suppose A18: [y,z] in the InternalRel of R ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then z in the carrier of R by ZFMISC_1:87;
then [x,z] in the InternalRel of R by A7, A15, A16, A18;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose [y,z] in the InternalRel of S ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then [x,z] in the InternalRel of R * the InternalRel of S by A16, RELAT_1:def 8;
then [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [x,z] in the InternalRel of (R [*] S) by Def2; :: thesis: verum
end;
suppose [y,z] in the InternalRel of R * the InternalRel of S ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then consider a being object such that
A19: [y,a] in the InternalRel of R and
A20: [a,z] in the InternalRel of S by RELAT_1:def 8;
a in the carrier of R by A19, ZFMISC_1:87;
then [x,a] in the InternalRel of R by A7, A15, A16, A19;
then [x,z] in the InternalRel of R * the InternalRel of S by A20, RELAT_1:def 8;
then [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [x,z] in the InternalRel of (R [*] S) by Def2; :: thesis: verum
end;
end;
end;
hence [x,z] in the InternalRel of (R [*] S) ; :: thesis: verum
end;
suppose A21: ( x in the carrier of R & y in the carrier of S & z in the carrier of R ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A22: y in the carrier of R by A2, A11, Th21;
then ( [x,y] in the InternalRel of R & [y,z] in the InternalRel of R ) by A3, A4, A10, A11, A21, Th4;
then [x,z] in the InternalRel of R by A7, A21, A22;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose A23: ( x in the carrier of S & y in the carrier of R & z in the carrier of R ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A24: [y,z] in the InternalRel of R by A3, A4, A11, Th4;
A25: x in the carrier of R by A2, A10, A23, Th21;
then [x,y] in the InternalRel of R by A3, A4, A10, A23, Th4;
then [x,z] in the InternalRel of R by A7, A23, A25, A24;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose A26: ( x in the carrier of S & y in the carrier of S & z in the carrier of R ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A27: [x,y] in the InternalRel of S by A3, A5, A10, Th5;
A28: z in the carrier of S by A1, A11, A26, Th17;
then [y,z] in the InternalRel of S by A3, A5, A11, A26, Th5;
then [x,z] in the InternalRel of S by A6, A26, A27, A28;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose A29: ( x in the carrier of S & y in the carrier of S & z in the carrier of S ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then ( [x,y] in the InternalRel of S & [y,z] in the InternalRel of S ) by A3, A5, A10, A11, Th5;
then [x,z] in the InternalRel of S by A6, A29;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose A30: ( x in the carrier of R & y in the carrier of S & z in the carrier of S ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A31: [y,z] in the InternalRel of S by A3, A5, A11, Th5;
[x,y] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by A10, Def2;
then A32: ( [x,y] in the InternalRel of R \/ the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by XBOOLE_0:def 3;
now :: thesis: [x,z] in the InternalRel of (R [*] S)
per cases ( [x,y] in the InternalRel of R or [x,y] in the InternalRel of S or [x,y] in the InternalRel of R * the InternalRel of S ) by A32, XBOOLE_0:def 3;
suppose [x,y] in the InternalRel of R ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then [x,z] in the InternalRel of R * the InternalRel of S by A31, RELAT_1:def 8;
then [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [x,z] in the InternalRel of (R [*] S) by Def2; :: thesis: verum
end;
suppose A33: [x,y] in the InternalRel of S ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then x in the carrier of S by ZFMISC_1:87;
then [x,z] in the InternalRel of S by A6, A30, A31, A33;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
suppose [x,y] in the InternalRel of R * the InternalRel of S ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then consider a being object such that
A34: [x,a] in the InternalRel of R and
A35: [a,y] in the InternalRel of S by RELAT_1:def 8;
a in the carrier of S by A35, ZFMISC_1:87;
then [a,z] in the InternalRel of S by A6, A30, A31, A35;
then [x,z] in the InternalRel of R * the InternalRel of S by A34, RELAT_1:def 8;
then [x,z] in ( the InternalRel of R \/ the InternalRel of S) \/ ( the InternalRel of R * the InternalRel of S) by XBOOLE_0:def 3;
hence [x,z] in the InternalRel of (R [*] S) by Def2; :: thesis: verum
end;
end;
end;
hence [x,z] in the InternalRel of (R [*] S) ; :: thesis: verum
end;
suppose A36: ( x in the carrier of S & y in the carrier of R & z in the carrier of S ) ; :: thesis: [x,z] in the InternalRel of (R [*] S)
then A37: y in the carrier of S by A1, A10, Th17;
then ( [x,y] in the InternalRel of S & [y,z] in the InternalRel of S ) by A3, A5, A10, A11, A36, Th5;
then [x,z] in the InternalRel of S by A6, A36, A37;
hence [x,z] in the InternalRel of (R [*] S) by Th6; :: thesis: verum
end;
end;
end;
hence R [*] S is transitive by ORDERS_2:def 3; :: thesis: verum