let I be set ; :: thesis: for A, X being ManySortedSet of I
for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let A, X be ManySortedSet of I; :: thesis: for B being V2() ManySortedSet of I st X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) holds
X c= union A
let B be V2() ManySortedSet of I; :: thesis: ( X c= union (A \/ B) & ( for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ) implies X c= union A )
assume that
A1: X c= union (A \/ B) and
A2: for Y being ManySortedSet of I st Y in B holds
Y /\ X = [[0]] I ; :: thesis: X c= union A
let i be set ; :: according to PBOOLE:def 5 :: thesis: ( not i in I or X . i c= (union A) . i )
assume A3: i in I ; :: thesis: X . i c= (union A) . i
A4: for Y9 being set st Y9 in B . i holds
Y9 misses X . i
proof
consider M being ManySortedSet of I such that
A5: M in B by PBOOLE:146;
let Y9 be set ; :: thesis: ( Y9 in B . i implies Y9 misses X . i )
assume A6: Y9 in B . i ; :: thesis: Y9 misses X . i
dom (M +* (i .--> Y9)) = I by A3, Lm1;
then reconsider K = M +* (i .--> Y9) as ManySortedSet of I by PARTFUN1:def 4, RELAT_1:def 18;
A7: dom (i .--> Y9) = {i} by FUNCOP_1:19;
i in {i} by TARSKI:def 1;
then A8: K . i = (i .--> Y9) . i by A7, FUNCT_4:14
.= Y9 by FUNCOP_1:87 ;
K in B
proof
let j be set ; :: according to PBOOLE:def 4 :: thesis: ( not j in I or K . j in B . j )
assume A9: j in I ; :: thesis: K . j in B . j
now
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: K . j in B . j
hence K . j in B . j by A6, A8; :: thesis: verum
end;
end;
end;
hence K . j in B . j ; :: thesis: verum
end;
then K /\ X = [[0]] I by A2;
then (K /\ X) . i = {} by PBOOLE:5;
then Y9 /\ (X . i) = {} by A3, A8, PBOOLE:def 8;
hence Y9 misses X . i by XBOOLE_0:def 7; :: thesis: verum
end;
X . i c= (union (A \/ B)) . i by A1, A3, PBOOLE:def 5;
then X . i c= union ((A . i) \/ (B . i)) by A3, Lm6;
then X . i c= union (A . i) by A4, SETFAM_1:57;
hence X . i c= (union A) . i by A3, Def2; :: thesis: verum