let I be set ; :: thesis: for A being V8() ManySortedSet of I st A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) holds
union A is V39()
let A be V8() ManySortedSet of I; :: thesis: ( A is V39() & ( for M being ManySortedSet of I st M in A holds
M is V39() ) implies union A is V39() )
assume that
A1: A is V39() and
A2: for M being ManySortedSet of I st M in A holds
M is V39() ; :: thesis: union A is V39()
let i be object ; :: according to FINSET_1:def 5 :: thesis: ( not i in I or (union A) . i is finite )
assume A3: i in I ; :: thesis: (union A) . i is finite
A4: for X9 being set st X9 in A . i holds
X9 is finite
proof
consider M being ManySortedSet of I such that
A5: M in A by PBOOLE:134;
let X9 be set ; :: thesis: ( X9 in A . i implies X9 is finite )
assume A6: X9 in A . i ; :: thesis: X9 is finite
dom (M +* (i .--> X9)) = I by A3, PZFMISC1:1;
then reconsider K = M +* (i .--> X9) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A7: dom (i .--> X9) = {i} ;
i in {i} by TARSKI:def 1;
then A8: K . i = (i .--> X9) . i by A7, FUNCT_4:13
.= X9 by FUNCOP_1:72 ;
K in A
proof
let j be object ; :: according to PBOOLE:def 1 :: thesis: ( not j in I or K . j in A . j )
assume A9: j in I ; :: thesis: K . j in A . j
now :: thesis: ( ( j = i & K . j in A . j ) or ( j <> i & K . j in A . j ) )
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: K . j in A . j
hence K . j in A . j by A6, A8; :: thesis: verum
end;
case j <> i ; :: thesis: K . j in A . j
then not j in dom (i .--> X9) by TARSKI:def 1;
then K . j = M . j by FUNCT_4:11;
hence K . j in A . j by A5, A9; :: thesis: verum
end;
end;
end;
hence K . j in A . j ; :: thesis: verum
end;
then K is V39() by A2;
hence X9 is finite by A8; :: thesis: verum
end;
A . i is finite by A1;
then union (A . i) is finite by A4, FINSET_1:7;
hence (union A) . i is finite by A3, MBOOLEAN:def 2; :: thesis: verum