### The Mizar article:

### Algebraic Operation on Subsets of Many Sorted Sets

**by****Agnieszka Julia Marasik**

- Received June 23, 1997
Copyright (c) 1997 Association of Mizar Users

- MML identifier: CLOSURE3
- [ MML identifier index ]

environ vocabulary PBOOLE, FUNCT_4, RELAT_1, CLOSURE2, SETFAM_1, MSSUBFAM, AMI_1, MSUALG_1, ZF_REFLE, MSUALG_2, UNIALG_2, BOOLE, CAT_4, FUNCT_1, QC_LANG1, TDGROUP, CANTOR_1, PRE_CIRC, FINSET_1, FUNCOP_1, TARSKI, MATRIX_1, WAYBEL_8, RELAT_2, MSAFREE2, BINOP_1, CLOSURE1, PROB_1, FUNCT_2, CLOSURE3; notation TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, CANTOR_1, SETFAM_1, RELAT_1, FUNCT_1, STRUCT_0, PARTFUN1, FUNCT_2, FINSET_1, FUNCT_4, PBOOLE, MSUALG_1, MSUALG_2, PROB_1, CLOSURE2, MSSUBFAM, MBOOLEAN, PRE_CIRC; constructors CLOSURE2, PRE_CIRC, PRALG_2, CANTOR_1, PROB_1, MSSUBFAM; clusters STRUCT_0, MSUALG_1, FUNCT_1, PBOOLE, CLOSURE2, FINSET_1, MSSUBFAM, RELSET_1, SUBSET_1, FUNCT_2, XBOOLE_0; requirements SUBSET, BOOLE; definitions XBOOLE_0, TARSKI, PBOOLE, CLOSURE2, MSUALG_2; theorems FUNCT_4, FUNCT_1, TARSKI, PBOOLE, MSUALG_1, MBOOLEAN, FUNCOP_1, MSUALG_2, STRUCT_0, CLOSURE2, ZFMISC_1, RELAT_1, PRE_CIRC, PROB_1, CANTOR_1, MSSUBFAM, FUNCT_2, RELSET_1, XBOOLE_0, XBOOLE_1; schemes FUNCT_1; begin :: Preliminaries definition let S be non empty 1-sorted; cluster the 1-sorted of S -> non empty; coherence by STRUCT_0:def 1; 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 PBOOLE:def 3 .= dom N by PBOOLE:def 3; hence thesis by FUNCT_4:20; end; theorem Th2: for I be set, M, N be ManySortedSet of I, F be SubsetFamily of M holds N in F implies meet |:F:| c=' N proof let I be set, M, N be ManySortedSet of I, F be SubsetFamily of M; assume N in F; then N in |:F:| by CLOSURE2:22; hence thesis by MSSUBFAM:43; end; 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 I = the carrier of S; reconsider FF = |:F:| as MSSubsetFamily of the Sorts of MA; A4: FF = [0]I by A3,CLOSURE2:def 4; set Q = the Sorts of MA; A5: Q = B by A2,A4,MSSUBFAM:41; reconsider Q as MSSubset of MA by MSUALG_2:def 1; for o be OperSymbol of S holds Q is_closed_on o proof let o be OperSymbol of S; A6: the OperSymbols of S <> {} by MSUALG_1:def 5; A7: (the Arity of S).o = the_arity_of o & (the ResultSort of S).o = the_result_sort_of o by MSUALG_1:def 6,def 7; A8: dom the Arity of S = the OperSymbols of S by FUNCT_2:def 1; A9: dom the ResultSort of S = the OperSymbols of S by FUNCT_2:def 1; A10: (Q# * (the Arity of S)).o = Q#.(the_arity_of o) by A6,A7,A8, FUNCT_1:23; A11: (Q * the ResultSort of S).o = Q.(the_result_sort_of o) by A6,A7,A9 ,FUNCT_1:23; A12: rng Den(o,MA) c= Result(o,MA) by RELSET_1:12; A13: Result(o,MA) = (Q * the ResultSort of S).o by MSUALG_1:def 10 .= Q.(the_result_sort_of o) by A6,A7,A9,FUNCT_1:23; rng ((Den(o,MA))|(Q#.(the_arity_of o))) c= rng Den(o,MA) by FUNCT_1:76; then rng ((Den(o,MA))|((Q#.(the_arity_of o)))) c= Q.(the_result_sort_of o) by A12,A13,XBOOLE_1:1; hence thesis by A10,A11,MSUALG_2:def 6; end; hence thesis by A5,MSUALG_2:def 7; suppose A14: F <> {}; set SS = S; let o be OperSymbol of SS; A15: the OperSymbols of SS <> {} by MSUALG_1:def 5; set i = (the_result_sort_of o); A16: (the Arity of SS).o = the_arity_of o & (the ResultSort of SS).o = the_result_sort_of o by MSUALG_1:def 6,def 7; A17: dom the Arity of SS = the OperSymbols of SS by FUNCT_2:def 1; A18: dom the ResultSort of SS = the OperSymbols of SS by FUNCT_2:def 1; A19: (B# * (the Arity of SS)).o = B#.(the_arity_of o) by A15,A16,A17,FUNCT_1 :23; A20: (B * the ResultSort of SS).o = B.(the_result_sort_of o) by A15,A16,A18, FUNCT_1:23; A21: rng Den(o,MA) c= Result(o,MA) by RELSET_1:12; A22: Result(o,MA) = ((the Sorts of MA) * the ResultSort of SS).o by MSUALG_1:def 10 .= (the Sorts of MA).(the_result_sort_of o) by A15,A16,A18,FUNCT_1: 23; rng ((Den(o,MA))|(B#.(the_arity_of o))) c= rng Den(o,MA) by FUNCT_1:76; then A23: rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= (the Sorts of MA).(the_result_sort_of o) by A21,A22,XBOOLE_1:1; rng ((Den(o,MA))|((B#.(the_arity_of o)))) c= B.(the_result_sort_of o) proof let v be set; assume A24: v in rng ((Den(o,MA))|((B#.(the_arity_of o)))); then consider p be set such that A25: p in dom ((Den(o,MA))|(B#.(the_arity_of o))) & v = ((Den(o,MA))|(B#.(the_arity_of o))).p by FUNCT_1:def 5; consider Q be Subset-Family of ((the Sorts of MA).i) such that A26: Q = |:F:|.i and A27: B.i = Intersect Q by A2,MSSUBFAM:def 2; for Y being set st Y in Q holds v in Y proof let Y be set such that A28: Y in Q; |:F:|.i = { xx.i where xx is Element of Bool the Sorts of MA : xx in F } by A14,CLOSURE2:15; then consider xx be Element of Bool the Sorts of MA such that A29: Y = xx.i & xx in F by A26,A28; reconsider xx as MSSubset of MA; xx is opers_closed by A1,A29,MSUALG_2:15; then xx is_closed_on o by MSUALG_2:def 7; then A30: rng ((Den(o,MA))|((xx# * the Arity of SS).o)) c= (xx * the ResultSort of SS).o by MSUALG_2:def 6; B c= xx by A2,A29,Th2; then (B#*(the Arity of SS)).o c= (xx#*(the Arity of SS)).o by MSUALG_2:3; then (Den(o,MA))|((B# * the Arity of SS).o) c= (Den(o,MA))|((xx# * the Arity of SS).o) by RELAT_1:104; then A31: dom ((Den(o,MA))|((B# * the Arity of SS).o)) c= dom ((Den(o,MA))|((xx# * the Arity of SS).o)) by RELAT_1:25; A32: v = (Den(o,MA)).p by A25,FUNCT_1:70; then v = ((Den(o,MA))|((xx# * the Arity of SS).o)).p by A19,A25,A31,FUNCT_1:70; then v in rng ((Den(o,MA))|((xx# * the Arity of SS).o)) by A19,A25,A31,FUNCT_1:def 5; then (Den(o,MA)).p in (xx * the ResultSort of SS).o by A30,A32; then (Den(o,MA)).p in xx.((the ResultSort of SS).o) by A15,A18, FUNCT_1:23; then (Den(o,MA)).p in xx.i by MSUALG_1:def 7; hence v in Y by A25,A29,FUNCT_1:70; end; hence v in B.i by A23,A24,A27,CANTOR_1:10; end; hence B is_closed_on o by A19,A20,MSUALG_2:def 6; end; begin :: Relationships between Subsets Families definition let I be set, M be ManySortedSet of I, B be SubsetFamily of M, A be SubsetFamily of M; pred A is_finer_than B means :Def1: for a be set st a in A ex b be set st b in B & a c= b; reflexivity; pred B is_coarser_than A means :Def2: for b be set st b in B ex a be set st a in A & a c= b; reflexivity; end; theorem for I be set, M be ManySortedSet of I for A,B,C be SubsetFamily of M holds A is_finer_than B & B is_finer_than C implies A is_finer_than C proof let I be set, M be ManySortedSet of I; let A,B,C be SubsetFamily of M; assume that A1: A is_finer_than B and A2: B is_finer_than C; let a be set; assume a in A; then consider b be set such that A3: b in B and A4: a c= b by A1,Def1; consider c be set such that A5: c in C and A6: b c= c by A2,A3,Def1; take c; thus thesis by A4,A5,A6,XBOOLE_1:1; end; theorem for I be set, M be ManySortedSet of I for A,B,C be SubsetFamily of M holds A is_coarser_than B & B is_coarser_than C implies A is_coarser_than C proof let I be set, M be ManySortedSet of I; let A,B,C be SubsetFamily of M; 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,Def2; consider c be set such that A5: c in C and A6: c c= b by A2,A3,Def2; take c; thus thesis by A4,A5,A6,XBOOLE_1:1; end; definition let I be non empty set, M be ManySortedSet of I; func supp M -> set means :Def3: it = { x where x is Element of I : M.x <> {} }; correctness; end; theorem for I be non empty set, M be non-empty ManySortedSet of I holds M = [0]I +* (M|supp M) proof let I be non empty set, M be non-empty ManySortedSet of I; set MM = M|supp M; A1: dom M = I by PBOOLE:def 3; supp M = I proof thus for v be set st v in supp M holds v in I proof let v be set; assume v in supp M; then v in { x where x is Element of I : M.x <> {} } by Def3; then consider x be Element of I such that A2: v = x and M.x <> {}; thus thesis by A2; end; thus for v be set st v in I holds v in supp M proof let v be set; assume A3: v in I; then M.v <> {} by PBOOLE:def 16; then v in { x where x is Element of I : M.x <> {} } by A3; hence thesis by Def3; end; end; then MM = M by A1,RELAT_1:97; hence thesis by Th1; end; theorem for I be non empty set, M1, M2 be non-empty ManySortedSet of I holds supp M1 = supp M2 & M1|supp M1 = M2|supp M2 implies M1 = M2 proof let I be non empty set, M1, M2 be non-empty ManySortedSet of I; assume that supp M1 = supp M2 and A1: M1|supp M1 = M2|supp M2; A2: dom M1 = I & dom M2 = I by PBOOLE:def 3; for x be set st x in I holds M1.x = M2.x proof let x be set; assume A3: x in I; then M1.x is non empty by PBOOLE:def 16; then x in { a where a is Element of I : M1.a <> {} } by A3; then A4: x in supp M1 by Def3; M2.x is non empty by A3,PBOOLE:def 16; then x in { a where a is Element of I : M2.a <> {} } by A3; then A5: x in supp M2 by Def3; dom (M1|supp M1) = dom M1 /\ supp M1 & dom (M2|supp M2) = dom M2 /\ supp M2 by RELAT_1:90; then A6: x in dom (M1|supp M1) & x in dom (M2|supp M2) by A2,A3,A4,A5,XBOOLE_0:def 3; then M1.x = (M2|supp M2).x by A1,FUNCT_1:70 .= M2.x by A6,FUNCT_1:70; hence thesis; end; hence M1 = M2 by A2,FUNCT_1:9; end; theorem for I be non empty set, M be ManySortedSet of I, x be Element of I holds (not x in supp M) implies M.x = {} proof let I be non empty set, M be ManySortedSet of I, x be Element of I; assume not x in supp M; then not x in { v where v is Element of I : M.v <> {} } by Def3; hence thesis; end; theorem Th9: 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 locally-finite & supp 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 = [0]I +* N; A2: dom N = {i} & rng N = {{y}} by FUNCOP_1:14,19; then A3: i in dom N by TARSKI:def 1; then A4: N.i = {y} by A2,FUNCOP_1:13; then A5: A.i = {y} by A3,FUNCT_4:14; A6: dom A = dom [0]I \/ dom N by FUNCT_4:def 1 .= I \/ {i} by A2,PBOOLE:def 3 .= I by ZFMISC_1:46; then reconsider A as ManySortedSet of I by PBOOLE:def 3; for j be set st j in I holds A.j c= M.j proof let j be set such that A7: j in I; per cases; suppose A8: i = j; let v be set; assume A9: v in A.j; reconsider x as ManySortedSubset of M; x c= M by MSUALG_2:def 1; then A10: x.j c= M.j by A7,PBOOLE:def 5; v in {y} by A3,A4,A8,A9,FUNCT_4:14; then v in x.j by A1,A8,TARSKI:def 1; hence thesis by A10; suppose i <> j; then A11: not j in {i} by TARSKI:def 1; j in dom [0]I \/ dom N by A6,A7,FUNCT_4:def 1; then A.j = ([0]I).j by A2,A11,FUNCT_4:def 1 .= (I --> {}).j by PBOOLE:def 6 .= {} by A7,FUNCOP_1:13; hence thesis by XBOOLE_1:2; end; then A c= M by PBOOLE:def 5; then reconsider AA = A as ManySortedSubset of M by MSUALG_2:def 1; reconsider a = AA as Element of Bool M by CLOSURE2:def 1; take a; A12: for j be set st j in I holds a.j is finite proof let j be set such that A13: j in I; per cases; suppose j = i; hence thesis by A3,A4,FUNCT_4:14; suppose j <> i; then A14: not j in {i} by TARSKI:def 1; j in dom [0]I \/ dom N by A6,A13,FUNCT_4:def 1; then a.j = ([0]I).j by A2,A14,FUNCT_4:def 1 .= (I --> {}).j by PBOOLE:def 6 .= {} by A13,FUNCOP_1:13; hence thesis; end; A15: { 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 set; assume A16: s in { b where b is Element of I : a.b <> {}}; assume A17: not s in {i}; consider b be Element of I such that A18: s = b and A19: a.b <> {} by A16; reconsider s as Element of I by A18; s in dom a by A6; then s in dom [0]I \/ dom N by FUNCT_4:def 1; then a.s = ([0]I).s by A2,A17,FUNCT_4:def 1 .= (I --> {}).s by PBOOLE:def 6 .= {} by FUNCOP_1:13; hence contradiction by A18,A19; end; let s be set; assume A20: s in {i}; then A21: s = i by TARSKI:def 1; reconsider s as Element of I by A20,TARSKI:def 1; a.s = {y} by A3,A4,A21,FUNCT_4:14; hence thesis; end; for j be set st j in I holds a.j c= x.j proof let j be set such that A22: j in I; per cases; suppose A23: i = j; let v be set; assume A24: v in a.j; a.j = {y} by A3,A4,A23,FUNCT_4:14; hence thesis by A1,A23,A24,TARSKI:def 1; suppose j <> i; then A25: not j in {i} by TARSKI:def 1; j in dom [0]I \/ dom N by A6,A22,FUNCT_4:def 1; then a.j = ([0]I).j by A2,A25,FUNCT_4:def 1 .= (I --> {}).j by PBOOLE:def 6 .= {} by A22,FUNCOP_1:13; hence thesis by XBOOLE_1:2; end; hence thesis by A5,A12,A15,Def3,PBOOLE:def 5,PRE_CIRC:def 3,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 :Def4: 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[set, set] means $2 = union { f.$1 where f is Element of Bool M: f in A }; A1: for x,y1,y2 be set st x in I & P[x,y1] & P[x,y2] holds y1 = y2; A2: for x be set st x in I ex y be set st P[x,y]; consider IT be Function such that A3: dom IT = I and A4: for x be set st x in I holds P[x, IT.x] from FuncEx(A1,A2); reconsider IT as ManySortedSet of I by A3,PBOOLE:def 3; for i be set st i in I holds IT.i c= M.i proof let i be set such that A5: i in I; for x be set holds x in IT.i implies x in M.i proof let x be set; assume A6: x in IT.i; IT.i = union { f.i where f is Element of Bool M: f in A } by A4,A5 ; then consider Y be set such that A7: x in Y and A8: Y in { f.i where f is Element of Bool M: f in A } by A6,TARSKI:def 4; consider ff be Element of Bool M such that A9: ff.i = Y and ff in A by A8; reconsider ff as ManySortedSubset of M; ff c= M by MSUALG_2:def 1; then ff.i c= M.i by A5,PBOOLE:def 5; hence thesis by A7,A9; end; hence IT.i c= M.i by TARSKI:def 3; end; then IT c= M by PBOOLE:def 5; then reconsider IT as ManySortedSubset of M by MSUALG_2:def 1; take IT; thus thesis by A4; end; uniqueness proof let B1,B2 be ManySortedSubset of M; assume that A10: 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 A11: 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 set st i in I holds B1.i = B2.i proof let i be set; assume A12: i in I; then B1.i = union { f.i where f is Element of Bool M : f in A } by A10 .= B2.i by A11,A12; hence thesis; end; hence thesis by PBOOLE:3; end; end; definition let I be set, M be ManySortedSet of I; let B be non empty SubsetFamily of M; redefine mode Element of B -> ManySortedSet of I; coherence proof let x be set; assume x is Element of B; hence thesis; end; end; definition let I be set, M be ManySortedSet of I, A be empty SubsetFamily of M; cluster MSUnion A -> empty-yielding; coherence proof set MA = MSUnion A; let i be set; assume i in I; then A1: MA.i = union {f.i where f is Element of Bool M : f in A} by Def4; assume MA.i is non empty; then consider v being set such that A2: v in MA.i by XBOOLE_0:def 1; 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; consider g be Element of Bool M such that h = g.i and A4: g in A by A3; thus contradiction by A4; 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 set st i in I holds (MSUnion A).i = UA.i proof let i be set; assume A2: i in I; then A3: AA.i = { g.i where g is Element of Bool M : g in A } by A1,CLOSURE2:15; UA.i = union (AA.i) by A2,MBOOLEAN:def 2; hence thesis by A2,A3,Def4; end; hence thesis by PBOOLE:3; suppose A4: A is empty SubsetFamily of M; for A be empty SubsetFamily of M holds MSUnion A is empty-yielding; then A5: MSUnion A is empty-yielding by A4; for i be set st i in I holds (MSUnion A).i = UA.i proof let i be set; assume A6: i in I; AA = [0]I by A4,CLOSURE2:def 4; then UA = [0]I by MBOOLEAN:22; then UA.i is empty by A6,PBOOLE:def 15; hence thesis by A5,A6,PBOOLE:def 15; end; hence thesis by PBOOLE:3; 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) = 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 set st i in I holds MAB.i = (MA \/ MB).i proof let i be set; assume A1: i in I; then A2: MAB.i = union {f.i where f is Element of Bool M : f in (A \/ B)} by Def4; A3: (MA \/ MB).i = MA.i \/ MB.i by A1,PBOOLE:def 7; A4: MA.i = union {f.i where f is Element of Bool M : f in A } by A1,Def4; A5: MB.i = union {f.i where f is Element of Bool M : f in B } by A1,Def4; A6: for v be set holds v in MAB.i implies v in (MA \/ MB).i proof let v be set; assume v in MAB.i; then consider h be set such that A7: v in h and A8: 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 A9: h = g.i and A10: g in (A \/ B) by A8; g in A or g in B by A10,XBOOLE_0:def 2; 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 A9; 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 A7,TARSKI:def 4; hence v in (MA \/ MB).i by A3,A4,A5,XBOOLE_0:def 2; end; for v be set holds v in (MA \/ MB).i implies v in MAB.i proof let v be set; assume v in (MA \/ MB).i; then A11: v in MA.i or v in MB.i by A3,XBOOLE_0:def 2; per cases by A1,A11,Def4; suppose v in union { f.i where f is Element of Bool M : f in A}; then consider g be set such that A12: v in g and A13: 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 A14: g = h.i and A15: h in A by A13; h in A \/ B by A15,XBOOLE_0:def 2; then g in { f.i where f is Element of Bool M : f in (A \/ B)} by A14; hence thesis by A2,A12,TARSKI:def 4; suppose v in union { f.i where f is Element of Bool M : f in B}; then consider g be set such that A16: v in g and A17: 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 A18: g = h.i and A19: h in B by A17; h in A \/ B by A19,XBOOLE_0:def 2; then g in { f.i where f is Element of Bool M : f in (A \/ B)} by A18; hence thesis by A2,A16,TARSKI:def 4; end; hence thesis by A6,TARSKI:2; end; hence thesis by PBOOLE:3; 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; assume A1: A c= B; 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 set st i in I holds MA.i c= MB.i proof let i be set such that A2: i in I; for v be set st v in MA.i holds v in MB.i proof let v be set such that A3: v in MA.i; MA.i = union {f.i where f is Element of Bool M : f in A} by A2,Def4; 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; consider g be Element of Bool M such that A6: h = g.i and A7: g in A by A5; h in {k.i where k is Element of Bool M : k in B} by A1,A6,A7; 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,Def4; end; hence MA.i c= MB.i by TARSKI:def 3; end; hence thesis by PBOOLE:def 5; 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:5; 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 set st i in I holds MAB.i c= (MA /\ MB).i proof let i be set; assume A1: i in I; then A2: MAB.i = union {f.i where f is Element of Bool M : f in (A /\ B)} by Def4; A3: MA.i = union {f.i where f is Element of Bool M : f in A } by A1,Def4; A4: MB.i = union {f.i where f is Element of Bool M : f in B } by A1,Def4; for v be set st v in MAB.i holds v in (MA /\ MB).i proof let v be set; assume v in MAB.i; then consider w be set such that A5: v in w and A6: w 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 A7: w = g.i and A8: g in A /\ B by A6; g in A & g in B by A8,XBOOLE_0:def 3; then w in {f.i where f is Element of Bool M : f in A } & w in {f.i where f is Element of Bool M : f in B } by A7; then v in union {f.i where f is Element of Bool M : f in A } & v in union {f.i where f is Element of Bool M : f in B } by A5,TARSKI:def 4; then v in (MA.i /\ MB.i) by A3,A4,XBOOLE_0:def 3; hence thesis by A1,PBOOLE:def 8; end; hence thesis by TARSKI:def 3; end; hence thesis by PBOOLE:def 5; 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; thus MSUnion B c= MSUnion A proof for i be set st i in I holds (MSUnion B).i c= (MSUnion A).i proof let i be set such that A4: i in I; now let a be set; 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,Def4; 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,Def4; 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,Def4; end; end; hence (MSUnion B).i c= (MSUnion A).i by TARSKI:def 3; end; hence thesis by PBOOLE:def 5; end; for i be set st i in I holds (MSUnion A).i c= (MSUnion B).i proof let i be set such that A15: i in I; let a be set; a in (MSUnion A).i implies a in (MSUnion B).i proof assume a in (MSUnion A).i; then a in union { f.i where f is Element of Bool M: f in A} by A15,Def4; then consider Y be set such that A16: a in Y and A17: 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 A18: f.i = Y and A19: f in A by A17; consider c be set such that A20: f in c and A21: c in AA by A3,A19,TARSKI:def 4; reconsider c as SubsetFamily of M by A1,A21; A22: (MSUnion c).i = union {v.i where v is Element of Bool M: v in c} by A15,Def4; f.i in {v.i where v is Element of Bool M: v in c} by A20; then A23: a in union {v.i where v is Element of Bool M: v in c} by A16,A18,TARSKI:def 4; A24: MSUnion c in { MSUnion X where X is SubsetFamily of M : X in AA } by A21; consider cos be set such that A25: a in cos and A26: cos = (MSUnion c).i by A22,A23; cos in { t.i where t is Element of Bool M : t in B} by A2,A24,A26; then a in union { t.i where t is Element of Bool M : t in B} by A25,TARSKI:def 4; hence thesis by A15,Def4; end; hence thesis; end; hence thesis by PBOOLE:def 5; 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 locally-finite & supp a is finite & a c= x} & x = MSUnion A; end; definition let I be non empty set, M be ManySortedSet of I; cluster algebraic reflexive monotonic idempotent 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 locally-finite & supp a is finite & a c= x}; A c= Bool M proof let v be set; assume v in A; then consider a be Element of Bool M such that A1: v = f.a and a is locally-finite & supp a is finite & a c= x; thus v in Bool M by A1; end; then reconsider A as SubsetFamily of M; take A; thus A = { f.a where a is Element of Bool M : a is locally-finite & supp a is finite & a c= x}; thus x c= MSUnion A proof let i be set such that A2: i in I; let y be set such that A3: y in x.i; consider a be Element of Bool M such that A4: y in a.i & a is locally-finite & supp a is finite & a c= x by A2,A3,Th9; a = f.a by FUNCT_1:35; then a in A by A4; 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 A4,TARSKI:def 4; hence thesis by A2,Def4; end; thus MSUnion A c= x proof let i be set such that A5: i in I; for v be set holds v in (MSUnion A).i implies v in x.i proof let v be set; assume v in (MSUnion A).i; then v in union {ff.i where ff is Element of Bool M: ff in A} by A5,Def4; then consider Y be set such that A6: v in Y and A7: 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 A8: Y = ff.i and A9: ff in A by A7; consider a be Element of Bool M such that A10: ff = f.a and A11: a is locally-finite & supp a is finite & a c= x by A9; ff = a by A10,FUNCT_1:35; then ff.i c= x.i by A5,A11,PBOOLE:def 5; hence thesis by A6,A8; end; hence thesis by TARSKI:def 3; end; end; thus f is reflexive proof let X be Element of Bool M; thus thesis by FUNCT_1:35; end; thus f is monotonic proof let X, Y be Element of Bool M such that A12: X c= Y; f.X = X & f.Y = Y by FUNCT_1:35; hence thesis by A12; end; thus f is idempotent proof let X be Element of Bool M; thus f.(f.X) = f.X by FUNCT_1:35; end; 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 :Def7: the Sorts of it = the Sorts of MA & the Family of it = SubSort MA; existence proof A1: SubSort MA c= Bool the Sorts of MA proof let x be set; assume x in SubSort MA; then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 12; hence x in Bool the Sorts of MA by CLOSURE2:def 1; end; reconsider SS = the Sorts of MA as ManySortedSet of the carrier of the 1-sorted of S; reconsider SF = SubSort MA as SubsetFamily of SS by A1; take ClosureStr (#SS, SF#); thus thesis; end; uniqueness; end; canceled; theorem Th16: 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 set; assume x in SubSort MA; then x is ManySortedSubset of the Sorts of MA by MSUALG_2:def 12; hence x in Bool the Sorts of MA 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 let F be SubsetFamily of the Sorts of MA such that A1: F c= SUBMA; set I = the carrier of S; set x = meet |:F:|; set M = bool (Union (the Sorts of MA)); A2: dom x = I by PBOOLE:def 3; rng x c= M proof let u be set; assume u in rng x; then consider i be set such that A3: i in dom x and A4: u = x.i by FUNCT_1:def 5; consider Q be Subset-Family of (the Sorts of MA).i such that Q = |:F:|.i and A5: u = Intersect Q by A2,A3,A4,MSSUBFAM:def 2; dom (the Sorts of MA) = I by PBOOLE:def 3; then (the Sorts of MA).i in rng (the Sorts of MA) by A2,A3,FUNCT_1:def 5; then (the Sorts of MA).i c= union rng (the Sorts of MA) by ZFMISC_1:92 ; 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 thesis by PROB_1:def 3; 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 12; end; hence thesis by CLOSURE2:def 8; end; definition 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 A1: the Sorts of SubAlgCl MA = the Sorts of MA by Def7; set F = the Family of SubAlgCl MA; reconsider SF = SubSort MA as absolutely-multiplicative SubsetFamily of the Sorts of MA by Th16; F = SF by Def7; hence thesis by A1,CLOSURE2:def 19; end; end; end; definition let S be non void non empty ManySortedSign, MA be strict non-empty MSAlgebra over S; cluster SubAlgCl MA -> algebraic; coherence proof 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 locally-finite & supp a is finite & a c= x}; A c= Bool M proof let v be set; assume v in A; then consider a be Element of Bool M such that A2: v = SS.a and a is locally-finite & supp a is finite & a c= x; reconsider vv = v as Element of Bool M by A2; vv in Bool M; hence thesis; end; then reconsider A as SubsetFamily of M; take A; reconsider I = the carrier of S as non empty set; thus A = { SS.b where b is Element of Bool M : b is locally-finite & supp b is finite & b c= x}; thus x c= MSUnion A proof for i be set st i in I holds x.i c= (MSUnion A).i proof let i be set such that A3: i in I; let v be set such that A4: v in x.i; consider b be Element of Bool M such that A5: v in b.i and A6: b is locally-finite & supp b is finite & b c= x by A3,A4,Th9; A7: SS.b in A by A6; reconsider SS' = SS as reflexive SetOp of M; b c=' SS'.b by CLOSURE2:def 12; then A8: b.i c= (SS'.b).i by A3,PBOOLE:def 5; (SS'.b).i in {f.i where f is Element of Bool M : f in A} by A7; then v in union {f.i where f is Element of Bool M : f in A} by A5,A8,TARSKI:def 4; hence v in (MSUnion A).i by A3,Def4; end; hence thesis by PBOOLE:def 5; end; thus MSUnion A c= x proof for i be set st i in I holds (MSUnion A).i c= x.i proof let i be set such that A9: i in I; for v be set holds v in (MSUnion A).i implies v in x.i proof let v be set; assume v in (MSUnion A).i; then v in union {ff.i where ff is Element of Bool M: ff in A} by A9,Def4; then consider Y be set such that A10: v in Y and A11: 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 A12: Y = ff.i and A13: ff in A by A11; consider a be Element of Bool M such that A14: ff = SS.a and a is locally-finite & supp a is finite and A15: a c=' x by A13; reconsider SS' = SS as monotonic SetOp of M; SS'.a c=' SS'.x by A15,CLOSURE2:def 13; then ff.i c= x.i by A1,A9,A14,PBOOLE:def 5; hence thesis by A10,A12; end; hence (MSUnion A).i c= x.i by TARSKI:def 3; end; hence thesis by PBOOLE:def 5; end; end; end;

Back to top