let I be set ; :: thesis: for M being ManySortedSet of I
for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let M be ManySortedSet of I; :: thesis: for X being Element of bool M
for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let X be Element of bool M; :: thesis: for i, x being set st i in I & x in ((id (bool M)) .. X) . i holds
ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
let i, x be set ; :: thesis: ( i in I & x in ((id (bool M)) .. X) . i implies ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i ) )
assume that
A1: i in I and
A2: x in ((id (bool M)) .. X) . i ; :: thesis: ex Y being finite-yielding Element of bool M st
( Y c= X & x in ((id (bool M)) .. Y) . i )
A3: x in X . i by A2, Th8;
set Y = (I --> {}) +* (i .--> {x});
dom ((I --> {}) +* (i .--> {x})) = I by A1, PZFMISC1:1;
then reconsider Y = (I --> {}) +* (i .--> {x}) as ManySortedSet of I by PARTFUN1:def 2, RELAT_1:def 18;
A4: dom (i .--> {x}) = {i} ;
i in {i} by TARSKI:def 1;
then A5: Y . i = (i .--> {x}) . i by A4, FUNCT_4:13
.= {x} by FUNCOP_1:72 ;
X in bool M by MSSUBFAM:12;
then X c= M by MBOOLEAN:18;
then A6: X . i c= M . i by A1;
Y is Element of bool M
proof
let j be object ; :: according to PBOOLE:def 14 :: thesis: ( not j in I or Y . j is Element of (bool M) . j )
assume A7: j in I ; :: thesis: Y . j is Element of (bool M) . j
now :: thesis: ( ( j = i & Y . j is Element of (bool M) . j ) or ( j <> i & Y . j is Element of (bool M) . j ) )
per cases ( j = i or j <> i ) ;
case A8: j = i ; :: thesis: Y . j is Element of (bool M) . j
then {x} c= M . j by A3, A6, ZFMISC_1:31;
hence Y . j is Element of (bool M) . j by A5, A7, A8, MBOOLEAN:def 1; :: thesis: verum
end;
case j <> i ; :: thesis: Y . j is Element of (bool M) . j
then not j in dom (i .--> {x}) by TARSKI:def 1;
then Y . j = (I --> {}) . j by FUNCT_4:11;
then Y . j = {} ;
then Y . j c= M . j ;
hence Y . j is Element of (bool M) . j by A7, MBOOLEAN:def 1; :: thesis: verum
end;
end;
end;
hence Y . j is Element of (bool M) . j ; :: thesis: verum
end;
then reconsider Y = Y as Element of bool M ;
Y is finite-yielding
proof
let j be object ; :: according to FINSET_1:def 5 :: thesis: ( not j in I or Y . j is finite )
assume j in I ; :: thesis: Y . j is finite
now :: thesis: ( ( j = i & Y . j is finite ) or ( j <> i & Y . j is finite ) )
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: Y . j is finite
hence Y . j is finite by A5; :: thesis: verum
end;
end;
end;
hence Y . j is finite ; :: thesis: verum
end;
then reconsider Y = Y as finite-yielding Element of bool M ;
take Y ; :: thesis: ( Y c= X & x in ((id (bool M)) .. Y) . i )
thus Y c= X :: thesis: x in ((id (bool M)) .. Y) . i
proof
let j be object ; :: according to PBOOLE:def 2 :: thesis: ( not j in I or Y . j c= X . j )
assume j in I ; :: thesis: Y . j c= X . j
now :: thesis: ( ( j = i & Y . j c= X . j ) or ( j <> i & Y . j c= X . j ) )
per cases ( j = i or j <> i ) ;
case j = i ; :: thesis: Y . j c= X . j
hence Y . j c= X . j by A3, A5, ZFMISC_1:31; :: thesis: verum
end;
end;
end;
hence Y . j c= X . j ; :: thesis: verum
end;
x in Y . i by A5, TARSKI:def 1;
hence x in ((id (bool M)) .. Y) . i by Th8; :: thesis: verum