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 object ; :: 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

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

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 object ; :: 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 object ; :: according to TARSKI:def 3 :: thesis: ( not a in (MSUnion A) . i or a in (MSUnion B) . i )
let a be object ; :: 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

end;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;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

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