:: CLOSURE3 semantic presentation
begin
registration
let S be non empty 1-sorted ;
cluster 1-sorted(# the carrier of S #) -> non empty ;
coherence
not 1-sorted(# the carrier of S #) is empty ;
end;
theorem Th1: :: CLOSURE3:1
for I being non empty set
for M, N being ManySortedSet of I holds M +* N = N
proof
let I be non empty set ; ::_thesis: for M, N being ManySortedSet of I holds M +* N = N
let M, N be ManySortedSet of I; ::_thesis: M +* N = N
dom M = I by PARTFUN1:def_2
.= dom N by PARTFUN1:def_2 ;
hence M +* N = N by FUNCT_4:19; ::_thesis: verum
end;
theorem :: CLOSURE3:2
for I being set
for M, N being ManySortedSet of I
for F being SubsetFamily of M st N in F holds
meet |:F:| c=' N by CLOSURE2:21, MSSUBFAM:43;
theorem Th3: :: CLOSURE3:3
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
proof
let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S
for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let MA be strict non-empty MSAlgebra over S; ::_thesis: for F being SubsetFamily of the Sorts of MA st F c= SubSort MA holds
for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SubSort MA implies for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed )
assume A1: F c= SubSort MA ; ::_thesis: for B being MSSubset of MA st B = meet |:F:| holds
B is opers_closed
let B be MSSubset of MA; ::_thesis: ( B = meet |:F:| implies B is opers_closed )
assume A2: B = meet |:F:| ; ::_thesis: B is opers_closed
percases ( F = {} or F <> {} ) ;
supposeA3: F = {} ; ::_thesis: B is opers_closed
set Q = the Sorts of MA;
reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA ;
set I = the carrier of S;
FF = [[0]] the carrier of S by A3, CLOSURE2:def_3;
then A4: the Sorts of MA = B by A2, MSSUBFAM:41;
reconsider Q = the Sorts of MA as MSSubset of MA by PBOOLE:def_18;
for o being OperSymbol of S holds Q is_closed_on o
proof
let o be OperSymbol of S; ::_thesis: Q is_closed_on o
A5: ( the ResultSort of S . o = the_result_sort_of o & dom the ResultSort of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_2;
Result (o,MA) = (Q * the ResultSort of S) . o by MSUALG_1:def_5
.= Q . (the_result_sort_of o) by A5, FUNCT_1:13 ;
then A6: rng ((Den (o,MA)) | ((Q #) . (the_arity_of o))) c= Q . (the_result_sort_of o) by RELAT_1:def_19;
( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1;
then A7: ((Q #) * the Arity of S) . o = (Q #) . (the_arity_of o) by FUNCT_1:13;
(Q * the ResultSort of S) . o = Q . (the_result_sort_of o) by A5, FUNCT_1:13;
hence Q is_closed_on o by A7, A6, MSUALG_2:def_5; ::_thesis: verum
end;
hence B is opers_closed by A4, MSUALG_2:def_6; ::_thesis: verum
end;
supposeA8: F <> {} ; ::_thesis: B is opers_closed
set SS = S;
let o be OperSymbol of S; :: according to MSUALG_2:def_6 ::_thesis: B is_closed_on o
set i = the_result_sort_of o;
A9: the ResultSort of S . o = the_result_sort_of o by MSUALG_1:def_2;
A10: dom the ResultSort of S = the carrier' of S by FUNCT_2:def_1;
( the Arity of S . o = the_arity_of o & dom the Arity of S = the carrier' of S ) by FUNCT_2:def_1, MSUALG_1:def_1;
then A11: ((B #) * the Arity of S) . o = (B #) . (the_arity_of o) by FUNCT_1:13;
Result (o,MA) = ( the Sorts of MA * the ResultSort of S) . o by MSUALG_1:def_5
.= the Sorts of MA . (the_result_sort_of o) by A9, A10, FUNCT_1:13 ;
then A12: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= the Sorts of MA . (the_result_sort_of o) by RELAT_1:def_19;
A13: rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) c= B . (the_result_sort_of o)
proof
consider Q being Subset-Family of ( the Sorts of MA . (the_result_sort_of o)) such that
A14: Q = |:F:| . (the_result_sort_of o) and
A15: B . (the_result_sort_of o) = Intersect Q by A2, MSSUBFAM:def_1;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) or v in B . (the_result_sort_of o) )
assume A16: v in rng ((Den (o,MA)) | ((B #) . (the_arity_of o))) ; ::_thesis: v in B . (the_result_sort_of o)
then consider p being set such that
A17: p in dom ((Den (o,MA)) | ((B #) . (the_arity_of o))) and
A18: v = ((Den (o,MA)) | ((B #) . (the_arity_of o))) . p by FUNCT_1:def_3;
for Y being set st Y in Q holds
v in Y
proof
A19: |:F:| . (the_result_sort_of o) = { (xx . (the_result_sort_of o)) where xx is Element of Bool the Sorts of MA : xx in F } by A8, CLOSURE2:14;
let Y be set ; ::_thesis: ( Y in Q implies v in Y )
assume Y in Q ; ::_thesis: v in Y
then consider xx being Element of Bool the Sorts of MA such that
A20: Y = xx . (the_result_sort_of o) and
A21: xx in F by A14, A19;
reconsider xx = xx as MSSubset of MA ;
xx is opers_closed by A1, A21, MSUALG_2:14;
then xx is_closed_on o by MSUALG_2:def_6;
then A22: rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) c= (xx * the ResultSort of S) . o by MSUALG_2:def_5;
B c= xx by A2, A21, CLOSURE2:21, MSSUBFAM:43;
then (Den (o,MA)) | (((B #) * the Arity of S) . o) c= (Den (o,MA)) | (((xx #) * the Arity of S) . o) by MSUALG_2:2, RELAT_1:75;
then A23: dom ((Den (o,MA)) | (((B #) * the Arity of S) . o)) c= dom ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by RELAT_1:11;
A24: v = (Den (o,MA)) . p by A17, A18, FUNCT_1:47;
then v = ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) . p by A11, A17, A23, FUNCT_1:47;
then v in rng ((Den (o,MA)) | (((xx #) * the Arity of S) . o)) by A11, A17, A23, FUNCT_1:def_3;
then (Den (o,MA)) . p in (xx * the ResultSort of S) . o by A22, A24;
then (Den (o,MA)) . p in xx . ( the ResultSort of S . o) by A10, FUNCT_1:13;
then (Den (o,MA)) . p in xx . (the_result_sort_of o) by MSUALG_1:def_2;
hence v in Y by A17, A18, A20, FUNCT_1:47; ::_thesis: verum
end;
hence v in B . (the_result_sort_of o) by A12, A16, A15, SETFAM_1:43; ::_thesis: verum
end;
(B * the ResultSort of S) . o = B . (the_result_sort_of o) by A9, A10, FUNCT_1:13;
hence B is_closed_on o by A11, A13, MSUALG_2:def_5; ::_thesis: verum
end;
end;
end;
begin
theorem :: CLOSURE3:4
for A, B, C being set st A is_coarser_than B & B is_coarser_than C holds
A is_coarser_than C
proof
let A, B, C be set ; ::_thesis: ( A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C )
assume that
A1: A is_coarser_than B and
A2: B is_coarser_than C ; ::_thesis: A is_coarser_than C
let a be set ; :: according to SETFAM_1:def_3 ::_thesis: ( not a in A or ex b1 being set st
( b1 in C & b1 c= a ) )
assume a in A ; ::_thesis: ex b1 being set st
( b1 in C & b1 c= a )
then consider b being set such that
A3: b in B and
A4: b c= a by A1, SETFAM_1:def_3;
consider c being set such that
A5: ( c in C & c c= b ) by A2, A3, SETFAM_1:def_3;
take c ; ::_thesis: ( c in C & c c= a )
thus ( c in C & c c= a ) by A4, A5, XBOOLE_1:1; ::_thesis: verum
end;
LM: now__::_thesis:_for_I_being_non_empty_set_
for_M_being_ManySortedSet_of_I_holds_support_M_=__{__x_where_x_is_Element_of_I_:_M_._x_<>_{}__}_
let I be non empty set ; ::_thesis: for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} }
let M be ManySortedSet of I; ::_thesis: support M = { x where x is Element of I : M . x <> {} }
set F = { x where x is Element of I : M . x <> {} } ;
thus support M = { x where x is Element of I : M . x <> {} } ::_thesis: verum
proof
thus support M c= { x where x is Element of I : M . x <> {} } :: according to XBOOLE_0:def_10 ::_thesis: { x where x is Element of I : M . x <> {} } c= support M
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in support M or x in { x where x is Element of I : M . x <> {} } )
A1: dom M = I by PARTFUN1:def_2;
A2: support M c= dom M by PRE_POLY:37;
assume A3: x in support M ; ::_thesis: x in { x where x is Element of I : M . x <> {} }
then M . x <> {} by PRE_POLY:def_7;
hence x in { x where x is Element of I : M . x <> {} } by A1, A2, A3; ::_thesis: verum
end;
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in { x where x is Element of I : M . x <> {} } or x in support M )
assume x in { x where x is Element of I : M . x <> {} } ; ::_thesis: x in support M
then ex i being Element of I st
( x = i & M . i <> {} ) ;
hence x in support M by PRE_POLY:def_7; ::_thesis: verum
end;
end;
definition
let I be non empty set ;
let M be ManySortedSet of I;
:: original: support
redefine func support M -> set equals :: CLOSURE3:def 1
{ x where x is Element of I : M . x <> {} } ;
compatibility
for b1 being set holds
( b1 = support M iff b1 = { x where x is Element of I : M . x <> {} } ) by LM;
end;
:: deftheorem defines support CLOSURE3:def_1_:_
for I being non empty set
for M being ManySortedSet of I holds support M = { x where x is Element of I : M . x <> {} } ;
theorem :: CLOSURE3:5
for I being non empty set
for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M))
proof
let I be non empty set ; ::_thesis: for M being V8() ManySortedSet of I holds M = ([[0]] I) +* (M | (support M))
let M be V8() ManySortedSet of I; ::_thesis: M = ([[0]] I) +* (M | (support M))
set MM = M | (support M);
A1: I c= support M
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in I or v in support M )
assume A2: v in I ; ::_thesis: v in support M
then M . v <> {} ;
hence v in support M by A2; ::_thesis: verum
end;
dom M = I by PARTFUN1:def_2;
then M | (support M) = M by A1, RELAT_1:68;
hence M = ([[0]] I) +* (M | (support M)) by Th1; ::_thesis: verum
end;
theorem :: CLOSURE3:6
for I being non empty set
for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
proof
let I be non empty set ; ::_thesis: for M1, M2 being V8() ManySortedSet of I st M1 | (support M1) = M2 | (support M2) holds
M1 = M2
let M1, M2 be V8() ManySortedSet of I; ::_thesis: ( M1 | (support M1) = M2 | (support M2) implies M1 = M2 )
A1: dom M1 = I by PARTFUN1:def_2;
A2: dom M2 = I by PARTFUN1:def_2;
assume A3: M1 | (support M1) = M2 | (support M2) ; ::_thesis: M1 = M2
for x being set st x in I holds
M1 . x = M2 . x
proof
let x be set ; ::_thesis: ( x in I implies M1 . x = M2 . x )
A4: dom (M2 | (support M2)) = (dom M2) /\ (support M2) by RELAT_1:61;
assume A5: x in I ; ::_thesis: M1 . x = M2 . x
then not M1 . x is empty ;
then A6: x in support M1 by A5;
not M2 . x is empty by A5;
then x in support M2 by A5;
then A7: x in dom (M2 | (support M2)) by A2, A5, A4, XBOOLE_0:def_4;
dom (M1 | (support M1)) = (dom M1) /\ (support M1) by RELAT_1:61;
then x in dom (M1 | (support M1)) by A1, A5, A6, XBOOLE_0:def_4;
then M1 . x = (M2 | (support M2)) . x by A3, FUNCT_1:47
.= M2 . x by A7, FUNCT_1:47 ;
hence M1 . x = M2 . x ; ::_thesis: verum
end;
hence M1 = M2 by A1, A2, FUNCT_1:2; ::_thesis: verum
end;
theorem :: CLOSURE3:7
canceled;
theorem Th8: :: CLOSURE3:8
for I being non empty set
for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
proof
let I be non empty set ; ::_thesis: for M being ManySortedSet of I
for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let M be ManySortedSet of I; ::_thesis: for x being Element of Bool M
for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let x be Element of Bool M; ::_thesis: for i being Element of I
for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let i be Element of I; ::_thesis: for y being set st y in x . i holds
ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
let y be set ; ::_thesis: ( y in x . i implies ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x ) )
assume A1: y in x . i ; ::_thesis: ex a being Element of Bool M st
( y in a . i & a is V42() & support a is finite & a c= x )
set N = {i} --> {y};
set A = ([[0]] I) +* ({i} --> {y});
A2: dom ({i} --> {y}) = {i} by FUNCOP_1:13;
then A3: i in dom ({i} --> {y}) by TARSKI:def_1;
then A4: ({i} --> {y}) . i = {y} by A2, FUNCOP_1:7;
then A5: (([[0]] I) +* ({i} --> {y})) . i = {y} by A3, FUNCT_4:13;
A6: dom (([[0]] I) +* ({i} --> {y})) = (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1
.= I \/ {i} by A2, PARTFUN1:def_2
.= I by ZFMISC_1:40 ;
then reconsider A = ([[0]] I) +* ({i} --> {y}) as ManySortedSet of I by PARTFUN1:def_2, RELAT_1:def_18;
for j being set st j in I holds
A . j c= M . j
proof
let j be set ; ::_thesis: ( j in I implies A . j c= M . j )
assume A7: j in I ; ::_thesis: A . j c= M . j
percases ( i = j or i <> j ) ;
supposeA8: i = j ; ::_thesis: A . j c= M . j
reconsider x = x as ManySortedSubset of M ;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in A . j or v in M . j )
assume v in A . j ; ::_thesis: v in M . j
then v in {y} by A3, A4, A8, FUNCT_4:13;
then A9: v in x . j by A1, A8, TARSKI:def_1;
x c= M by PBOOLE:def_18;
then x . j c= M . j by A7, PBOOLE:def_2;
hence v in M . j by A9; ::_thesis: verum
end;
suppose i <> j ; ::_thesis: A . j c= M . j
then A10: not j in {i} by TARSKI:def_1;
j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A7, FUNCT_4:def_1;
then A . j = (I --> {}) . j by A2, A10, FUNCT_4:def_1
.= {} by A7, FUNCOP_1:7 ;
hence A . j c= M . j by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
then A c= M by PBOOLE:def_2;
then reconsider AA = A as ManySortedSubset of M by PBOOLE:def_18;
reconsider a = AA as Element of Bool M by CLOSURE2:def_1;
A11: for j being set st j in I holds
a . j c= x . j
proof
let j be set ; ::_thesis: ( j in I implies a . j c= x . j )
assume A12: j in I ; ::_thesis: a . j c= x . j
percases ( i = j or j <> i ) ;
supposeA13: i = j ; ::_thesis: a . j c= x . j
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in a . j or v in x . j )
assume A14: v in a . j ; ::_thesis: v in x . j
a . j = {y} by A3, A4, A13, FUNCT_4:13;
hence v in x . j by A1, A13, A14, TARSKI:def_1; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: a . j c= x . j
then A15: not j in {i} by TARSKI:def_1;
j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A12, FUNCT_4:def_1;
then a . j = (I --> {}) . j by A2, A15, FUNCT_4:def_1
.= {} by A12, FUNCOP_1:7 ;
hence a . j c= x . j by XBOOLE_1:2; ::_thesis: verum
end;
end;
end;
A16: { b where b is Element of I : a . b <> {} } = {i}
proof
thus { b where b is Element of I : a . b <> {} } c= {i} :: according to XBOOLE_0:def_10 ::_thesis: {i} c= { b where b is Element of I : a . b <> {} }
proof
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in { b where b is Element of I : a . b <> {} } or s in {i} )
assume s in { b where b is Element of I : a . b <> {} } ; ::_thesis: s in {i}
then A17: ex b being Element of I st
( s = b & a . b <> {} ) ;
assume A18: not s in {i} ; ::_thesis: contradiction
reconsider s = s as Element of I by A17;
s in dom a by A6;
then s in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by FUNCT_4:def_1;
then a . s = (I --> {}) . s by A2, A18, FUNCT_4:def_1
.= {} by FUNCOP_1:7 ;
hence contradiction by A17; ::_thesis: verum
end;
let s be set ; :: according to TARSKI:def_3 ::_thesis: ( not s in {i} or s in { b where b is Element of I : a . b <> {} } )
assume A19: s in {i} ; ::_thesis: s in { b where b is Element of I : a . b <> {} }
then A20: s = i by TARSKI:def_1;
reconsider s = s as Element of I by A19, TARSKI:def_1;
a . s = {y} by A3, A4, A20, FUNCT_4:13;
hence s in { b where b is Element of I : a . b <> {} } ; ::_thesis: verum
end;
take a ; ::_thesis: ( y in a . i & a is V42() & support a is finite & a c= x )
for j being set st j in I holds
a . j is finite
proof
let j be set ; ::_thesis: ( j in I implies a . j is finite )
assume A21: j in I ; ::_thesis: a . j is finite
percases ( j = i or j <> i ) ;
suppose j = i ; ::_thesis: a . j is finite
hence a . j is finite by A3, A4, FUNCT_4:13; ::_thesis: verum
end;
suppose j <> i ; ::_thesis: a . j is finite
then A22: not j in {i} by TARSKI:def_1;
j in (dom ([[0]] I)) \/ (dom ({i} --> {y})) by A6, A21, FUNCT_4:def_1;
then a . j = (I --> {}) . j by A2, A22, FUNCT_4:def_1
.= {} by A21, FUNCOP_1:7 ;
hence a . j is finite ; ::_thesis: verum
end;
end;
end;
hence ( y in a . i & a is V42() & support a is finite & a c= x ) by A5, A16, A11, FINSET_1:def_5, PBOOLE:def_2, TARSKI:def_1; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
let A be SubsetFamily of M;
func MSUnion A -> ManySortedSubset of M means :Def2: :: CLOSURE3:def 2
for i being set st i in I holds
it . i = union { (f . i) where f is Element of Bool M : f in A } ;
existence
ex b1 being ManySortedSubset of M st
for i being set st i in I holds
b1 . i = union { (f . i) where f is Element of Bool M : f in A }
proof
defpred S1[ set , set ] means $2 = union { (f . $1) where f is Element of Bool M : f in A } ;
A1: for x being set st x in I holds
ex y being set st S1[x,y] ;
consider IT being Function such that
A2: dom IT = I and
A3: for x being set st x in I holds
S1[x,IT . x] from CLASSES1:sch_1(A1);
reconsider IT = IT as ManySortedSet of I by A2, PARTFUN1:def_2, RELAT_1:def_18;
for i being set st i in I holds
IT . i c= M . i
proof
let i be set ; ::_thesis: ( i in I implies IT . i c= M . i )
assume A4: i in I ; ::_thesis: IT . i c= M . i
for x being set st x in IT . i holds
x in M . i
proof
let x be set ; ::_thesis: ( x in IT . i implies x in M . i )
assume A5: x in IT . i ; ::_thesis: x in M . i
IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3, A4;
then consider Y being set such that
A6: x in Y and
A7: Y in { (f . i) where f is Element of Bool M : f in A } by A5, TARSKI:def_4;
consider ff being Element of Bool M such that
A8: ff . i = Y and
ff in A by A7;
reconsider ff = ff as ManySortedSubset of M ;
ff c= M by PBOOLE:def_18;
then ff . i c= M . i by A4, PBOOLE:def_2;
hence x in M . i by A6, A8; ::_thesis: verum
end;
hence IT . i c= M . i by TARSKI:def_3; ::_thesis: verum
end;
then IT c= M by PBOOLE:def_2;
then reconsider IT = IT as ManySortedSubset of M by PBOOLE:def_18;
take IT ; ::_thesis: for i being set st i in I holds
IT . i = union { (f . i) where f is Element of Bool M : f in A }
thus for i being set st i in I holds
IT . i = union { (f . i) where f is Element of Bool M : f in A } by A3; ::_thesis: verum
end;
uniqueness
for b1, b2 being ManySortedSubset of M st ( for i being set st i in I holds
b1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds
b2 . i = union { (f . i) where f is Element of Bool M : f in A } ) holds
b1 = b2
proof
let B1, B2 be ManySortedSubset of M; ::_thesis: ( ( for i being set st i in I holds
B1 . i = union { (f . i) where f is Element of Bool M : f in A } ) & ( for i being set st i in I holds
B2 . i = union { (f . i) where f is Element of Bool M : f in A } ) implies B1 = B2 )
assume that
A9: for i being set st i in I holds
B1 . i = union { (f . i) where f is Element of Bool M : f in A } and
A10: for i being set st i in I holds
B2 . i = union { (ff . i) where ff is Element of Bool M : ff in A } ; ::_thesis: B1 = B2
for i being set st i in I holds
B1 . i = B2 . i
proof
let i be set ; ::_thesis: ( i in I implies B1 . i = B2 . i )
assume A11: i in I ; ::_thesis: B1 . i = B2 . i
then B1 . i = union { (f . i) where f is Element of Bool M : f in A } by A9
.= B2 . i by A10, A11 ;
hence B1 . i = B2 . i ; ::_thesis: verum
end;
hence B1 = B2 by PBOOLE:3; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines MSUnion CLOSURE3:def_2_:_
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M
for b4 being ManySortedSubset of M holds
( b4 = MSUnion A iff for i being set st i in I holds
b4 . i = union { (f . i) where f is Element of Bool M : f in A } );
registration
let I be set ;
let M be ManySortedSet of I;
let A be empty SubsetFamily of M;
cluster MSUnion A -> V9() ;
coherence
MSUnion A is empty-yielding
proof
let i be set ; :: according to PBOOLE:def_12 ::_thesis: ( not i in I or (MSUnion A) . i is empty )
set MA = MSUnion A;
assume i in I ; ::_thesis: (MSUnion A) . i is empty
then A1: (MSUnion A) . i = union { (f . i) where f is Element of Bool M : f in A } by Def2;
assume not (MSUnion A) . i is empty ; ::_thesis: contradiction
then consider v being set such that
A2: v in (MSUnion A) . i by XBOOLE_0:def_1;
consider h being set such that
v in h and
A3: h in { (f . i) where f is Element of Bool M : f in A } by A1, A2, TARSKI:def_4;
ex g being Element of Bool M st
( h = g . i & g in A ) by A3;
hence contradiction ; ::_thesis: verum
end;
end;
theorem :: CLOSURE3:9
for I being set
for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A being SubsetFamily of M holds MSUnion A = union |:A:|
let M be ManySortedSet of I; ::_thesis: for A being SubsetFamily of M holds MSUnion A = union |:A:|
let A be SubsetFamily of M; ::_thesis: MSUnion A = union |:A:|
set AA = |:A:|;
reconsider UA = union |:A:| as ManySortedSet of I ;
percases ( not A is empty or A is empty SubsetFamily of M ) ;
supposeA1: not A is empty ; ::_thesis: MSUnion A = union |:A:|
for i being set st i in I holds
(MSUnion A) . i = UA . i
proof
let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume A2: i in I ; ::_thesis: (MSUnion A) . i = UA . i
then ( |:A:| . i = { (g . i) where g is Element of Bool M : g in A } & UA . i = union (|:A:| . i) ) by A1, CLOSURE2:14, MBOOLEAN:def_2;
hence (MSUnion A) . i = UA . i by A2, Def2; ::_thesis: verum
end;
hence MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum
end;
supposeA3: A is empty SubsetFamily of M ; ::_thesis: MSUnion A = union |:A:|
for i being set st i in I holds
(MSUnion A) . i = UA . i
proof
let i be set ; ::_thesis: ( i in I implies (MSUnion A) . i = UA . i )
assume i in I ; ::_thesis: (MSUnion A) . i = UA . i
|:A:| = [[0]] I by A3, CLOSURE2:def_3;
then UA = [[0]] I by MBOOLEAN:21;
then UA . i is empty ;
hence (MSUnion A) . i = UA . i by A3; ::_thesis: verum
end;
hence MSUnion A = union |:A:| by PBOOLE:3; ::_thesis: verum
end;
end;
end;
definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: \/
redefine funcA \/ B -> SubsetFamily of M;
correctness
coherence
A \/ B is SubsetFamily of M;
by CLOSURE2:3;
end;
theorem :: CLOSURE3:10
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
let A, B be SubsetFamily of M; ::_thesis: MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B)
reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M ;
reconsider MAB = MAB as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
for i being set st i in I holds
MAB . i = (MA \/ MB) . i
proof
let i be set ; ::_thesis: ( i in I implies MAB . i = (MA \/ MB) . i )
assume A1: i in I ; ::_thesis: MAB . i = (MA \/ MB) . i
then A2: MAB . i = union { (f . i) where f is Element of Bool M : f in A \/ B } by Def2;
A3: (MA \/ MB) . i = (MA . i) \/ (MB . i) by A1, PBOOLE:def_4;
A4: for v being set st v in (MA \/ MB) . i holds
v in MAB . i
proof
let v be set ; ::_thesis: ( v in (MA \/ MB) . i implies v in MAB . i )
assume v in (MA \/ MB) . i ; ::_thesis: v in MAB . i
then A5: ( v in MA . i or v in MB . i ) by A3, XBOOLE_0:def_3;
percases ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A1, A5, Def2;
suppose v in union { (f . i) where f is Element of Bool M : f in A } ; ::_thesis: v in MAB . i
then consider g being set such that
A6: v in g and
A7: g in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def_4;
consider h being Element of Bool M such that
A8: g = h . i and
A9: h in A by A7;
h in A \/ B by A9, XBOOLE_0:def_3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A8;
hence v in MAB . i by A2, A6, TARSKI:def_4; ::_thesis: verum
end;
suppose v in union { (f . i) where f is Element of Bool M : f in B } ; ::_thesis: v in MAB . i
then consider g being set such that
A10: v in g and
A11: g in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def_4;
consider h being Element of Bool M such that
A12: g = h . i and
A13: h in B by A11;
h in A \/ B by A13, XBOOLE_0:def_3;
then g in { (f . i) where f is Element of Bool M : f in A \/ B } by A12;
hence v in MAB . i by A2, A10, TARSKI:def_4; ::_thesis: verum
end;
end;
end;
A14: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by A1, Def2;
for v being set st v in MAB . i holds
v in (MA \/ MB) . i
proof
let v be set ; ::_thesis: ( v in MAB . i implies v in (MA \/ MB) . i )
assume v in MAB . i ; ::_thesis: v in (MA \/ MB) . i
then consider h being set such that
A15: v in h and
A16: h in { (f . i) where f is Element of Bool M : f in A \/ B } by A2, TARSKI:def_4;
consider g being Element of Bool M such that
A17: h = g . i and
A18: g in A \/ B by A16;
( g in A or g in B ) by A18, XBOOLE_0:def_3;
then ( h in { (f . i) where f is Element of Bool M : f in A } or h in { (f . i) where f is Element of Bool M : f in B } ) by A17;
then ( v in union { (f . i) where f is Element of Bool M : f in A } or v in union { (f . i) where f is Element of Bool M : f in B } ) by A15, TARSKI:def_4;
hence v in (MA \/ MB) . i by A3, A14, XBOOLE_0:def_3; ::_thesis: verum
end;
hence MAB . i = (MA \/ MB) . i by A4, TARSKI:1; ::_thesis: verum
end;
hence MSUnion (A \/ B) = (MSUnion A) \/ (MSUnion B) by PBOOLE:3; ::_thesis: verum
end;
theorem :: CLOSURE3:11
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M st A c= B holds
MSUnion A c= MSUnion B
let A, B be SubsetFamily of M; ::_thesis: ( A c= B implies MSUnion A c= MSUnion B )
reconsider MA = MSUnion A as ManySortedSubset of M ;
reconsider MA = MA as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSubset of M ;
reconsider MB = MB as ManySortedSet of I ;
assume A1: A c= B ; ::_thesis: MSUnion A c= MSUnion B
for i being set st i in I holds
MA . i c= MB . i
proof
let i be set ; ::_thesis: ( i in I implies MA . i c= MB . i )
assume A2: i in I ; ::_thesis: MA . i c= MB . i
for v being set st v in MA . i holds
v in MB . i
proof
A3: MA . i = union { (f . i) where f is Element of Bool M : f in A } by A2, Def2;
let v be set ; ::_thesis: ( v in MA . i implies v in MB . i )
assume v in MA . i ; ::_thesis: v in MB . i
then consider h being set such that
A4: v in h and
A5: h in { (f . i) where f is Element of Bool M : f in A } by A3, TARSKI:def_4;
ex g being Element of Bool M st
( h = g . i & g in A ) by A5;
then h in { (k . i) where k is Element of Bool M : k in B } by A1;
then v in union { (k . i) where k is Element of Bool M : k in B } by A4, TARSKI:def_4;
hence v in MB . i by A2, Def2; ::_thesis: verum
end;
hence MA . i c= MB . i by TARSKI:def_3; ::_thesis: verum
end;
hence MSUnion A c= MSUnion B by PBOOLE:def_2; ::_thesis: verum
end;
definition
let I be set ;
let M be ManySortedSet of I;
let A, B be SubsetFamily of M;
:: original: /\
redefine funcA /\ B -> SubsetFamily of M;
correctness
coherence
A /\ B is SubsetFamily of M;
by CLOSURE2:4;
end;
theorem :: CLOSURE3:12
for I being set
for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let M be ManySortedSet of I; ::_thesis: for A, B being SubsetFamily of M holds MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
let A, B be SubsetFamily of M; ::_thesis: MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B)
reconsider MAB = MSUnion (A /\ B) as ManySortedSet of I ;
reconsider MA = MSUnion A as ManySortedSet of I ;
reconsider MB = MSUnion B as ManySortedSet of I ;
for i being set st i in I holds
MAB . i c= (MA /\ MB) . i
proof
let i be set ; ::_thesis: ( i in I implies MAB . i c= (MA /\ MB) . i )
assume A1: i in I ; ::_thesis: MAB . i c= (MA /\ MB) . i
then A2: ( MA . i = union { (f . i) where f is Element of Bool M : f in A } & MB . i = union { (f . i) where f is Element of Bool M : f in B } ) by Def2;
A3: MAB . i = union { (f . i) where f is Element of Bool M : f in A /\ B } by A1, Def2;
for v being set st v in MAB . i holds
v in (MA /\ MB) . i
proof
let v be set ; ::_thesis: ( v in MAB . i implies v in (MA /\ MB) . i )
assume v in MAB . i ; ::_thesis: v in (MA /\ MB) . i
then consider w being set such that
A4: v in w and
A5: w in { (f . i) where f is Element of Bool M : f in A /\ B } by A3, TARSKI:def_4;
consider g being Element of Bool M such that
A6: w = g . i and
A7: g in A /\ B by A5;
g in B by A7, XBOOLE_0:def_4;
then w in { (f . i) where f is Element of Bool M : f in B } by A6;
then A8: v in union { (f . i) where f is Element of Bool M : f in B } by A4, TARSKI:def_4;
g in A by A7, XBOOLE_0:def_4;
then w in { (f . i) where f is Element of Bool M : f in A } by A6;
then v in union { (f . i) where f is Element of Bool M : f in A } by A4, TARSKI:def_4;
then v in (MA . i) /\ (MB . i) by A2, A8, XBOOLE_0:def_4;
hence v in (MA /\ MB) . i by A1, PBOOLE:def_5; ::_thesis: verum
end;
hence MAB . i c= (MA /\ MB) . i by TARSKI:def_3; ::_thesis: verum
end;
hence MSUnion (A /\ B) c= (MSUnion A) /\ (MSUnion B) by PBOOLE:def_2; ::_thesis: verum
end;
theorem :: CLOSURE3:13
for I being set
for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A
proof
let I be set ; ::_thesis: for M being ManySortedSet of I
for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A
let M be ManySortedSet of I; ::_thesis: for AA being set st ( for x being set st x in AA holds
x is SubsetFamily of M ) holds
for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A
let AA be set ; ::_thesis: ( ( for x being set st x in AA holds
x is SubsetFamily of M ) implies for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A )
assume A1: for x being set st x in AA holds
x is SubsetFamily of M ; ::_thesis: for A, B being SubsetFamily of M st B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA holds
MSUnion B = MSUnion A
let A, B be SubsetFamily of M; ::_thesis: ( B = { (MSUnion X) where X is SubsetFamily of M : X in AA } & A = union AA implies MSUnion B = MSUnion A )
assume that
A2: B = { (MSUnion X) where X is SubsetFamily of M : X in AA } and
A3: A = union AA ; ::_thesis: MSUnion B = MSUnion A
let i be set ; :: according to PBOOLE:def_10 ::_thesis: ( not i in I or (MSUnion B) . i = (MSUnion A) . i )
assume A4: i in I ; ::_thesis: (MSUnion B) . i = (MSUnion A) . i
thus (MSUnion B) . i c= (MSUnion A) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSUnion A) . i c= (MSUnion B) . i
proof
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion B) . i or a in (MSUnion A) . i )
thus ( a in (MSUnion B) . i implies a in (MSUnion A) . i ) ::_thesis: verum
proof
assume a in (MSUnion B) . i ; ::_thesis: a in (MSUnion A) . i
then a in union { (f . i) where f is Element of Bool M : f in B } by A4, Def2;
then consider Y being set such that
A5: a in Y and
A6: Y in { (f . i) where f is Element of Bool M : f in B } by TARSKI:def_4;
consider f being Element of Bool M such that
A7: f . i = Y and
A8: f in B by A6;
consider Q being SubsetFamily of M such that
A9: f = MSUnion Q and
A10: Q in AA by A2, A8;
(MSUnion Q) . i = union { (g . i) where g is Element of Bool M : g in Q } by A4, Def2;
then consider d being set such that
A11: a in d and
A12: d in { (g . i) where g is Element of Bool M : g in Q } by A5, A7, A9, TARSKI:def_4;
consider g being Element of Bool M such that
A13: d = g . i and
A14: g in Q by A12;
g in union AA by A10, A14, TARSKI:def_4;
then d in { (h . i) where h is Element of Bool M : h in union AA } by A13;
then a in union { (h . i) where h is Element of Bool M : h in union AA } by A11, TARSKI:def_4;
hence a in (MSUnion A) . i by A3, A4, Def2; ::_thesis: verum
end;
end;
let a be set ; :: according to TARSKI:def_3 ::_thesis: ( not a in (MSUnion A) . i or a in (MSUnion B) . i )
assume a in (MSUnion A) . i ; ::_thesis: a in (MSUnion B) . i
then a in union { (f . i) where f is Element of Bool M : f in A } by A4, Def2;
then consider Y being set such that
A15: a in Y and
A16: Y in { (f . i) where f is Element of Bool M : f in A } by TARSKI:def_4;
consider f being Element of Bool M such that
A17: f . i = Y and
A18: f in A by A16;
consider c being set such that
A19: f in c and
A20: c in AA by A3, A18, TARSKI:def_4;
reconsider c = c as SubsetFamily of M by A1, A20;
f . i in { (v . i) where v is Element of Bool M : v in c } by A19;
then A21: a in union { (v . i) where v is Element of Bool M : v in c } by A15, A17, TARSKI:def_4;
(MSUnion c) . i = union { (v . i) where v is Element of Bool M : v in c } by A4, Def2;
then consider cos being set such that
A22: a in cos and
A23: cos = (MSUnion c) . i by A21;
MSUnion c in { (MSUnion X) where X is SubsetFamily of M : X in AA } by A20;
then cos in { (t . i) where t is Element of Bool M : t in B } by A2, A23;
then a in union { (t . i) where t is Element of Bool M : t in B } by A22, TARSKI:def_4;
hence a in (MSUnion B) . i by A4, Def2; ::_thesis: verum
end;
begin
definition
let I be non empty set ;
let M be ManySortedSet of I;
let S be SetOp of M;
attrS is algebraic means :: CLOSURE3:def 3
for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A );
end;
:: deftheorem defines algebraic CLOSURE3:def_3_:_
for I being non empty set
for M being ManySortedSet of I
for S being SetOp of M holds
( S is algebraic iff for x being Element of Bool M st x = S . x holds
ex A being SubsetFamily of M st
( A = { (S . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) );
registration
let I be non empty set ;
let M be ManySortedSet of I;
cluster non empty Relation-like Bool M -defined Bool M -valued Function-like V17( Bool M) quasi_total reflexive monotonic idempotent algebraic for Element of bool [:(Bool M),(Bool M):];
existence
ex b1 being SetOp of M st
( b1 is algebraic & b1 is reflexive & b1 is monotonic & b1 is idempotent )
proof
reconsider f = id (Bool M) as SetOp of M ;
take f ; ::_thesis: ( f is algebraic & f is reflexive & f is monotonic & f is idempotent )
thus f is algebraic ::_thesis: ( f is reflexive & f is monotonic & f is idempotent )
proof
let x be Element of Bool M; :: according to CLOSURE3:def_3 ::_thesis: ( x = f . x implies ex A being SubsetFamily of M st
( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) )
assume x = f . x ; ::_thesis: ex A being SubsetFamily of M st
( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A )
set A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ;
{ (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } c= Bool M
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } or v in Bool M )
assume v in { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: v in Bool M
then ex a being Element of Bool M st
( v = f . a & a is V42() & support a is finite & a c= x ) ;
hence v in Bool M ; ::_thesis: verum
end;
then reconsider A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } as SubsetFamily of M ;
take A ; ::_thesis: ( A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A )
thus A = { (f . a) where a is Element of Bool M : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: x = MSUnion A
let i be Element of I; :: according to PBOOLE:def_21 ::_thesis: x . i = (MSUnion A) . i
thus x . i c= (MSUnion A) . i :: according to XBOOLE_0:def_10 ::_thesis: (MSUnion A) . i c= x . i
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in x . i or y in (MSUnion A) . i )
assume y in x . i ; ::_thesis: y in (MSUnion A) . i
then consider a being Element of Bool M such that
A1: y in a . i and
A2: ( a is V42() & support a is finite & a c= x ) by Th8;
a = f . a by FUNCT_1:18;
then a in A by A2;
then a . i in { (g . i) where g is Element of Bool M : g in A } ;
then y in union { (g . i) where g is Element of Bool M : g in A } by A1, TARSKI:def_4;
hence y in (MSUnion A) . i by Def2; ::_thesis: verum
end;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in (MSUnion A) . i or v in x . i )
assume v in (MSUnion A) . i ; ::_thesis: v in x . i
then v in union { (ff . i) where ff is Element of Bool M : ff in A } by Def2;
then consider Y being set such that
A3: v in Y and
A4: Y in { (ff . i) where ff is Element of Bool M : ff in A } by TARSKI:def_4;
consider ff being Element of Bool M such that
A5: Y = ff . i and
A6: ff in A by A4;
consider a being Element of Bool M such that
A7: ff = f . a and
a is V42() and
support a is finite and
A8: a c= x by A6;
ff = a by A7, FUNCT_1:18;
then ff . i c= x . i by A8, PBOOLE:def_2;
hence v in x . i by A3, A5; ::_thesis: verum
end;
thus f is reflexive ::_thesis: ( f is monotonic & f is idempotent )
proof
let X be Element of Bool M; :: according to CLOSURE2:def_10 ::_thesis: X c= f . X
thus X c= f . X by FUNCT_1:18; ::_thesis: verum
end;
thus f is monotonic ::_thesis: f is idempotent
proof
let X, Y be Element of Bool M; :: according to CLOSURE2:def_11 ::_thesis: ( not X c= Y or f . X c= f . Y )
assume A9: X c= Y ; ::_thesis: f . X c= f . Y
f . X = X by FUNCT_1:18;
hence f . X c= f . Y by A9, FUNCT_1:18; ::_thesis: verum
end;
thus f is idempotent ::_thesis: verum
proof
let X be Element of Bool M; :: according to CLOSURE2:def_12 ::_thesis: f . X = f . (f . X)
thus f . (f . X) = f . X by FUNCT_1:18; ::_thesis: verum
end;
end;
end;
definition
let S be non empty 1-sorted ;
let IT be ClosureSystem of S;
attrIT is algebraic means :: CLOSURE3:def 4
ClSys->ClOp IT is algebraic ;
end;
:: deftheorem defines algebraic CLOSURE3:def_4_:_
for S being non empty 1-sorted
for IT being ClosureSystem of S holds
( IT is algebraic iff ClSys->ClOp IT is algebraic );
definition
let S be non empty non void ManySortedSign ;
let MA be non-empty MSAlgebra over S;
func SubAlgCl MA -> strict ClosureStr over 1-sorted(# the carrier of S #) means :Def5: :: CLOSURE3:def 5
( the Sorts of it = the Sorts of MA & the Family of it = SubSort MA );
existence
ex b1 being strict ClosureStr over 1-sorted(# the carrier of S #) st
( the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA )
proof
reconsider SS = the Sorts of MA as ManySortedSet of the carrier of 1-sorted(# the carrier of S #) ;
SubSort MA c= Bool the Sorts of MA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )
assume x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA
then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11;
hence x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum
end;
then reconsider SF = SubSort MA as SubsetFamily of SS ;
take ClosureStr(# SS,SF #) ; ::_thesis: ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA )
thus ( the Sorts of ClosureStr(# SS,SF #) = the Sorts of MA & the Family of ClosureStr(# SS,SF #) = SubSort MA ) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being strict ClosureStr over 1-sorted(# the carrier of S #) st the Sorts of b1 = the Sorts of MA & the Family of b1 = SubSort MA & the Sorts of b2 = the Sorts of MA & the Family of b2 = SubSort MA holds
b1 = b2 ;
end;
:: deftheorem Def5 defines SubAlgCl CLOSURE3:def_5_:_
for S being non empty non void ManySortedSign
for MA being non-empty MSAlgebra over S
for b3 being strict ClosureStr over 1-sorted(# the carrier of S #) holds
( b3 = SubAlgCl MA iff ( the Sorts of b3 = the Sorts of MA & the Family of b3 = SubSort MA ) );
theorem Th14: :: CLOSURE3:14
for S being non empty non void ManySortedSign
for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
proof
let S be non empty non void ManySortedSign ; ::_thesis: for MA being strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
let MA be strict non-empty MSAlgebra over S; ::_thesis: SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA
SubSort MA c= Bool the Sorts of MA
proof
let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SubSort MA or x in Bool the Sorts of MA )
assume x in SubSort MA ; ::_thesis: x in Bool the Sorts of MA
then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def_11;
hence x in Bool the Sorts of MA by CLOSURE2:def_1; ::_thesis: verum
end;
then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA ;
for F being SubsetFamily of the Sorts of MA st F c= SUBMA holds
meet |:F:| in SUBMA
proof
set M = bool (Union the Sorts of MA);
set I = the carrier of S;
let F be SubsetFamily of the Sorts of MA; ::_thesis: ( F c= SUBMA implies meet |:F:| in SUBMA )
assume A1: F c= SUBMA ; ::_thesis: meet |:F:| in SUBMA
set x = meet |:F:|;
A2: dom (meet |:F:|) = the carrier of S by PARTFUN1:def_2;
rng (meet |:F:|) c= bool (Union the Sorts of MA)
proof
let u be set ; :: according to TARSKI:def_3 ::_thesis: ( not u in rng (meet |:F:|) or u in bool (Union the Sorts of MA) )
assume u in rng (meet |:F:|) ; ::_thesis: u in bool (Union the Sorts of MA)
then consider i being set such that
A3: i in dom (meet |:F:|) and
A4: u = (meet |:F:|) . i by FUNCT_1:def_3;
dom the Sorts of MA = the carrier of S by PARTFUN1:def_2;
then the Sorts of MA . i in rng the Sorts of MA by A2, A3, FUNCT_1:def_3;
then A5: the Sorts of MA . i c= union (rng the Sorts of MA) by ZFMISC_1:74;
ex Q being Subset-Family of ( the Sorts of MA . i) st
( Q = |:F:| . i & u = Intersect Q ) by A2, A3, A4, MSSUBFAM:def_1;
then u c= union (rng the Sorts of MA) by A5, XBOOLE_1:1;
then u in bool (union (rng the Sorts of MA)) ;
hence u in bool (Union the Sorts of MA) by CARD_3:def_4; ::_thesis: verum
end;
then A6: meet |:F:| in Funcs ( the carrier of S,(bool (Union the Sorts of MA))) by A2, FUNCT_2:def_2;
reconsider x = meet |:F:| as MSSubset of MA ;
for B being MSSubset of MA st B = x holds
B is opers_closed by A1, Th3;
hence meet |:F:| in SUBMA by A6, MSUALG_2:def_11; ::_thesis: verum
end;
hence SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA by CLOSURE2:def_7; ::_thesis: verum
end;
registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA -> strict absolutely-multiplicative ;
coherence
SubAlgCl MA is absolutely-multiplicative
proof
thus SubAlgCl MA is absolutely-multiplicative ::_thesis: verum
proof
reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th14;
set F = the Family of (SubAlgCl MA);
( the Sorts of (SubAlgCl MA) = the Sorts of MA & the Family of (SubAlgCl MA) = SF ) by Def5;
hence SubAlgCl MA is absolutely-multiplicative ; ::_thesis: verum
end;
end;
end;
registration
let S be non empty non void ManySortedSign ;
let MA be strict non-empty MSAlgebra over S;
cluster SubAlgCl MA -> strict algebraic ;
coherence
SubAlgCl MA is algebraic
proof
set I = the carrier of S;
set SS = ClSys->ClOp (SubAlgCl MA);
set M = the Sorts of (SubAlgCl MA);
let x be Element of Bool the Sorts of (SubAlgCl MA); :: according to CLOSURE3:def_3,CLOSURE3:def_4 ::_thesis: ( x = (ClSys->ClOp (SubAlgCl MA)) . x implies ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st
( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A ) )
assume A1: x = (ClSys->ClOp (SubAlgCl MA)) . x ; ::_thesis: ex A being SubsetFamily of the Sorts of (SubAlgCl MA) st
( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A )
set A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } ;
{ ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } c= Bool the Sorts of (SubAlgCl MA)
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } or v in Bool the Sorts of (SubAlgCl MA) )
assume v in { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } ; ::_thesis: v in Bool the Sorts of (SubAlgCl MA)
then ex a being Element of Bool the Sorts of (SubAlgCl MA) st
( v = (ClSys->ClOp (SubAlgCl MA)) . a & a is V42() & support a is finite & a c= x ) ;
then reconsider vv = v as Element of Bool the Sorts of (SubAlgCl MA) ;
vv in Bool the Sorts of (SubAlgCl MA) ;
hence v in Bool the Sorts of (SubAlgCl MA) ; ::_thesis: verum
end;
then reconsider A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } as SubsetFamily of the Sorts of (SubAlgCl MA) ;
take A ; ::_thesis: ( A = { ((ClSys->ClOp (SubAlgCl MA)) . a) where a is Element of Bool the Sorts of (SubAlgCl MA) : ( a is V42() & support a is finite & a c= x ) } & x = MSUnion A )
thus A = { ((ClSys->ClOp (SubAlgCl MA)) . b) where b is Element of Bool the Sorts of (SubAlgCl MA) : ( b is V42() & support b is finite & b c= x ) } ; ::_thesis: x = MSUnion A
reconsider y = x, z = MSUnion A as ManySortedSet of the carrier of S ;
y = z
proof
let i be Element of the carrier of S; :: according to PBOOLE:def_21 ::_thesis: y . i = z . i
reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as reflexive SetOp of the Sorts of (SubAlgCl MA) ;
thus y . i c= z . i :: according to XBOOLE_0:def_10 ::_thesis: z . i c= y . i
proof
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in y . i or v in z . i )
assume v in y . i ; ::_thesis: v in z . i
then consider b being Element of Bool the Sorts of (SubAlgCl MA) such that
A2: v in b . i and
A3: ( b is V42() & support b is finite & b c= x ) by Th8;
b c=' SS9 . b by CLOSURE2:def_10;
then A4: b . i c= (SS9 . b) . i by PBOOLE:def_2;
(ClSys->ClOp (SubAlgCl MA)) . b in A by A3;
then (SS9 . b) . i in { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } ;
then v in union { (f . i) where f is Element of Bool the Sorts of (SubAlgCl MA) : f in A } by A2, A4, TARSKI:def_4;
hence v in z . i by Def2; ::_thesis: verum
end;
reconsider SS9 = ClSys->ClOp (SubAlgCl MA) as monotonic SetOp of the Sorts of (SubAlgCl MA) ;
let v be set ; :: according to TARSKI:def_3 ::_thesis: ( not v in z . i or v in y . i )
assume v in z . i ; ::_thesis: v in y . i
then v in union { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by Def2;
then consider Y being set such that
A5: v in Y and
A6: Y in { (ff . i) where ff is Element of Bool the Sorts of (SubAlgCl MA) : ff in A } by TARSKI:def_4;
consider ff being Element of Bool the Sorts of (SubAlgCl MA) such that
A7: Y = ff . i and
A8: ff in A by A6;
consider a being Element of Bool the Sorts of (SubAlgCl MA) such that
A9: ff = (ClSys->ClOp (SubAlgCl MA)) . a and
a is V42() and
support a is finite and
A10: a c=' x by A8;
SS9 . a c=' SS9 . x by A10, CLOSURE2:def_11;
then ff . i c= x . i by A1, A9, PBOOLE:def_2;
hence v in y . i by A5, A7; ::_thesis: verum
end;
hence x = MSUnion A ; ::_thesis: verum
end;
end;