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
(
x in the
carrier of
(pcs-union C) &
y in the
carrier of
(pcs-union C) &
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) &
y in the
carrier of
(C . i) )
by A4, A7, ZFMISC_1:106;
A14:
(pcs-InternalRels C) . j = the
InternalRel of
(C . j)
by Def6;
A15:
(
C . i in rng C &
C . j in rng C )
by A3, FUNCT_1:12;
A16:
the
InternalRel of
(C . i) is_transitive_in the
carrier of
(C . i)
by ORDERS_2:def 5;
A17:
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 A15, Def35;
suppose
C . i c= C . j
;
:: thesis: [^,^] in the InternalRel of (pcs-union C)then A18:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by Def34;
then
[x,y] in the
InternalRel of
(C . j)
by A4, A7, A12;
then
(
x in the
carrier of
(C . j) &
y in the
carrier of
(C . j) &
z in the
carrier of
(C . j) )
by A8, A11, A14, ZFMISC_1:106;
then A19:
[x,z] in the
InternalRel of
(C . j)
by A4, A7, A8, A11, A12, A14, A17, A18, RELAT_2:def 8;
the
InternalRel of
(C . j) c= the
InternalRel of
(pcs-union C)
by A1, A9, A11, A14, ZFMISC_1:92;
hence
[^,^] in the
InternalRel of
(pcs-union C)
by A19;
:: thesis: verum end; suppose
C . j c= C . i
;
:: thesis: [^,^] in the InternalRel of (pcs-union C)then A20:
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, A14;
then
z in the
carrier of
(C . i)
by ZFMISC_1:106;
then A21:
[x,z] in the
InternalRel of
(C . i)
by A4, A7, A8, A11, A12, A13, A14, A16, A20, 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 A21;
:: 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
A22:
p (--) q
and
A23:
p' <= p
and
A24:
q' <= q
; :: thesis: p' (--) q'
[p',p] in the InternalRel of (pcs-union C)
by A23, ORDERS_2:def 9;
then consider Z1 being set such that
A25:
[p',p] in Z1
and
A26:
Z1 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider i being set such that
A27:
i in dom (pcs-InternalRels C)
and
A28:
(pcs-InternalRels C) . i = Z1
by A26, FUNCT_1:def 5;
reconsider I = I as non empty set by A27, PARTFUN1:def 4;
reconsider C = C as pcs-Chain of ;
reconsider i = i as Element of I by A27, PARTFUN1:def 4;
A29:
(pcs-ToleranceRels C) . i = the ToleranceRel of (C . i)
by Def20;
A30:
(pcs-InternalRels C) . i = the InternalRel of (C . i)
by Def6;
then reconsider pi = p, p'i = p' as Element of (C . i) by A25, A28, ZFMISC_1:106;
[q',q] in the InternalRel of (pcs-union C)
by A24, ORDERS_2:def 9;
then consider Z2 being set such that
A31:
[q',q] in Z2
and
A32:
Z2 in rng (pcs-InternalRels C)
by A1, TARSKI:def 4;
consider j being set such that
A33:
j in dom (pcs-InternalRels C)
and
A34:
(pcs-InternalRels C) . j = Z2
by A32, FUNCT_1:def 5;
reconsider j = j as Element of I by A33, PARTFUN1:def 4;
A35:
(pcs-ToleranceRels C) . j = the ToleranceRel of (C . j)
by Def20;
A36:
(pcs-InternalRels C) . j = the InternalRel of (C . j)
by Def6;
then A37:
( q' in the carrier of (C . j) & q in the carrier of (C . j) )
by A31, A34, ZFMISC_1:106;
reconsider qj = q as Element of (C . j) by A31, A34, A36, ZFMISC_1:106;
[p,q] in the ToleranceRel of (pcs-union C)
by A22, Def7;
then consider Z3 being set such that
A38:
[p,q] in Z3
and
A39:
Z3 in rng (pcs-ToleranceRels C)
by A2, TARSKI:def 4;
consider k being set such that
A40:
k in dom (pcs-ToleranceRels C)
and
A41:
(pcs-ToleranceRels C) . k = Z3
by A39, FUNCT_1:def 5;
reconsider k = k as Element of I by A40, PARTFUN1:def 4;
A42:
(pcs-ToleranceRels C) . k = the ToleranceRel of (C . k)
by Def20;
then reconsider pk = p, qk = q as Element of (C . k) by A38, A41, ZFMISC_1:106;
A43:
( C . i in rng C & C . j in rng C & C . k in rng C )
by A3, FUNCT_1:12;
A44:
dom (pcs-ToleranceRels C) = I
by PARTFUN1:def 4;
then A45:
the ToleranceRel of (C . i) c= the ToleranceRel of (pcs-union C)
by A2, A29, FUNCT_1:12, ZFMISC_1:92;
A46:
the ToleranceRel of (C . j) c= the ToleranceRel of (pcs-union C)
by A2, A35, A44, FUNCT_1:12, ZFMISC_1:92;
A47:
the ToleranceRel of (C . k) c= the ToleranceRel of (pcs-union C)
by A2, A39, A41, A42, 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 A43, Def35;
suppose that A48:
C . i c= C . j
and A49:
C . j c= C . k
;
:: thesis: p' (--) q'A50:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . k)
by A49, Def34;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by A48, Def34;
then A51:
[p',p] in the
InternalRel of
(C . j)
by A25, A28, A30;
then
[p',p] in the
InternalRel of
(C . k)
by A50;
then reconsider p'k =
p' as
Element of
(C . k) by ZFMISC_1:106;
[q',q] in the
InternalRel of
(C . k)
by A31, A34, A36, A50;
then reconsider q'k =
q' as
Element of
(C . k) by ZFMISC_1:106;
A52:
(
p'k <= pk &
q'k <= qk )
by A31, A34, A36, A50, A51, ORDERS_2:def 9;
pk (--) qk
by A38, A41, A42, Def7;
then
p'k (--) q'k
by A52, 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 A47;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A53:
C . j c= C . i
and A54:
C . i c= C . k
;
:: thesis: p' (--) q'A55:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . k)
by A54, Def34;
A56:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A53, Def34;
[p',p] in the
InternalRel of
(C . k)
by A25, A28, A30, A55;
then reconsider p'k =
p' as
Element of
(C . k) by ZFMISC_1:106;
A57:
[q',q] in the
InternalRel of
(C . i)
by A31, A34, A36, A56;
then
[q',q] in the
InternalRel of
(C . k)
by A55;
then reconsider q'k =
q' as
Element of
(C . k) by ZFMISC_1:106;
A58:
(
p'k <= pk &
q'k <= qk )
by A25, A28, A30, A55, A57, ORDERS_2:def 9;
pk (--) qk
by A38, A41, A42, Def7;
then
p'k (--) q'k
by A58, 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 A47;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A59:
C . i c= C . k
and A60:
C . k c= C . j
;
:: thesis: p' (--) q'A61:
the
InternalRel of
(C . k) c= the
InternalRel of
(C . j)
by A60, Def34;
A62:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A60, Def34;
the
InternalRel of
(C . i) c= the
InternalRel of
(C . k)
by A59, Def34;
then A63:
[p',p] in the
InternalRel of
(C . k)
by A25, A28, A30;
then A64:
[p',p] in the
InternalRel of
(C . j)
by A61;
then reconsider p'j =
p' as
Element of
(C . j) by ZFMISC_1:106;
reconsider q'j =
q' as
Element of
(C . j) by A31, A34, A36, ZFMISC_1:106;
reconsider pj =
p as
Element of
(C . j) by A64, ZFMISC_1:106;
A65:
(
p'j <= pj &
q'j <= qj )
by A31, A34, A36, A61, A63, ORDERS_2:def 9;
pj (--) qj
by A38, A41, A42, A62, Def7;
then
p'j (--) q'j
by A65, 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 A46;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A66:
C . k c= C . i
and A67:
C . i c= C . j
;
:: thesis: p' (--) q'A68:
the
InternalRel of
(C . i) c= the
InternalRel of
(C . j)
by A67, Def34;
A69:
the
ToleranceRel of
(C . i) c= the
ToleranceRel of
(C . j)
by A67, Def34;
A70:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . i)
by A66, Def34;
A71:
[p',p] in the
InternalRel of
(C . j)
by A25, A28, A30, A68;
then reconsider p'j =
p' as
Element of
(C . j) by ZFMISC_1:106;
reconsider q'j =
q' as
Element of
(C . j) by A31, A34, A36, ZFMISC_1:106;
reconsider pj =
p as
Element of
(C . j) by A71, ZFMISC_1:106;
q in the
carrier of
(C . k)
by A38, A41, A42, ZFMISC_1:106;
then reconsider qi =
q as
Element of
(C . i) by A66, Lm3;
A72:
(
p'j <= pj &
q'j <= qj )
by A25, A28, A30, A31, A34, A36, A68, ORDERS_2:def 9;
pi (--) qi
by A38, A41, A42, A70, Def7;
then
pj (--) qj
by A69, Th9;
then
p'j (--) q'j
by A72, 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 A46;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A73:
C . k c= C . j
and A74:
C . j c= C . i
;
:: thesis: p' (--) q'A75:
the
ToleranceRel of
(C . j) c= the
ToleranceRel of
(C . i)
by A74, Def34;
A76:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . j)
by A73, Def34;
A77:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . i)
by A74, Def34;
reconsider q'i =
q' as
Element of
(C . i) by A37, A74, Lm3;
reconsider qi =
q as
Element of
(C . i) by A37, A74, Lm3;
p in the
carrier of
(C . k)
by A38, A41, A42, ZFMISC_1:106;
then reconsider pj =
p as
Element of
(C . j) by A73, Lm3;
A78:
(
p'i <= pi &
q'i <= qi )
by A25, A28, A30, A31, A34, A36, A77, ORDERS_2:def 9;
pj (--) qj
by A38, A41, A42, A76, Def7;
then
pi (--) qi
by A75, Th9;
then
p'i (--) q'i
by A78, 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 A45;
:: according to PCS_0:def 7 :: thesis: verum end; suppose that A79:
C . j c= C . k
and A80:
C . k c= C . i
;
:: thesis: p' (--) q'A81:
the
ToleranceRel of
(C . k) c= the
ToleranceRel of
(C . i)
by A80, Def34;
A82:
the
InternalRel of
(C . k) c= the
InternalRel of
(C . i)
by A80, Def34;
A83:
the
InternalRel of
(C . j) c= the
InternalRel of
(C . k)
by A79, Def34;
reconsider q'k =
q' as
Element of
(C . k) by A37, A79, Lm3;
A84:
the
carrier of
(C . j) c= the
carrier of
(C . k)
by A79, Def34;
then reconsider q'i =
q' as
Element of
(C . i) by A37, A80, Lm3;
reconsider qi =
q as
Element of
(C . i) by A37, A80, A84, Lm3;
q'k <= qk
by A31, A34, A36, A83, ORDERS_2:def 9;
then A85:
(
p'i <= pi &
q'i <= qi )
by A25, A28, A30, A82, Th8, ORDERS_2:def 9;
pi (--) qi
by A38, A41, A42, A81, Def7;
then
p'i (--) q'i
by A85, 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 A45;
:: according to PCS_0:def 7 :: thesis: verum end;