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
for i being set st i in I holds
(MSUnion B) . i c= (MSUnion A) . i
proof
let i be
set ;
( i in I implies (MSUnion B) . i c= (MSUnion A) . i )
assume A4:
i in I
;
(MSUnion B) . i c= (MSUnion A) . i
now let a be
set ;
( a in (MSUnion B) . i implies 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, Def4;
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, Def4;
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, Def4;
verum
end; end;
hence
(MSUnion B) . i c= (MSUnion A) . i
by TARSKI:def 3;
verum
end;
hence
MSUnion B c= MSUnion A
by PBOOLE:def 2; PBOOLE:def 10 MSUnion A c= MSUnion B
for i being set st i in I holds
(MSUnion A) . i c= (MSUnion B) . i
proof
let i be
set ;
( i in I implies (MSUnion A) . i c= (MSUnion B) . i )
assume A15:
i in I
;
(MSUnion A) . i c= (MSUnion B) . i
let a be
set ;
TARSKI:def 3 ( not a in (MSUnion A) . i or a in (MSUnion B) . i )
(
a in (MSUnion A) . i implies
a in (MSUnion B) . i )
proof
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 A15, Def4;
then consider Y being
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 being
Element of
Bool M such that A18:
f . i = Y
and A19:
f in A
by A17;
consider c being
set such that A20:
f in c
and A21:
c in AA
by A3, A19, TARSKI:def 4;
reconsider c =
c as
SubsetFamily of
M by A1, A21;
f . i in { (v . i) where v is Element of Bool M : v in c }
by A20;
then A22:
a in union { (v . i) where v is Element of Bool M : v in c }
by A16, A18, TARSKI:def 4;
(MSUnion c) . i = union { (v . i) where v is Element of Bool M : v in c }
by A15, Def4;
then consider cos being
set such that A23:
a in cos
and A24:
cos = (MSUnion c) . i
by A22;
MSUnion c in { (MSUnion X) where X is SubsetFamily of M : X in AA }
by A21;
then
cos in { (t . i) where t is Element of Bool M : t in B }
by A2, A24;
then
a in union { (t . i) where t is Element of Bool M : t in B }
by A23, TARSKI:def 4;
hence
a in (MSUnion B) . i
by A15, Def4;
verum
end;
hence
( not
a in (MSUnion A) . i or
a in (MSUnion B) . i )
;
verum
end;
hence
MSUnion A c= MSUnion B
by PBOOLE:def 2; verum