let I be 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
let M be 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 AA be set ; ( ( 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
; 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; ( 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
; MSUnion B = MSUnion A
let i be object ; PBOOLE:def 10 ( not i in I or (MSUnion B) . i = (MSUnion A) . i )
assume A4:
i in I
; (MSUnion B) . i = (MSUnion A) . i
thus
(MSUnion B) . i c= (MSUnion A) . i
XBOOLE_0:def 10 (MSUnion A) . i c= (MSUnion B) . iproof
let a be
object ;
TARSKI:def 3 ( not a in (MSUnion B) . i or a in (MSUnion A) . i )
thus
(
a in (MSUnion B) . i implies
a in (MSUnion A) . i )
verumproof
assume
a in (MSUnion B) . i
;
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;
verum
end;
end;
let a be object ; TARSKI:def 3 ( not a in (MSUnion A) . i or a in (MSUnion B) . i )
assume
a in (MSUnion A) . i
; 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; verum