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 ;
:: according to TARSKI:def 3 :: thesis: ( not x in Union (pcs-InternalRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-InternalRels C)
;
:: thesis: 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 &
(pcs-InternalRels C) . i = the
InternalRel of
R )
by A4, Def5;
consider x1,
x2 being
set such that A8:
x = [x1,x2]
and A9:
(
x1 in the
carrier of
R &
x2 in the
carrier of
R )
by A2, A5, A7, 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
the
carrier of
R in rng (Carrier C)
by A1, A4, A6, A7, FUNCT_1:def 5;
then
(
x1 in union (rng (Carrier C)) &
x2 in union (rng (Carrier C)) )
by A9, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A8, ZFMISC_1:106;
:: thesis: 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 ;
:: according to TARSKI:def 3 :: thesis: ( not x in Union (pcs-ToleranceRels C) or x in [:(Union (Carrier C)),(Union (Carrier C)):] )
assume
x in Union (pcs-ToleranceRels C)
;
:: thesis: x in [:(Union (Carrier C)),(Union (Carrier C)):]
then consider P being
set such that A10:
x in P
and A11:
P in rng (pcs-ToleranceRels C)
by TARSKI:def 4;
consider i being
set such that A12:
i in dom (pcs-ToleranceRels C)
and A13:
(pcs-ToleranceRels C) . i = P
by A11, FUNCT_1:def 5;
A14:
dom (pcs-ToleranceRels C) = I
by PARTFUN1:def 4;
then consider R being
TolStr such that A15:
(
R = C . i &
(pcs-ToleranceRels C) . i = the
ToleranceRel of
R )
by A12, Def19;
consider x1,
x2 being
set such that A16:
x = [x1,x2]
and A17:
(
x1 in the
carrier of
R &
x2 in the
carrier of
R )
by A10, A13, A15, RELSET_1:6;
ex
S being
1-sorted st
(
S = C . i &
(Carrier C) . i = the
carrier of
S )
by A12, A14, PRALG_1:def 13;
then
the
carrier of
R in rng (Carrier C)
by A1, A12, A14, A15, FUNCT_1:def 5;
then
(
x1 in union (rng (Carrier C)) &
x2 in union (rng (Carrier C)) )
by A17, TARSKI:def 4;
hence
x in [:(Union (Carrier C)),(Union (Carrier C)):]
by A16, ZFMISC_1:106;
:: thesis: verum
end;
then reconsider TR = Union (pcs-ToleranceRels C) as Relation of (Union (Carrier C)) ;
take
pcs-Str(# (Union (Carrier C)),IR,TR #)
; :: thesis: ( 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) )
; :: thesis: verum