set P = pcs-union C;
set IR = the InternalRel of (pcs-union C);
set TR = the ToleranceRel of (pcs-union C);
set CA = the carrier of (pcs-union C);
A1:
the InternalRel of (pcs-union C) = Union (pcs-InternalRels C)
by Def36;
A2:
the ToleranceRel of (pcs-union C) = Union (pcs-ToleranceRels C)
by Def36;
A3:
dom C = I
by PARTFUN1:def 2;
thus
pcs-union C is transitive
pcs-union C is pcs-compatible proof
let x,
y,
z be
object ;
RELAT_2:def 8,
ORDERS_2:def 3 ( not x in the carrier of (pcs-union C) or not y in the carrier of (pcs-union C) or not z in the carrier of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) )
assume that
x in the
carrier of
(pcs-union C)
and
y in the
carrier of
(pcs-union C)
and
z in the
carrier of
(pcs-union C)
;
( not [^,^] in the InternalRel of (pcs-union C) or not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) )
assume
[x,y] in the
InternalRel of
(pcs-union C)
;
( not [^,^] in the InternalRel of (pcs-union C) or [^,^] in the InternalRel of (pcs-union C) )
then consider Z1 being
set such that A4:
[x,y] in Z1
and A5:
Z1 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider i being
object such that A6:
i in dom (pcs-InternalRels C)
and A7:
(pcs-InternalRels C) . i = Z1
by A5, FUNCT_1:def 3;
assume
[y,z] in the
InternalRel of
(pcs-union C)
;
[^,^] in the InternalRel of (pcs-union C)
then consider Z2 being
set such that A8:
[y,z] in Z2
and A9:
Z2 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider j being
object such that A10:
j in dom (pcs-InternalRels C)
and A11:
(pcs-InternalRels C) . j = Z2
by A9, FUNCT_1:def 3;
reconsider I =
I as non
empty set by A6;
reconsider C =
C as
pcs-Chain of
I ;
reconsider i =
i,
j =
j as
Element of
I by A6, A10;
A12:
(pcs-InternalRels C) . i = the
InternalRel of
(C . i)
by Def6;
then A13:
x in the
carrier of
(C . i)
by A4, A7, ZFMISC_1:87;
A14:
y in the
carrier of
(C . i)
by A4, A7, A12, ZFMISC_1:87;
A15:
(pcs-InternalRels C) . j = the
InternalRel of
(C . j)
by Def6;
A16:
C . i in rng C
by A3, FUNCT_1:3;
A17:
C . j in rng C
by A3, FUNCT_1:3;
A18:
the
InternalRel of
(C . i) is_transitive_in the
carrier of
(C . i)
by ORDERS_2:def 3;
A19:
the
InternalRel of
(C . j) is_transitive_in the
carrier of
(C . j)
by ORDERS_2:def 3;
per cases
( C . i c= C . j or C . j c= C . i )
by A16, A17, Def35;
suppose
C . i c= C . j
;
[^,^] in the InternalRel of (pcs-union C)then A20:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
;
then A21:
[x,y] in the
InternalRel of
(C . j)
by A4, A7, A12;
then A22:
x in the
carrier of
(C . j)
by ZFMISC_1:87;
A23:
y in the
carrier of
(C . j)
by A21, ZFMISC_1:87;
z in the
carrier of
(C . j)
by A8, A11, A15, ZFMISC_1:87;
then A24:
[x,z] in the
InternalRel of
(C . j)
by A4, A7, A8, A11, A12, A15, A19, A20, A22, A23;
the
InternalRel of
(C . j) c= the
InternalRel of
(pcs-union C)
by A1, A9, A11, A15, ZFMISC_1:74;
hence
[^,^] in the
InternalRel of
(pcs-union C)
by A24;
verum end; suppose
C . j c= C . i
;
[^,^] in the InternalRel of (pcs-union C)then A25:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
;
then
[y,z] in the
InternalRel of
(C . i)
by A8, A11, A15;
then
z in the
carrier of
(C . i)
by ZFMISC_1:87;
then A26:
[x,z] in the
InternalRel of
(C . i)
by A4, A7, A8, A11, A12, A13, A14, A15, A18, A25;
the
InternalRel of
(C . i) c= the
InternalRel of
(pcs-union C)
by A1, A5, A7, A12, ZFMISC_1:74;
hence
[^,^] in the
InternalRel of
(pcs-union C)
by A26;
verum end;
end;
let p, p9, q, q9 be Element of (pcs-union C); PCS_0:def 22 ( p (--) q & p9 <= p & q9 <= q implies p9 (--) q9 )
assume that
A27:
p (--) q
and
A28:
p9 <= p
and
A29:
q9 <= q
; p9 (--) q9
[p9,p] in the InternalRel of (pcs-union C)
by A28;
then consider Z1 being set such that
A30:
[p9,p] in Z1
and
A31:
Z1 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider i being object such that
A32:
i in dom (pcs-InternalRels C)
and
A33:
(pcs-InternalRels C) . i = Z1
by A31, FUNCT_1:def 3;
reconsider I = I as non empty set by A32;
reconsider C = C as pcs-Chain of I ;
reconsider i = i as Element of I by A32;
A34:
(pcs-ToleranceRels C) . i = the ToleranceRel of (C . i)
by Def20;
A35:
(pcs-InternalRels C) . i = the InternalRel of (C . i)
by Def6;
then reconsider pi1 = p, p9i = p9 as Element of (C . i) by A30, A33, ZFMISC_1:87;
[q9,q] in the InternalRel of (pcs-union C)
by A29;
then consider Z2 being set such that
A36:
[q9,q] in Z2
and
A37:
Z2 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider j being object such that
A38:
j in dom (pcs-InternalRels C)
and
A39:
(pcs-InternalRels C) . j = Z2
by A37, FUNCT_1:def 3;
reconsider j = j as Element of I by A38;
A40:
(pcs-ToleranceRels C) . j = the ToleranceRel of (C . j)
by Def20;
A41:
(pcs-InternalRels C) . j = the InternalRel of (C . j)
by Def6;
then A42:
q9 in the carrier of (C . j)
by A36, A39, ZFMISC_1:87;
A43:
q in the carrier of (C . j)
by A36, A39, A41, ZFMISC_1:87;
reconsider qj = q as Element of (C . j) by A36, A39, A41, ZFMISC_1:87;
[p,q] in the ToleranceRel of (pcs-union C)
by A27;
then consider Z3 being set such that
A44:
[p,q] in Z3
and
A45:
Z3 in rng (pcs-ToleranceRels C)
by A2, TARSKI:def 4;
consider k being object such that
A46:
k in dom (pcs-ToleranceRels C)
and
A47:
(pcs-ToleranceRels C) . k = Z3
by A45, FUNCT_1:def 3;
reconsider k = k as Element of I by A46;
A48:
(pcs-ToleranceRels C) . k = the ToleranceRel of (C . k)
by Def20;
then reconsider pk = p, qk = q as Element of (C . k) by A44, A47, ZFMISC_1:87;
A49:
C . i in rng C
by A3, FUNCT_1:3;
A50:
C . j in rng C
by A3, FUNCT_1:3;
A51:
C . k in rng C
by A3, FUNCT_1:3;
A52:
dom (pcs-ToleranceRels C) = I
by PARTFUN1:def 2;
then A53:
the ToleranceRel of (C . i) c= the ToleranceRel of (pcs-union C)
by A2, A34, FUNCT_1:3, ZFMISC_1:74;
A54:
the ToleranceRel of (C . j) c= the ToleranceRel of (pcs-union C)
by A2, A40, A52, FUNCT_1:3, ZFMISC_1:74;
A55:
the ToleranceRel of (C . k) c= the ToleranceRel of (pcs-union C)
by A2, A45, A47, A48, ZFMISC_1:74;
per cases
( ( C . i c= C . j & C . j c= C . k ) or ( C . j c= C . i & C . i c= C . k ) or ( C . i c= C . k & C . k c= C . j ) or ( C . k c= C . i & C . i c= C . j ) or ( C . k c= C . j & C . j c= C . i ) or ( C . j c= C . k & C . k c= C . i ) )
by A49, A50, A51, Def35;
suppose that A56:
C . i c= C . j
and A57:
C . j c= C . k
;
p9 (--) q9A58:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . k)
by A57;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by A56;
then A59:
[p9,p] in the
InternalRel of
(C . j)
by A30, A33, A35;
then
[p9,p] in the
InternalRel of
(C . k)
by A58;
then reconsider p9k =
p9 as
Element of
(C . k) by ZFMISC_1:87;
[q9,q] in the
InternalRel of
(C . k)
by A36, A39, A41, A58;
then reconsider q9k =
q9 as
Element of
(C . k) by ZFMISC_1:87;
A60:
p9k <= pk
by A58, A59;
A61:
q9k <= qk
by A36, A39, A41, A58;
pk (--) qk
by A44, A47, A48;
then
p9k (--) q9k
by A60, A61, Def22;
then
[p9k,q9k] in the
ToleranceRel of
(C . k)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A55;
PCS_0:def 7 verum end; suppose that A62:
C . j c= C . i
and A63:
C . i c= C . k
;
p9 (--) q9A64:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . k)
by A63;
A65:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A62;
[p9,p] in the
InternalRel of
(C . k)
by A30, A33, A35, A64;
then reconsider p9k =
p9 as
Element of
(C . k) by ZFMISC_1:87;
A66:
[q9,q] in the
InternalRel of
(C . i)
by A36, A39, A41, A65;
then
[q9,q] in the
InternalRel of
(C . k)
by A64;
then reconsider q9k =
q9 as
Element of
(C . k) by ZFMISC_1:87;
A67:
p9k <= pk
by A30, A33, A35, A64;
A68:
q9k <= qk
by A64, A66;
pk (--) qk
by A44, A47, A48;
then
p9k (--) q9k
by A67, A68, Def22;
then
[p9k,q9k] in the
ToleranceRel of
(C . k)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A55;
PCS_0:def 7 verum end; suppose that A69:
C . i c= C . k
and A70:
C . k c= C . j
;
p9 (--) q9A71:
the
InternalRel of
(C . k) c= the
InternalRel of
(C . j)
by A70;
A72:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A70;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . k)
by A69;
then A73:
[p9,p] in the
InternalRel of
(C . k)
by A30, A33, A35;
then A74:
[p9,p] in the
InternalRel of
(C . j)
by A71;
then reconsider p9j =
p9 as
Element of
(C . j) by ZFMISC_1:87;
reconsider q9j =
q9 as
Element of
(C . j) by A36, A39, A41, ZFMISC_1:87;
reconsider pj =
p as
Element of
(C . j) by A74, ZFMISC_1:87;
A75:
p9j <= pj
by A71, A73;
A76:
q9j <= qj
by A36, A39, A41;
pj (--) qj
by A44, A47, A48, A72;
then
p9j (--) q9j
by A75, A76, Def22;
then
[p9j,q9j] in the
ToleranceRel of
(C . j)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A54;
PCS_0:def 7 verum end; suppose that A77:
C . k c= C . i
and A78:
C . i c= C . j
;
p9 (--) q9A79:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by A78;
A80:
the
ToleranceRel of
(C . i) c= the
ToleranceRel of
(C . j)
by A78;
A81:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . i)
by A77;
A82:
[p9,p] in the
InternalRel of
(C . j)
by A30, A33, A35, A79;
then reconsider p9j =
p9 as
Element of
(C . j) by ZFMISC_1:87;
reconsider q9j =
q9 as
Element of
(C . j) by A36, A39, A41, ZFMISC_1:87;
reconsider pj =
p as
Element of
(C . j) by A82, ZFMISC_1:87;
q in the
carrier of
(C . k)
by A44, A47, A48, ZFMISC_1:87;
then reconsider qi =
q as
Element of
(C . i) by A77;
A83:
p9j <= pj
by A30, A33, A35, A79;
A84:
q9j <= qj
by A36, A39, A41;
pi1 (--) qi
by A44, A47, A48, A81;
then
pj (--) qj
by A80;
then
p9j (--) q9j
by A83, A84, Def22;
then
[p9j,q9j] in the
ToleranceRel of
(C . j)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A54;
PCS_0:def 7 verum end; suppose that A85:
C . k c= C . j
and A86:
C . j c= C . i
;
p9 (--) q9A87:
the
ToleranceRel of
(C . j) c= the
ToleranceRel of
(C . i)
by A86;
A88:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A85;
A89:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A86;
reconsider q9i =
q9 as
Element of
(C . i) by A42, A86;
reconsider qi =
q as
Element of
(C . i) by A43, A86;
p in the
carrier of
(C . k)
by A44, A47, A48, ZFMISC_1:87;
then reconsider pj =
p as
Element of
(C . j) by A85;
A90:
p9i <= pi1
by A30, A33, A35;
A91:
q9i <= qi
by A36, A39, A41, A89;
pj (--) qj
by A44, A47, A48, A88;
then
pi1 (--) qi
by A87;
then
p9i (--) q9i
by A90, A91, Def22;
then
[p9i,q9i] in the
ToleranceRel of
(C . i)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A53;
PCS_0:def 7 verum end; suppose that A92:
C . j c= C . k
and A93:
C . k c= C . i
;
p9 (--) q9A94:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . i)
by A93;
A95:
the
InternalRel of
(C . k) c= the
InternalRel of
(C . i)
by A93;
A96:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . k)
by A92;
reconsider q9k =
q9 as
Element of
(C . k) by A42, A92;
A97:
the
carrier of
(C . j) c= the
carrier of
(C . k)
by A92;
then reconsider q9i =
q9 as
Element of
(C . i) by A42, A93, Lm2;
reconsider qi =
q as
Element of
(C . i) by A43, A93, A97, Lm2;
A98:
q9k <= qk
by A36, A39, A41, A96;
A99:
p9i <= pi1
by A30, A33, A35;
A100:
q9i <= qi
by A95, A98;
pi1 (--) qi
by A44, A47, A48, A94;
then
p9i (--) q9i
by A99, A100, Def22;
then
[p9i,q9i] in the
ToleranceRel of
(C . i)
;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A53;
PCS_0:def 7 verum end;