let A be partial non-empty UAStr ; :: thesis: for P being a_partition of A st P = Class (LimDomRel A) holds
for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign A,P is_rougher_than S
let P be a_partition of A; :: thesis: ( P = Class (LimDomRel A) implies for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign A,P is_rougher_than S )
assume A1:
P = Class (LimDomRel A)
; :: thesis: for S being non empty non void ManySortedSign st A can_be_characterized_by S holds
MSSign A,P is_rougher_than S
set S1 = MSSign A,P;
let S2 be non empty non void ManySortedSign ; :: thesis: ( A can_be_characterized_by S2 implies MSSign A,P is_rougher_than S2 )
given G being MSAlgebra of S2, Q being IndexedPartition of the carrier' of S2 such that A2:
A can_be_characterized_by S2,G,Q
; :: according to PUA2MSS1:def 17 :: thesis: MSSign A,P is_rougher_than S2
A3:
( the Sorts of G is IndexedPartition of A & dom Q = dom the charact of A )
by A2, Def16;
then reconsider G = G as non-empty MSAlgebra of S2 by MSUALG_1:def 8;
reconsider R = the Sorts of G as IndexedPartition of A by A2, Def16;
A4:
dom R = the carrier of S2
by PARTFUN1:def 4;
then reconsider SG = the Sorts of G as Function of the carrier of S2,(rng R) by RELSET_1:11;
A5:
the carrier' of (MSSign A,P) = { [o,p] where o is OperSymbol of A, p is Element of P * : product p meets dom (Den o,A) }
by Def15;
A6:
the carrier of (MSSign A,P) = P
by Def15;
defpred S1[ set , set ] means $1 c= $2;
A7:
rng R is_finer_than P
by A1, Th28;
then A8:
for r being set st r in rng R holds
ex p being set st
( p in P & S1[r,p] )
by SETFAM_1:def 2;
consider em being Function such that
A9:
( dom em = rng R & rng em c= P )
and
A10:
for r being set st r in rng R holds
S1[r,em . r]
from WELLORD2:sch 1(A8);
reconsider em = em as Function of (rng R),P by A9, FUNCT_2:4;
( dom (em * R) = dom R & rng (em * R) = rng em )
by A9, RELAT_1:46, RELAT_1:47;
then reconsider f = em * R as Function of the carrier of S2,the carrier of (MSSign A,P) by A4, A6, FUNCT_2:4;
take
f
; :: according to PUA2MSS1:def 14 :: thesis: ex g being Function st
( f,g form_morphism_between S2, MSSign A,P & rng f = the carrier of (MSSign A,P) & rng g = the carrier' of (MSSign A,P) )
defpred S2[ set , set ] means ex p being FinSequence of P ex o being OperSymbol of S2 st
( $2 = [(Q -index_of $1),p] & $1 = o & Args o,G c= product p );
A11:
for s2 being set st s2 in the carrier' of S2 holds
ex s1 being set st
( s1 in the carrier' of (MSSign A,P) & S2[s2,s1] )
proof
let s2 be
set ;
:: thesis: ( s2 in the carrier' of S2 implies ex s1 being set st
( s1 in the carrier' of (MSSign A,P) & S2[s2,s1] ) )
assume
s2 in the
carrier' of
S2
;
:: thesis: ex s1 being set st
( s1 in the carrier' of (MSSign A,P) & S2[s2,s1] )
then reconsider s2 =
s2 as
OperSymbol of
S2 ;
SG * (the_arity_of s2) is
FinSequence of
rng R
by Lm2;
then consider p being
FinSequence of
P such that A12:
product (SG * (the_arity_of s2)) c= product p
by A7, Th4;
reconsider p =
p as
Element of
P * by FINSEQ_1:def 11;
take s1 =
[(Q -index_of s2),p];
:: thesis: ( s1 in the carrier' of (MSSign A,P) & S2[s2,s1] )
reconsider o =
Q -index_of s2 as
OperSymbol of
A by A3, Def4;
consider aa being
Element of
Args s2,
G;
A13:
aa in Args s2,
G
;
A14:
dom (Den s2,G) = Args s2,
G
by FUNCT_2:def 1;
A15:
(
dom the
Arity of
S2 = the
carrier' of
S2 &
dom the
Charact of
G = the
carrier' of
S2 )
by PARTFUN1:def 4;
the
Charact of
G | (Q . o) is
IndexedPartition of
Den o,
A
by A2, Def16;
then
rng (the Charact of G | (Q . o)) is
a_partition of
Den o,
A
by Def3;
then
( the
Charact of
G .: (Q . o) is
a_partition of
Den o,
A &
s2 in Q . o )
by Def4, RELAT_1:148;
then
(
Den s2,
G = the
Charact of
G . s2 & the
Charact of
G . s2 in the
Charact of
G .: (Q . o) & the
Charact of
G .: (Q . o) c= bool (Den o,A) )
by A15, FUNCT_1:def 12;
then A16:
dom (Den s2,G) c= dom (Den o,A)
by RELAT_1:25;
A17:
Args s2,
G =
(the Sorts of G # ) . (the Arity of S2 . s2)
by A15, FUNCT_1:23
.=
product (SG * (the_arity_of s2))
by PBOOLE:def 19
;
then
product p meets dom (Den o,A)
by A12, A13, A14, A16, XBOOLE_0:3;
hence
s1 in the
carrier' of
(MSSign A,P)
by A5;
:: thesis: S2[s2,s1]
take
p
;
:: thesis: ex o being OperSymbol of S2 st
( s1 = [(Q -index_of s2),p] & s2 = o & Args o,G c= product p )
take
s2
;
:: thesis: ( s1 = [(Q -index_of s2),p] & s2 = s2 & Args s2,G c= product p )
thus
(
s1 = [(Q -index_of s2),p] &
s2 = s2 &
Args s2,
G c= product p )
by A12, A17;
:: thesis: verum
end;
consider g being Function such that
A18:
( dom g = the carrier' of S2 & rng g c= the carrier' of (MSSign A,P) & ( for s being set st s in the carrier' of S2 holds
S2[s,g . s] ) )
from WELLORD2:sch 1(A11);
reconsider g = g as Function of the carrier' of S2,the carrier' of (MSSign A,P) by A18, FUNCT_2:4;
take
g
; :: thesis: ( f,g form_morphism_between S2, MSSign A,P & rng f = the carrier of (MSSign A,P) & rng g = the carrier' of (MSSign A,P) )
thus A19:
( dom f = the carrier of S2 & dom g = the carrier' of S2 & rng f c= the carrier of (MSSign A,P) & rng g c= the carrier' of (MSSign A,P) )
by FUNCT_2:def 1; :: according to PUA2MSS1:def 13 :: thesis: ( f * the ResultSort of S2 = the ResultSort of (MSSign A,P) * g & ( for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign A,P) . (g . o) ) & rng f = the carrier of (MSSign A,P) & rng g = the carrier' of (MSSign A,P) )
now let c be
OperSymbol of
S2;
:: thesis: (f * the ResultSort of S2) . c = (the ResultSort of (MSSign A,P) * g) . cset s = the
ResultSort of
S2 . c;
A20:
(
R . (the ResultSort of S2 . c) = (the Sorts of G * the ResultSort of S2) . c &
(f * the ResultSort of S2) . c = f . (the ResultSort of S2 . c) )
by FUNCT_2:21;
R . (the ResultSort of S2 . c) in rng R
by A4, FUNCT_1:def 5;
then
R . (the ResultSort of S2 . c) c= em . (R . (the ResultSort of S2 . c))
by A10;
then A21:
R . (the ResultSort of S2 . c) c= f . (the ResultSort of S2 . c)
by A4, FUNCT_1:23;
consider p being
FinSequence of
P,
o being
OperSymbol of
S2 such that A22:
(
g . c = [(Q -index_of c),p] &
c = o &
Args o,
G c= product p )
by A18;
reconsider p =
p as
Element of
P * by FINSEQ_1:def 11;
reconsider s2 =
Q -index_of c as
OperSymbol of
A by A3, Def4;
consider aa being
Element of
Args o,
G;
the
Charact of
G | (Q . s2) is
IndexedPartition of
Den s2,
A
by A2, Def16;
then
rng (the Charact of G | (Q . s2)) is
a_partition of
Den s2,
A
by Def3;
then
(
o in Q . s2 &
dom the
Charact of
G = the
carrier' of
S2 & the
Charact of
G .: (Q . s2) is
a_partition of
Den s2,
A )
by A22, Def4, PARTFUN1:def 4, RELAT_1:148;
then A23:
(
Den o,
G = the
Charact of
G . o & the
Charact of
G . o in the
Charact of
G .: (Q . s2) & the
Charact of
G .: (Q . s2) c= bool (Den s2,A) )
by FUNCT_1:def 12;
then A24:
(
dom (Den o,G) = Args o,
G &
dom (Den o,G) c= dom (Den s2,A) &
aa in Args o,
G )
by FUNCT_2:def 1, RELAT_1:25;
then
product p meets dom (Den s2,A)
by A22, XBOOLE_0:3;
then A25:
(Den s2,A) .: (product p) c= the
ResultSort of
(MSSign A,P) . (g . c)
by A22, Def15;
rng (Den c,G) = (Den c,G) .: (Args c,G)
by A22, A24, RELAT_1:146;
then
(
rng (Den c,G) c= (Den c,G) .: (product p) &
(Den c,G) .: (product p) c= (Den s2,A) .: (product p) )
by A22, A23, RELAT_1:156, RELAT_1:157;
then
rng (Den c,G) c= (Den s2,A) .: (product p)
by XBOOLE_1:1;
then
(
rng (Den c,G) c= the
ResultSort of
(MSSign A,P) . (g . c) &
(Den c,G) . aa in rng (Den c,G) )
by A22, A24, A25, FUNCT_1:def 5, XBOOLE_1:1;
then
(
(Den c,G) . aa in (the Sorts of G * the ResultSort of S2) . c &
(Den c,G) . aa in the
ResultSort of
(MSSign A,P) . (g . c) )
;
then
(
(f * the ResultSort of S2) . c in P &
(the ResultSort of (MSSign A,P) * g) . c in P &
(Den c,G) . aa in (f * the ResultSort of S2) . c &
(Den c,G) . aa in (the ResultSort of (MSSign A,P) * g) . c )
by A6, A20, A21, FUNCT_2:21;
hence
(f * the ResultSort of S2) . c = (the ResultSort of (MSSign A,P) * g) . c
by Th3;
:: thesis: verum end;
hence
f * the ResultSort of S2 = the ResultSort of (MSSign A,P) * g
by FUNCT_2:113; :: thesis: ( ( for o being set
for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign A,P) . (g . o) ) & rng f = the carrier of (MSSign A,P) & rng g = the carrier' of (MSSign A,P) )
hereby :: thesis: ( rng f = the carrier of (MSSign A,P) & rng g = the carrier' of (MSSign A,P) )
let o be
set ;
:: thesis: for p being Function st o in the carrier' of S2 & p = the Arity of S2 . o holds
f * p = the Arity of (MSSign A,P) . (g . o)let p be
Function;
:: thesis: ( o in the carrier' of S2 & p = the Arity of S2 . o implies f * p = the Arity of (MSSign A,P) . (g . o) )assume
o in the
carrier' of
S2
;
:: thesis: ( p = the Arity of S2 . o implies f * p = the Arity of (MSSign A,P) . (g . o) )then reconsider s =
o as
OperSymbol of
S2 ;
assume A26:
p = the
Arity of
S2 . o
;
:: thesis: f * p = the Arity of (MSSign A,P) . (g . o)reconsider q = the
Arity of
S2 . s as
Element of the
carrier of
S2 * ;
reconsider r =
SG * q as
FinSequence of
rng R by Lm2;
consider p' being
FinSequence of
P,
o' being
OperSymbol of
S2 such that A27:
(
g . s = [(Q -index_of s),p'] &
s = o' &
Args o',
G c= product p' )
by A18;
g . s in the
carrier' of
(MSSign A,P)
;
then consider o1 being
OperSymbol of
A,
p1 being
Element of
P * such that A28:
(
g . s = [o1,p1] &
product p1 meets dom (Den o1,A) )
by A5;
(
p' = p1 &
Q -index_of s = o1 )
by A27, A28, ZFMISC_1:33;
then A29:
the
Arity of
(MSSign A,P) . (g . o) = p'
by A28, Def15;
Args o',
G =
(the Sorts of G # ) . q
by A27, FUNCT_2:21
.=
product r
by PBOOLE:def 19
;
then
em * r = p'
by A10, A27, Th5;
hence
f * p = the
Arity of
(MSSign A,P) . (g . o)
by A26, A29, RELAT_1:55;
:: thesis: verum
end;
thus
rng f c= the carrier of (MSSign A,P)
; :: according to XBOOLE_0:def 10 :: thesis: ( the carrier of (MSSign A,P) c= rng f & rng g = the carrier' of (MSSign A,P) )
thus
the carrier of (MSSign A,P) c= rng f
:: thesis: rng g = the carrier' of (MSSign A,P)
thus
rng g c= the carrier' of (MSSign A,P)
; :: according to XBOOLE_0:def 10 :: thesis: the carrier' of (MSSign A,P) c= rng g
thus
the carrier' of (MSSign A,P) c= rng g
:: thesis: verumproof
let s1 be
set ;
:: according to TARSKI:def 3 :: thesis: ( not s1 in the carrier' of (MSSign A,P) or s1 in rng g )
assume
s1 in the
carrier' of
(MSSign A,P)
;
:: thesis: s1 in rng g
then consider o being
OperSymbol of
A,
p being
Element of
P * such that A31:
(
s1 = [o,p] &
product p meets dom (Den o,A) )
by A5;
consider a being
set such that A32:
(
a in product p &
a in dom (Den o,A) )
by A31, XBOOLE_0:3;
consider h being
Function such that A33:
(
a = h &
dom h = dom p & ( for
x being
set st
x in dom p holds
h . x in p . x ) )
by A32, CARD_3:def 5;
reconsider h =
h as
FinSequence by A33, Lm1;
product p c= Funcs (dom p),
(Union p)
by FUNCT_6:10;
then
(
rng p c= P & ex
f being
Function st
(
h = f &
dom f = dom p &
rng f c= Union p ) )
by A32, A33, FUNCT_2:def 2;
then
(
rng h c= Union p &
Union p = union (rng p) &
union (rng p) c= union P &
union P = the
carrier of
A )
by CARD_3:def 4, EQREL_1:def 6, ZFMISC_1:95;
then
rng h c= the
carrier of
A
by XBOOLE_1:1;
then
h is
FinSequence of the
carrier of
A
by FINSEQ_1:def 4;
then consider r being
FinSequence of
rng R such that A34:
h in product r
by Th7;
A35:
(
dom h = dom r &
rng r c= rng R &
rng p c= P )
by A34, CARD_3:18;
A36:
Den o,
A is_exactly_partitable_wrt P
by Def11;
then A39:
(
product r c= product p &
product p c= dom (Den o,A) )
by A31, A33, A35, A36, Def10, CARD_3:38;
then
product r c= dom (Den o,A)
by XBOOLE_1:1;
then consider s2 being
OperSymbol of
S2 such that A40:
( the
Sorts of
G * (the_arity_of s2) = r &
s2 in Q . o )
by A2, Th33;
consider p' being
FinSequence of
P,
o' being
OperSymbol of
S2 such that A41:
(
g . s2 = [(Q -index_of s2),p'] &
s2 = o' &
Args o',
G c= product p' )
by A18;
dom the
Arity of
S2 = the
carrier' of
S2
by FUNCT_2:def 1;
then Args s2,
G =
(the Sorts of G # ) . (the Arity of S2 . s2)
by FUNCT_1:23
.=
product r
by A40, PBOOLE:def 19
;
then
(
p' = em * r &
p = em * r &
Q -index_of s2 = o )
by A3, A10, A39, A40, A41, Def4, Th5;
hence
s1 in rng g
by A18, A31, A41, FUNCT_1:def 5;
:: thesis: verum
end;