set CA = Carrier C;
set IRA = pcs-InternalRels C;
set TRA = pcs-ToleranceRels C;
set D = Union (Carrier C);
set IR = Union (pcs-InternalRels C);
set TR = Union (pcs-ToleranceRels C);
A1:
dom (Carrier C) = I
by PARTFUN1:def 4;
Union (pcs-InternalRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):]
proof
let x be
set ;
TARSKI:def 3 ( not x in Union (pcs-InternalRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-InternalRels C)
;
x in [:(Union (Carrier C)),(Union (Carrier C)):]
then consider P being
set such that A2:
x in P
and A3:
P in rng (pcs-InternalRels C)
by TARSKI:def 4;
consider i being
set such that A4:
i in dom (pcs-InternalRels C)
and A5:
(pcs-InternalRels C) . i = P
by A3, FUNCT_1:def 5;
A6:
dom (pcs-InternalRels C) = I
by PARTFUN1:def 4;
then consider R being
RelStr such that A7:
R = C . i
and A8:
(pcs-InternalRels C) . i = the
InternalRel of
R
by A4, Def5;
consider x1,
x2 being
set such that A9:
x = [x1,x2]
and A10:
x1 in the
carrier of
R
and A11:
x2 in the
carrier of
R
by A2, A5, A8, RELSET_1:6;
ex
S being
1-sorted st
(
S = C . i &
(Carrier C) . i = the
carrier of
S )
by A4, A6, PRALG_1:def 13;
then A12:
the
carrier of
R in rng (Carrier C)
by A1, A4, A6, A7, FUNCT_1:def 5;
then A13:
x1 in union (rng (Carrier C))
by A10, TARSKI:def 4;
x2 in union (rng (Carrier C))
by A11, A12, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A9, A13, ZFMISC_1:106;
verum
end;
then reconsider IR = Union (pcs-InternalRels C) as Relation of (Union (Carrier C)) ;
Union (pcs-ToleranceRels C) c= [:(Union (Carrier C)),(Union (Carrier C)):]
proof
let x be
set ;
TARSKI:def 3 ( not x in Union (pcs-ToleranceRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-ToleranceRels C)
;
x in [:(Union (Carrier C)),(Union (Carrier C)):]
then consider P being
set such that A14:
x in P
and A15:
P in rng (pcs-ToleranceRels C)
by TARSKI:def 4;
consider i being
set such that A16:
i in dom (pcs-ToleranceRels C)
and A17:
(pcs-ToleranceRels C) . i = P
by A15, FUNCT_1:def 5;
A18:
dom (pcs-ToleranceRels C) = I
by PARTFUN1:def 4;
then consider R being
TolStr such that A19:
R = C . i
and A20:
(pcs-ToleranceRels C) . i = the
ToleranceRel of
R
by A16, Def19;
consider x1,
x2 being
set such that A21:
x = [x1,x2]
and A22:
x1 in the
carrier of
R
and A23:
x2 in the
carrier of
R
by A14, A17, A20, RELSET_1:6;
ex
S being
1-sorted st
(
S = C . i &
(Carrier C) . i = the
carrier of
S )
by A16, A18, PRALG_1:def 13;
then A24:
the
carrier of
R in rng (Carrier C)
by A1, A16, A18, A19, FUNCT_1:def 5;
then A25:
x1 in union (rng (Carrier C))
by A22, TARSKI:def 4;
x2 in union (rng (Carrier C))
by A23, A24, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A21, A25, ZFMISC_1:106;
verum
end;
then reconsider TR = Union (pcs-ToleranceRels C) as Relation of (Union (Carrier C)) ;
take
pcs-Str(# (Union (Carrier C)),IR,TR #)
; ( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) )
thus
( the carrier of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (Carrier C) & the InternalRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-InternalRels C) & the ToleranceRel of pcs-Str(# (Union (Carrier C)),IR,TR #) = Union (pcs-ToleranceRels C) )
; verum