reconsider R = id ( the carrier of S, the Sorts of A) as ManySortedRelation of A ;
take
R
; ( R is invariant & R is stable & R is MSEquivalence-like )
thus
R is invariant
( R is stable & R is MSEquivalence-like )proof
let s1,
s2 be
SortSymbol of
S;
MSUALG_6:def 8 for t being Function st t is_e.translation_of A,s1,s2 holds
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2let t be
Function;
( t is_e.translation_of A,s1,s2 implies for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2 )
assume
t is_e.translation_of A,
s1,
s2
;
for a, b being set st [a,b] in R . s1 holds
[(t . a),(t . b)] in R . s2
then reconsider f =
t as
Function of
( the Sorts of A . s1),
( the Sorts of A . s2) by Th11;
let a,
b be
set ;
( [a,b] in R . s1 implies [(t . a),(t . b)] in R . s2 )
assume A1:
[a,b] in R . s1
;
[(t . a),(t . b)] in R . s2
then
a in the
Sorts of
A . s1
by ZFMISC_1:87;
then A2:
f . a in the
Sorts of
A . s2
by FUNCT_2:5;
R . s1 = id ( the Sorts of A . s1)
by Def10;
then A3:
a = b
by A1, RELAT_1:def 10;
R . s2 = id ( the Sorts of A . s2)
by Def10;
hence
[(t . a),(t . b)] in R . s2
by A3, A2, RELAT_1:def 10;
verum
end;
thus
R is stable
R is MSEquivalence-like proof
let h be
Endomorphism of
A;
MSUALG_6:def 9 for s being SortSymbol of S
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . slet s be
SortSymbol of
S;
for a, b being set st [a,b] in R . s holds
[((h . s) . a),((h . s) . b)] in R . slet a,
b be
set ;
( [a,b] in R . s implies [((h . s) . a),((h . s) . b)] in R . s )
A4:
R . s = id ( the Sorts of A . s)
by Def10;
assume A5:
[a,b] in R . s
;
[((h . s) . a),((h . s) . b)] in R . s
then
a in the
Sorts of
A . s
by A4, RELAT_1:def 10;
then A6:
(h . s) . a in the
Sorts of
A . s
by FUNCT_2:5;
a = b
by A4, A5, RELAT_1:def 10;
hence
[((h . s) . a),((h . s) . b)] in R . s
by A4, A6, RELAT_1:def 10;
verum
end;
let i be set ; MSUALG_4:def 2,MSUALG_4:def 3 for b1 being Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] holds
( not i in the carrier of S or not R . i = b1 or b1 is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
let P be Relation of ( the Sorts of A . i); ( not i in the carrier of S or not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
assume
i in the carrier of S
; ( not R . i = P or P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):] )
then reconsider s = i as SortSymbol of S ;
assume
R . i = P
; P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
then
P = id ( the Sorts of A . s)
by Def10;
hence
P is Element of bool [:( the Sorts of A . i),( the Sorts of A . i):]
; verum