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
:: thesis: pcs-union C is pcs-compatible proof
let x,
y,
z be
set ;
:: according to RELAT_2:def 8,
ORDERS_2:def 5 :: thesis: ( 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)
;
:: thesis: ( 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)
;
:: thesis: ( 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)
;
:: thesis: [^,^] 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 ;
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
;
:: thesis: [^,^] 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;
:: thesis: verum end; suppose
C . j c= C . i
;
:: thesis: [^,^] 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;
:: thesis: verum end;
end;
let p, p', q, q' be Element of (pcs-union C); :: according to PCS_0:def 22 :: thesis: ( p (--) q & p' <= p & q' <= q implies p' (--) q' )
assume that
A27:
p (--) q
and
A28:
p' <= p
and
A29:
q' <= q
; :: thesis: p' (--) q'
[p',p] in the InternalRel of (pcs-union C)
by A28, ORDERS_2:def 9;
then consider Z1 being set such that
A30:
[p',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 ;
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 pi = p, p'i = p' as Element of (C . i) by A30, A33, ZFMISC_1:106;
[q',q] in the InternalRel of (pcs-union C)
by A29, ORDERS_2:def 9;
then consider Z2 being set such that
A36:
[q',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:
q' 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
;
:: thesis: p' (--) q'A58:
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:
[p',p] in the
InternalRel of
(C . j)
by A30, A33, A35;
then
[p',p] in the
InternalRel of
(C . k)
by A58;
then reconsider p'k =
p' as
Element of
(C . k) by ZFMISC_1:106;
[q',q] in the
InternalRel of
(C . k)
by A36, A39, A41, A58;
then reconsider q'k =
q' as
Element of
(C . k) by ZFMISC_1:106;
A60:
p'k <= pk
by A58, A59, ORDERS_2:def 9;
A61:
q'k <= qk
by A36, A39, A41, A58, ORDERS_2:def 9;
pk (--) qk
by A44, A47, A48, Def7;
then
p'k (--) q'k
by A60, A61, Def22;
then
[p'k,q'k] in the
ToleranceRel of
(C . k)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A55;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A62:
C . j c= C . i
and A63:
C . i c= C . k
;
:: thesis: p' (--) q'A64:
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;
[p',p] in the
InternalRel of
(C . k)
by A30, A33, A35, A64;
then reconsider p'k =
p' as
Element of
(C . k) by ZFMISC_1:106;
A66:
[q',q] in the
InternalRel of
(C . i)
by A36, A39, A41, A65;
then
[q',q] in the
InternalRel of
(C . k)
by A64;
then reconsider q'k =
q' as
Element of
(C . k) by ZFMISC_1:106;
A67:
p'k <= pk
by A30, A33, A35, A64, ORDERS_2:def 9;
A68:
q'k <= qk
by A64, A66, ORDERS_2:def 9;
pk (--) qk
by A44, A47, A48, Def7;
then
p'k (--) q'k
by A67, A68, Def22;
then
[p'k,q'k] in the
ToleranceRel of
(C . k)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A55;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A69:
C . i c= C . k
and A70:
C . k c= C . j
;
:: thesis: p' (--) q'A71:
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:
[p',p] in the
InternalRel of
(C . k)
by A30, A33, A35;
then A74:
[p',p] in the
InternalRel of
(C . j)
by A71;
then reconsider p'j =
p' as
Element of
(C . j) by ZFMISC_1:106;
reconsider q'j =
q' 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:
p'j <= pj
by A71, A73, ORDERS_2:def 9;
A76:
q'j <= qj
by A36, A39, A41, ORDERS_2:def 9;
pj (--) qj
by A44, A47, A48, A72, Def7;
then
p'j (--) q'j
by A75, A76, Def22;
then
[p'j,q'j] in the
ToleranceRel of
(C . j)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A54;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A77:
C . k c= C . i
and A78:
C . i c= C . j
;
:: thesis: p' (--) q'A79:
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:
[p',p] in the
InternalRel of
(C . j)
by A30, A33, A35, A79;
then reconsider p'j =
p' as
Element of
(C . j) by ZFMISC_1:106;
reconsider q'j =
q' 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:
p'j <= pj
by A30, A33, A35, A79, ORDERS_2:def 9;
A84:
q'j <= qj
by A36, A39, A41, ORDERS_2:def 9;
pi (--) qi
by A44, A47, A48, A81, Def7;
then
pj (--) qj
by A80, Th9;
then
p'j (--) q'j
by A83, A84, Def22;
then
[p'j,q'j] in the
ToleranceRel of
(C . j)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A54;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A85:
C . k c= C . j
and A86:
C . j c= C . i
;
:: thesis: p' (--) q'A87:
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 q'i =
q' 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:
p'i <= pi
by A30, A33, A35, ORDERS_2:def 9;
A91:
q'i <= qi
by A36, A39, A41, A89, ORDERS_2:def 9;
pj (--) qj
by A44, A47, A48, A88, Def7;
then
pi (--) qi
by A87, Th9;
then
p'i (--) q'i
by A90, A91, Def22;
then
[p'i,q'i] in the
ToleranceRel of
(C . i)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A53;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A92:
C . j c= C . k
and A93:
C . k c= C . i
;
:: thesis: p' (--) q'A94:
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 q'k =
q' 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 q'i =
q' as
Element of
(C . i) by A42, A93, Lm3;
reconsider qi =
q as
Element of
(C . i) by A43, A93, A97, Lm3;
A98:
q'k <= qk
by A36, A39, A41, A96, ORDERS_2:def 9;
A99:
p'i <= pi
by A30, A33, A35, ORDERS_2:def 9;
A100:
q'i <= qi
by A95, A98, Th8;
pi (--) qi
by A44, A47, A48, A94, Def7;
then
p'i (--) q'i
by A99, A100, Def22;
then
[p'i,q'i] in the
ToleranceRel of
(C . i)
by Def7;
hence
[p',q'] in the
ToleranceRel of
(pcs-union C)
by A53;
:: according to PCS_0:def 7 :: thesis: verum end;