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 4;
thus
pcs-union C is transitive
pcs-union C is pcs-compatible proof
let x,
y,
z be
set ;
RELAT_2:def 8,
ORDERS_2:def 5 ( 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
set such that A6:
i in dom (pcs-InternalRels C)
and A7:
(pcs-InternalRels C) . i = Z1
by A5, FUNCT_1:def 5;
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
set such that A10:
j in dom (pcs-InternalRels C)
and A11:
(pcs-InternalRels C) . j = Z2
by A9, FUNCT_1:def 5;
reconsider I =
I as non
empty set by A6, PARTFUN1:def 4;
reconsider C =
C as
pcs-Chain of
I ;
reconsider i =
i,
j =
j as
Element of
I by A6, A10, PARTFUN1:def 4;
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:106;
A14:
y in the
carrier of
(C . i)
by A4, A7, A12, ZFMISC_1:106;
A15:
(pcs-InternalRels C) . j = the
InternalRel of
(C . j)
by Def6;
A16:
C . i in rng C
by A3, FUNCT_1:12;
A17:
C . j in rng C
by A3, FUNCT_1:12;
A18:
the
InternalRel of
(C . i) is_transitive_in the
carrier of
(C . i)
by ORDERS_2:def 5;
A19:
the
InternalRel of
(C . j) is_transitive_in the
carrier of
(C . j)
by ORDERS_2:def 5;
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)
by Def34;
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:106;
A23:
y in the
carrier of
(C . j)
by A21, ZFMISC_1:106;
z in the
carrier of
(C . j)
by A8, A11, A15, ZFMISC_1:106;
then A24:
[x,z] in the
InternalRel of
(C . j)
by A4, A7, A8, A11, A12, A15, A19, A20, A22, A23, RELAT_2:def 8;
the
InternalRel of
(C . j) c= the
InternalRel of
(pcs-union C)
by A1, A9, A11, A15, ZFMISC_1:92;
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)
by Def34;
then
[y,z] in the
InternalRel of
(C . i)
by A8, A11, A15;
then
z in the
carrier of
(C . i)
by ZFMISC_1:106;
then A26:
[x,z] in the
InternalRel of
(C . i)
by A4, A7, A8, A11, A12, A13, A14, A15, A18, A25, RELAT_2:def 8;
the
InternalRel of
(C . i) c= the
InternalRel of
(pcs-union C)
by A1, A5, A7, A12, ZFMISC_1:92;
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, ORDERS_2:def 9;
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 set such that
A32:
i in dom (pcs-InternalRels C)
and
A33:
(pcs-InternalRels C) . i = Z1
by A31, FUNCT_1:def 5;
reconsider I = I as non empty set by A32, PARTFUN1:def 4;
reconsider C = C as pcs-Chain of I ;
reconsider i = i as Element of I by A32, PARTFUN1:def 4;
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:106;
[q9,q] in the InternalRel of (pcs-union C)
by A29, ORDERS_2:def 9;
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 set such that
A38:
j in dom (pcs-InternalRels C)
and
A39:
(pcs-InternalRels C) . j = Z2
by A37, FUNCT_1:def 5;
reconsider j = j as Element of I by A38, PARTFUN1:def 4;
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:106;
A43:
q in the carrier of (C . j)
by A36, A39, A41, ZFMISC_1:106;
reconsider qj = q as Element of (C . j) by A36, A39, A41, ZFMISC_1:106;
[p,q] in the ToleranceRel of (pcs-union C)
by A27, Def7;
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 set such that
A46:
k in dom (pcs-ToleranceRels C)
and
A47:
(pcs-ToleranceRels C) . k = Z3
by A45, FUNCT_1:def 5;
reconsider k = k as Element of I by A46, PARTFUN1:def 4;
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:106;
A49:
C . i in rng C
by A3, FUNCT_1:12;
A50:
C . j in rng C
by A3, FUNCT_1:12;
A51:
C . k in rng C
by A3, FUNCT_1:12;
A52:
dom (pcs-ToleranceRels C) = I
by PARTFUN1:def 4;
then A53:
the ToleranceRel of (C . i) c= the ToleranceRel of (pcs-union C)
by A2, A34, FUNCT_1:12, ZFMISC_1:92;
A54:
the ToleranceRel of (C . j) c= the ToleranceRel of (pcs-union C)
by A2, A40, A52, FUNCT_1:12, ZFMISC_1:92;
A55:
the ToleranceRel of (C . k) c= the ToleranceRel of (pcs-union C)
by A2, A45, A47, A48, ZFMISC_1:92;
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, Def34;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by A56, Def34;
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:106;
[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:106;
A60:
p9k <= pk
by A58, A59, ORDERS_2:def 9;
A61:
q9k <= qk
by A36, A39, A41, A58, ORDERS_2:def 9;
pk (--) qk
by A44, A47, A48, Def7;
then
p9k (--) q9k
by A60, A61, Def22;
then
[p9k,q9k] in the
ToleranceRel of
(C . k)
by Def7;
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, Def34;
A65:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A62, Def34;
[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:106;
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:106;
A67:
p9k <= pk
by A30, A33, A35, A64, ORDERS_2:def 9;
A68:
q9k <= qk
by A64, A66, ORDERS_2:def 9;
pk (--) qk
by A44, A47, A48, Def7;
then
p9k (--) q9k
by A67, A68, Def22;
then
[p9k,q9k] in the
ToleranceRel of
(C . k)
by Def7;
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, Def34;
A72:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A70, Def34;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . k)
by A69, Def34;
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:106;
reconsider q9j =
q9 as
Element of
(C . j) by A36, A39, A41, ZFMISC_1:106;
reconsider pj =
p as
Element of
(C . j) by A74, ZFMISC_1:106;
A75:
p9j <= pj
by A71, A73, ORDERS_2:def 9;
A76:
q9j <= qj
by A36, A39, A41, ORDERS_2:def 9;
pj (--) qj
by A44, A47, A48, A72, Def7;
then
p9j (--) q9j
by A75, A76, Def22;
then
[p9j,q9j] in the
ToleranceRel of
(C . j)
by Def7;
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, Def34;
A80:
the
ToleranceRel of
(C . i) c= the
ToleranceRel of
(C . j)
by A78, Def34;
A81:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . i)
by A77, Def34;
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:106;
reconsider q9j =
q9 as
Element of
(C . j) by A36, A39, A41, ZFMISC_1:106;
reconsider pj =
p as
Element of
(C . j) by A82, ZFMISC_1:106;
q in the
carrier of
(C . k)
by A44, A47, A48, ZFMISC_1:106;
then reconsider qi =
q as
Element of
(C . i) by A77, Lm3;
A83:
p9j <= pj
by A30, A33, A35, A79, ORDERS_2:def 9;
A84:
q9j <= qj
by A36, A39, A41, ORDERS_2:def 9;
pi1 (--) qi
by A44, A47, A48, A81, Def7;
then
pj (--) qj
by A80, Th9;
then
p9j (--) q9j
by A83, A84, Def22;
then
[p9j,q9j] in the
ToleranceRel of
(C . j)
by Def7;
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, Def34;
A88:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A85, Def34;
A89:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A86, Def34;
reconsider q9i =
q9 as
Element of
(C . i) by A42, A86, Lm3;
reconsider qi =
q as
Element of
(C . i) by A43, A86, Lm3;
p in the
carrier of
(C . k)
by A44, A47, A48, ZFMISC_1:106;
then reconsider pj =
p as
Element of
(C . j) by A85, Lm3;
A90:
p9i <= pi1
by A30, A33, A35, ORDERS_2:def 9;
A91:
q9i <= qi
by A36, A39, A41, A89, ORDERS_2:def 9;
pj (--) qj
by A44, A47, A48, A88, Def7;
then
pi1 (--) qi
by A87, Th9;
then
p9i (--) q9i
by A90, A91, Def22;
then
[p9i,q9i] in the
ToleranceRel of
(C . i)
by Def7;
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, Def34;
A95:
the
InternalRel of
(C . k) c= the
InternalRel of
(C . i)
by A93, Def34;
A96:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . k)
by A92, Def34;
reconsider q9k =
q9 as
Element of
(C . k) by A42, A92, Lm3;
A97:
the
carrier of
(C . j) c= the
carrier of
(C . k)
by A92, Def34;
then reconsider q9i =
q9 as
Element of
(C . i) by A42, A93, Lm3;
reconsider qi =
q as
Element of
(C . i) by A43, A93, A97, Lm3;
A98:
q9k <= qk
by A36, A39, A41, A96, ORDERS_2:def 9;
A99:
p9i <= pi1
by A30, A33, A35, ORDERS_2:def 9;
A100:
q9i <= qi
by A95, A98, Th8;
pi1 (--) qi
by A44, A47, A48, A94, Def7;
then
p9i (--) q9i
by A99, A100, Def22;
then
[p9i,q9i] in the
ToleranceRel of
(C . i)
by Def7;
hence
[p9,q9] in the
ToleranceRel of
(pcs-union C)
by A53;
PCS_0:def 7 verum end;