:: Algebraic Operation on Subsets of Many Sorted Sets :: by Agnieszka Julia Marasik :: :: Received June 23, 1997 :: Copyright (c) 1997-2018 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies XBOOLE_0, STRUCT_0, PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1, MSUALG_1, TARSKI, MSUALG_2, UNIALG_2, MSSUBFAM, FUNCT_1, MARGREL1, SUBSET_1, FINSET_1, FUNCOP_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1, ZFMISC_1, CARD_3, FUNCT_2, CLOSURE3, PRE_POLY, SETLIM_2; notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, FUNCOP_1, PBOOLE, FINSEQ_2, MSUALG_1, MSUALG_2, CARD_3, PRE_POLY, CLOSURE2, MSSUBFAM, MBOOLEAN; constructors SETFAM_1, FUNCT_4, MSSUBFAM, MSUALG_2, PRALG_2, CLOSURE2, RELSET_1, FINSEQ_2, PRE_POLY; registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, PBOOLE, STRUCT_0, MSUALG_1, CLOSURE2, FINSEQ_1; requirements SUBSET, BOOLE; definitions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE; equalities PBOOLE, ORDINAL1; expansions TARSKI, XBOOLE_0, CLOSURE2, MSUALG_2, SETFAM_1, PBOOLE; theorems FUNCT_4, FUNCT_1, TARSKI, PBOOLE, MSUALG_1, MBOOLEAN, FUNCOP_1, MSUALG_2, CLOSURE2, ZFMISC_1, RELAT_1, CARD_3, MSSUBFAM, FUNCT_2, XBOOLE_0, SETFAM_1, PARTFUN1, FINSET_1, PRE_POLY; schemes CLASSES1; begin :: Preliminaries registration let S be non empty 1-sorted; cluster the 1-sorted of S -> non empty; coherence; end; theorem Th1: for I be non empty set, M, N be ManySortedSet of I holds M +* N = N proof let I be non empty set, M, N be ManySortedSet of I; dom M = I by PARTFUN1:def 2 .= dom N by PARTFUN1:def 2; hence thesis by FUNCT_4:19; end; theorem for I be set, M, N be ManySortedSet of I, F be SubsetFamily of M holds N in F implies meet |:F:| c=' N by CLOSURE2:21,MSSUBFAM:43; theorem Th3: for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S for F be SubsetFamily of the Sorts of MA st F c= SubSort MA for B be MSSubset of MA st B = meet |:F:| holds B is opers_closed proof let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; let F be SubsetFamily of the Sorts of MA such that A1: F c= SubSort MA; let B be MSSubset of MA such that A2: B = meet |:F:|; per cases; suppose A3: F = {}; set Q = the Sorts of MA; reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA; set I = the carrier of S; FF = EmptyMS I by A3; then A4: Q = B by A2,MSSUBFAM:41; reconsider Q as MSSubset of MA by PBOOLE:def 18; for o be OperSymbol of S holds Q is_closed_on o proof let o be OperSymbol of S; 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 thesis by A7,A6; end; hence thesis by A4; end; suppose A8: F <> {}; set SS = S; let o be OperSymbol of SS; set i = (the_result_sort_of o); A9: (the ResultSort of SS).o = the_result_sort_of o by MSUALG_1:def 2; A10: dom the ResultSort of SS = the carrier' of SS by FUNCT_2:def 1; (the Arity of SS).o = the_arity_of o & dom the Arity of SS = the carrier' of SS by FUNCT_2:def 1,MSUALG_1:def 1; then A11: (B# * (the Arity of SS)).o = B#.(the_arity_of o) by FUNCT_1:13; Result(o,MA) = ((the Sorts of MA) * the ResultSort of SS).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 be Subset-Family of ((the Sorts of MA).i) such that A14: Q = |:F:|.i and A15: B.i = Intersect Q by A2,MSSUBFAM:def 1; let v be object; assume A16: v in rng ((Den(o,MA))|((B#.(the_arity_of o)))); then consider p be object 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:|.i = { xx.i where xx is Element of Bool the Sorts of MA : xx in F } by A8,CLOSURE2:14; let Y be set; assume Y in Q; then consider xx be Element of Bool the Sorts of MA such that A20: Y = xx.i and A21: xx in F by A14,A19; reconsider xx as MSSubset of MA; xx is opers_closed by A1,A21,MSUALG_2:14; then xx is_closed_on o; then A22: rng ((Den(o,MA))|((xx# * the Arity of SS).o)) c= (xx * the ResultSort of SS).o; B c= xx by A2,A21,CLOSURE2:21,MSSUBFAM:43; then (Den(o,MA))|((B# * the Arity of SS).o) c= (Den(o,MA))|((xx# * the Arity of SS).o) by MSUALG_2:2,RELAT_1:75; then A23: dom ((Den(o,MA))|((B# * the Arity of SS).o)) c= dom ((Den(o,MA))| ((xx# * the Arity of SS).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 SS).o)).p by A11,A17,A23, FUNCT_1:47; then v in rng ((Den(o,MA))|((xx# * the Arity of SS).o)) by A11,A17,A23, FUNCT_1:def 3; then (Den(o,MA)).p in (xx * the ResultSort of SS).o by A22,A24; then (Den(o,MA)).p in xx.((the ResultSort of SS).o) by A10,FUNCT_1:13; then (Den(o,MA)).p in xx.i by MSUALG_1:def 2; hence thesis by A17,A18,A20,FUNCT_1:47; end; hence thesis by A12,A16,A15,SETFAM_1:43; end; (B * the ResultSort of SS).o = B.(the_result_sort_of o) by A9,A10, FUNCT_1:13; hence thesis by A11,A13; end; end; begin :: Relationships between Subsets Families theorem for A,B,C be set holds A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C proof let A,B,C be set; assume that A1: A is_coarser_than B and A2: B is_coarser_than C; let a be set; assume a in A; then consider b be set such that A3: b in B and A4: b c= a by A1; consider c be set such that A5: c in C & c c= b by A2,A3; take c; thus thesis by A4,A5; end; Lm1: now let I be non empty set, M be ManySortedSet of I; set F = { x where x is Element of I : M.x <> {} }; thus support M = F proof thus support M c= F proof let x be object; A1: dom M = I by PARTFUN1:def 2; A2: support M c= dom M by PRE_POLY:37; assume A3: x in support M; then M.x <> {} by PRE_POLY:def 7; hence thesis by A1,A2,A3; end; let x be object; assume x in F; then ex i being Element of I st x = i & M.i <> {}; hence thesis by PRE_POLY:def 7; end; end; definition let I be non empty set, M be ManySortedSet of I; redefine func support M equals { x where x is Element of I : M.x <> {} }; compatibility by Lm1; end; theorem for I be non empty set, M be non-empty ManySortedSet of I holds M = EmptyMS I +* (M|support M) proof let I be non empty set, M be non-empty ManySortedSet of I; set MM = M|support M; A1: I c= support M proof let v be object; assume A2: v in I; then M.v <> {}; hence thesis by A2; end; dom M = I by PARTFUN1:def 2; then MM = M by A1,RELAT_1:68; hence thesis by Th1; end; theorem for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds M1|support M1 = M2|support M2 implies M1 = M2 proof let I be non empty set, M1, M2 be non-empty ManySortedSet of I; A1: dom M1 = I by PARTFUN1:def 2; A2: dom M2 = I by PARTFUN1:def 2; assume A3: M1|support M1 = M2|support M2; for x be object st x in I holds M1.x = M2.x proof let x be object; A4: dom (M2|support M2) = dom M2 /\ support M2 by RELAT_1:61; assume A5: x in I; then M1.x is non empty; then A6: x in support M1 by A5; M2.x is non 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 thesis; end; hence thesis; end; ::$CT theorem Th7: for I being non empty set, M being ManySortedSet of I, x being Element of Bool M, i being Element of I for y being set st y in x.i ex a being Element of Bool M st y in a.i & a is finite-yielding & support a is finite & a c= x proof let I be non empty set, M be ManySortedSet of I, x be Element of Bool M, i be Element of I; let y be set such that A1: y in x.i; set N = {i} --> {y}; set A = EmptyMS I +* N; A2: dom N = {i} by FUNCOP_1:13; then A3: i in dom N by TARSKI:def 1; then A4: N.i = {y} by A2,FUNCOP_1:7; then A5: A.i = {y} by A3,FUNCT_4:13; A6: dom A = dom EmptyMS I \/ dom N by FUNCT_4:def 1 .= I \/ {i} by A2,PARTFUN1:def 2 .= I by ZFMISC_1:40; then reconsider A as ManySortedSet of I by PARTFUN1:def 2,RELAT_1:def 18; for j be object st j in I holds A.j c= M.j proof let j be object such that A7: j in I; per cases; suppose A8: i = j; reconsider x as ManySortedSubset of M; let v be object; assume v in A.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; hence thesis by A9; end; suppose i <> j; then A10: not j in {i} by TARSKI:def 1; j in dom EmptyMS I \/ dom N 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 thesis; end; end; then A c= M; 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 be object st j in I holds a.j c= x.j proof let j be object such that A12: j in I; per cases; suppose A13: i = j; let v be object; assume A14: v in a.j; a.j = {y} by A3,A4,A13,FUNCT_4:13; hence thesis by A1,A13,A14,TARSKI:def 1; end; suppose j <> i; then A15: not j in {i} by TARSKI:def 1; j in dom EmptyMS I \/ dom N 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 thesis; 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} proof let s be object; assume s in { b where b is Element of I : a.b <> {}}; then A17: ex b be Element of I st s = b & a.b <> {}; assume A18: not s in {i}; reconsider s as Element of I by A17; s in dom a by A6; then s in dom EmptyMS I \/ dom N 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; end; let s be object; assume A19: s in {i}; then A20: s = i by TARSKI:def 1; reconsider s as Element of I by A19,TARSKI:def 1; a.s = {y} by A3,A4,A20,FUNCT_4:13; hence thesis; end; take a; for j be object st j in I holds a.j is finite proof let j be object such that A21: j in I; per cases; suppose j = i; hence thesis by A3,A4,FUNCT_4:13; end; suppose j <> i; then A22: not j in {i} by TARSKI:def 1; j in dom EmptyMS I \/ dom N 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 thesis; end; end; hence thesis by A5,A16,A11,FINSET_1:def 5,TARSKI:def 1; end; definition let I be set, M be ManySortedSet of I; let A be SubsetFamily of M; func MSUnion A -> ManySortedSubset of M means :Def2: for i be set st i in I holds it.i = union { f.i where f is Element of Bool M: f in A }; existence proof defpred P[object,object] means $2 = union { f.$1 where f is Element of Bool M:f in A }; A1: for x be object st x in I ex y be object st P[x,y]; consider IT be Function such that A2: dom IT = I and A3: for x be object st x in I holds P[x, IT.x] from CLASSES1:sch 1(A1); reconsider IT as ManySortedSet of I by A2,PARTFUN1:def 2,RELAT_1:def 18; for i be object st i in I holds IT.i c= M.i proof let i be object such that A4: i in I; for x be object holds x in IT.i implies x in M.i proof let x be object; assume A5: x in IT.i; IT.i = union { f.i where f is Element of Bool M: f in A } by A3,A4; then consider Y be 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 be Element of Bool M such that A8: ff.i = Y and ff in A by A7; reconsider ff as ManySortedSubset of M; ff c= M by PBOOLE:def 18; then ff.i c= M.i by A4; hence thesis by A6,A8; end; hence thesis; end; then IT c= M; then reconsider IT as ManySortedSubset of M by PBOOLE:def 18; take IT; thus thesis by A3; end; uniqueness proof let B1,B2 be ManySortedSubset of M; assume that A9: for i be 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 be set st i in I holds B2.i = union { ff.i where ff is Element of Bool M: ff in A }; for i be object st i in I holds B1.i = B2.i proof let i be object; assume A11: i in 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 thesis; end; hence thesis; end; end; registration let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M; cluster MSUnion A -> empty-yielding; coherence proof let i be object; set MA = MSUnion A; assume i in I; then A1: MA.i = union {f.i where f is Element of Bool M : f in A} by Def2; assume MA.i is non empty; then consider v being object such that A2: v in MA.i; consider h be 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 be Element of Bool M st h = g.i & g in A by A3; hence contradiction; end; end; theorem for I be set, M be ManySortedSet of I, A be SubsetFamily of M holds MSUnion A = union |:A:| proof let I be set, M be ManySortedSet of I, A be SubsetFamily of M; set AA = |:A:|; reconsider UA = union AA as ManySortedSet of I; per cases; suppose A1: A is non empty; for i be object st i in I holds (MSUnion A).i = UA.i proof let i be object; assume A2: i in I; then AA.i = { g.i where g is Element of Bool M : g in A } & UA.i = union (AA.i) by A1,CLOSURE2:14,MBOOLEAN:def 2; hence thesis by A2,Def2; end; hence thesis; end; suppose A3: A is empty SubsetFamily of M; for i be object st i in I holds (MSUnion A).i = UA.i proof let i be object; assume i in I; AA = EmptyMS I by A3; then UA = EmptyMS I by MBOOLEAN:21; then UA.i is empty; hence thesis by A3; end; hence thesis; end; end; definition let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M; redefine func A \/ B -> SubsetFamily of M; correctness by CLOSURE2:3; end; theorem for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds MSUnion (A \/ B) = MSUnion A (\/) MSUnion B proof let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M; reconsider MAB = MSUnion (A \/ B) as ManySortedSubset of M; reconsider MAB as ManySortedSet of I; reconsider MA = MSUnion A as ManySortedSubset of M; reconsider MA as ManySortedSet of I; reconsider MB = MSUnion B as ManySortedSubset of M; reconsider MB as ManySortedSet of I; for i be object st i in I holds MAB.i = (MA (\/) MB).i proof let i be object; assume A1: i in 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 be object holds v in (MA (\/) MB).i implies v in MAB.i proof let v be object; assume v in (MA (\/) MB).i; then A5: v in MA.i or v in MB.i by A3,XBOOLE_0:def 3; per cases by A1,A5,Def2; suppose v in union { f.i where f is Element of Bool M : f in A}; then consider g be 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 be 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 thesis by A2,A6,TARSKI:def 4; end; suppose v in union { f.i where f is Element of Bool M : f in B}; then consider g be 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 be 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 thesis by A2,A10,TARSKI:def 4; 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 be object holds v in MAB.i implies v in (MA (\/) MB).i proof let v be object; assume v in MAB.i; then consider h be 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 be 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 thesis by A3,A14,XBOOLE_0:def 3; end; hence thesis by A4,TARSKI:2; end; hence thesis; end; theorem for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds A c= B implies MSUnion A c= MSUnion B proof let I be set, M be ManySortedSet of I; let A, B be SubsetFamily of M; reconsider MA = MSUnion A as ManySortedSubset of M; reconsider MA as ManySortedSet of I; reconsider MB = MSUnion B as ManySortedSubset of M; reconsider MB as ManySortedSet of I; assume A1: A c= B; for i be object st i in I holds MA.i c= MB.i proof let i be object such that A2: i in I; for v be object 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 object; assume v in MA.i; then consider h be 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 be 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 thesis by A2,Def2; end; hence thesis; end; hence thesis; end; definition let I be set, M be ManySortedSet of I, A, B be SubsetFamily of M; redefine func A /\ B -> SubsetFamily of M; correctness by CLOSURE2:4; end; theorem for I be set, M be ManySortedSet of I for A, B be SubsetFamily of M holds MSUnion (A /\ B) c= MSUnion A (/\) MSUnion B proof let I be set, M be ManySortedSet of I; let A, B be SubsetFamily of M; 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 be object st i in I holds MAB.i c= (MA (/\) MB).i proof let i be object; assume A1: i in 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 be object st v in MAB.i holds v in (MA (/\) MB).i proof let v be object; assume v in MAB.i; then consider w be 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 be 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 thesis by A1,PBOOLE:def 5; end; hence thesis; end; hence thesis; end; theorem for I be set, M be ManySortedSet of I, AA be set st for x being set st x in AA holds x is SubsetFamily of M for A,B be 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, M be ManySortedSet of I, AA be set such that A1: for x being set st x in AA holds x is SubsetFamily of M; let A,B be SubsetFamily of M such that A2: B = { MSUnion X where X is SubsetFamily of M : X in AA} and A3: A = union AA; let i be object such that A4: i in I; thus (MSUnion B).i c= (MSUnion A).i proof let a be object; thus a in (MSUnion B).i implies a in (MSUnion A).i proof assume a in (MSUnion B).i; then a in union { f.i where f is Element of Bool M: f in B} by A4,Def2; then consider Y be 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 be Element of Bool M such that A7: f.i = Y and A8: f in B by A6; consider Q be 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 be 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 be 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 thesis by A3,A4,Def2; end; end; let a be object; assume a in (MSUnion A).i; then a in union { f.i where f is Element of Bool M: f in A} by A4,Def2; then consider Y be 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 be Element of Bool M such that A17: f.i = Y and A18: f in A by A16; consider c be set such that A19: f in c and A20: c in AA by A3,A18,TARSKI:def 4; reconsider 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 be 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 thesis by A4,Def2; end; begin ::Algebraic Operation on Subsets of Many Sorted Sets definition let I be non empty set, M be ManySortedSet of I, S be SetOp of M; attr S is algebraic means for x be Element of Bool M st x = S.x ex A be SubsetFamily of M st A = { S.a where a is Element of Bool M : a is finite-yielding & support a is finite & a c= x} & x = MSUnion A; end; registration let I be non empty set, M be ManySortedSet of I; cluster algebraic reflexive monotonic idempotent for SetOp of M; existence proof reconsider f = id (Bool M) as SetOp of M; take f; thus f is algebraic proof let x be Element of Bool M such that x = f.x; set A = { f.a where a is Element of Bool M : a is finite-yielding & support a is finite & a c= x}; A c= Bool M proof let v be object; assume v in A; then ex a be Element of Bool M st v = f.a & a is finite-yielding & support a is finite & a c= x; hence thesis; end; then reconsider A as SubsetFamily of M; take A; thus A = { f.a where a is Element of Bool M : a is finite-yielding & support a is finite & a c= x}; let i be Element of I; thus x.i c= (MSUnion A).i proof let y be object; assume y in x.i; then consider a be Element of Bool M such that A1: y in a.i and A2: a is finite-yielding & support a is finite & a c= x by Th7; a = f.a; 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 thesis by Def2; end; let v be object; assume v in (MSUnion A).i; then v in union {ff.i where ff is Element of Bool M: ff in A} by Def2; then consider Y be 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 be Element of Bool M such that A5: Y = ff.i and A6: ff in A by A4; consider a be Element of Bool M such that A7: ff = f.a and a is finite-yielding and support a is finite and A8: a c= x by A6; ff = a by A7; then ff.i c= x.i by A8; hence thesis by A3,A5; end; thus f is reflexive; thus f is monotonic; thus f is idempotent; end; end; definition let S be non empty 1-sorted, IT be ClosureSystem of S; attr IT is algebraic means ClSys->ClOp IT is algebraic; end; definition let S be non void non empty ManySortedSign, MA be non-empty MSAlgebra over S; func SubAlgCl MA -> strict ClosureStr over the 1-sorted of S means :Def5: the Sorts of it = the Sorts of MA & the Family of it = SubSort MA; existence proof reconsider SS = the Sorts of MA as ManySortedSet of the carrier of the 1-sorted of S; SubSort MA c= Bool the Sorts of MA proof let x be object; assume x in SubSort MA; then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11; hence thesis by CLOSURE2:def 1; end; then reconsider SF = SubSort MA as SubsetFamily of SS; take ClosureStr (#SS, SF#); thus thesis; end; uniqueness; end; theorem Th13: for S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S holds SubSort MA is absolutely-multiplicative SubsetFamily of the Sorts of MA proof let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; SubSort MA c= Bool the Sorts of MA proof let x be object; assume x in SubSort MA; then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 11; hence thesis by CLOSURE2:def 1; end; then reconsider SUBMA = SubSort MA as SubsetFamily of the Sorts of MA; for F be 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 such that A1: F c= SUBMA; set x = meet |:F:|; A2: dom x = I by PARTFUN1:def 2; rng x c= M proof let u be object; reconsider uu=u as set by TARSKI:1; assume u in rng x; then consider i be object such that A3: i in dom x and A4: u = x.i by FUNCT_1:def 3; dom (the Sorts of MA) = I 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 be Subset-Family of (the Sorts of MA).i st Q = |:F:|. i & u = Intersect Q by A2,A3,A4,MSSUBFAM:def 1; then uu c= union rng (the Sorts of MA) by A5; then u in bool (union rng (the Sorts of MA)); hence thesis by CARD_3:def 4; end; then A6: x in Funcs ( I, M) by A2,FUNCT_2:def 2; reconsider x as MSSubset of MA; for B be MSSubset of MA st B = x holds B is opers_closed by A1,Th3; hence thesis by A6,MSUALG_2:def 11; end; hence thesis by CLOSURE2:def 7; end; registration let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> absolutely-multiplicative; coherence proof thus SubAlgCl MA is absolutely-multiplicative proof reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th13; set F = the Family of SubAlgCl MA; the Sorts of SubAlgCl MA = the Sorts of MA & F = SF by Def5; hence thesis; end; end; end; registration let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> algebraic; coherence proof set I = the carrier of S; set SS = ClSys->ClOp SubAlgCl MA, M = the Sorts of SubAlgCl MA; let x be Element of Bool M such that A1: x = SS.x; set A = { SS.a where a is Element of Bool M : a is finite-yielding & support a is finite & a c= x}; A c= Bool M proof let v be object; assume v in A; then ex a be Element of Bool M st v = SS.a & a is finite-yielding & support a is finite & a c= x; then reconsider vv = v as Element of Bool M; vv in Bool M; hence thesis; end; then reconsider A as SubsetFamily of M; take A; thus A = { SS.b where b is Element of Bool M : b is finite-yielding & support b is finite & b c= x}; reconsider y = x, z = MSUnion A as ManySortedSet of I; y = z proof let i be Element of I; reconsider SS9 = SS as reflexive SetOp of M; thus y.i c= z.i proof let v be object; assume v in y.i; then consider b be Element of Bool M such that A2: v in b.i and A3: b is finite-yielding & support b is finite & b c= x by Th7; b c=' SS9.b by CLOSURE2:def 10; then A4: b.i c= (SS9.b).i; SS.b in A by A3; then (SS9.b).i in {f.i where f is Element of Bool M : f in A}; then v in union {f.i where f is Element of Bool M : f in A} by A2,A4, TARSKI:def 4; hence thesis by Def2; end; reconsider SS9 = SS as monotonic SetOp of M; let v be object; assume v in z.i; then v in union {ff.i where ff is Element of Bool M: ff in A} by Def2; then consider Y be set such that A5: v in Y and A6: Y in {ff.i where ff is Element of Bool M: ff in A} by TARSKI:def 4; consider ff be Element of Bool M such that A7: Y = ff.i and A8: ff in A by A6; consider a be Element of Bool M such that A9: ff = SS.a and a is finite-yielding 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; hence thesis by A5,A7; end; hence thesis; end; end;