let I be set ; for A being V2() V26() ManySortedSet of I st ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) holds
union A in A
let A be V2() V26() ManySortedSet of I; ( ( for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X ) implies union A in A )
assume A1:
for X, Y being ManySortedSet of I st X in A & Y in A & not X c= Y holds
Y c= X
; union A in A
let i be object ; PBOOLE:def 1 ( not i in I or (union A) . i in A . i )
assume A2:
i in I
; (union A) . i in A . i
then
i in dom A
by PARTFUN1:def 2;
then
A . i in rng A
by FUNCT_1:3;
then A3:
A . i is finite
by FINSET_1:def 2;
A4:
for X9, Y9 being set st X9 in A . i & Y9 in A . i & not X9 c= Y9 holds
Y9 c= X9
proof
let X9,
Y9 be
set ;
( X9 in A . i & Y9 in A . i & not X9 c= Y9 implies Y9 c= X9 )
assume that A5:
X9 in A . i
and A6:
Y9 in A . i
;
( X9 c= Y9 or Y9 c= X9 )
consider M being
ManySortedSet of
I such that A7:
M in A
by PBOOLE:134;
(
dom (M +* (i .--> Y9)) = I &
dom (M +* (i .--> X9)) = I )
by A2, Lm1;
then reconsider K1 =
M +* (i .--> X9),
K2 =
M +* (i .--> Y9) as
ManySortedSet of
I by PARTFUN1:def 2, RELAT_1:def 18;
assume A8:
not
X9 c= Y9
;
Y9 c= X9
A9:
i in {i}
by TARSKI:def 1;
dom (i .--> Y9) = {i}
;
then A11:
K2 . i =
(i .--> Y9) . i
by A9, FUNCT_4:13
.=
Y9
by FUNCOP_1:72
;
A12:
K2 in A
dom (i .--> X9) = {i}
;
then A15:
K1 . i =
(i .--> X9) . i
by A9, FUNCT_4:13
.=
X9
by FUNCOP_1:72
;
K1 in A
then
(
K1 c= K2 or
K2 c= K1 )
by A1, A12;
hence
Y9 c= X9
by A2, A8, A15, A11;
verum
end;
A . i <> {}
by A2, PBOOLE:def 13;
then
union (A . i) in A . i
by A3, A4, CARD_2:62;
hence
(union A) . i in A . i
by A2, Def2; verum