let f be Function; :: thesis: ( dom f is subset-closed & f is union-distributive & dom f is d.union-closed implies for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} ) )
assume A1: dom f is subset-closed ; :: thesis: ( not f is union-distributive or not dom f is d.union-closed or for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} ) )
then reconsider C = dom f as subset-closed set ;
A2: {} is Subset of (dom f) by XBOOLE_1:2;
assume that
A3: f is union-distributive and
AB: dom f is d.union-closed ; :: thesis: for a, y being set st a in dom f & y in f . a holds
ex x being set st
( x in a & y in f . {x} )
let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex x being set st
( x in a & y in f . {x} ) )
assume that
A4: a in dom f and
A5: y in f . a ; :: thesis: ex x being set st
( x in a & y in f . {x} )
consider b being set such that
b is finite and
A6: b c= a and
A7: y in f . b by A1, A4, A5, Th21, AB, A3;
A9: dom f = C ;
then {} in dom f by A4, CLASSES1:def 1, XBOOLE_1:2;
then f . {} = union (f .: {}) by A3, A2, ZFMISC_1:2, COHSP_1:def 9
.= {} by ZFMISC_1:2 ;
then reconsider b = b as non empty set by A7;
reconsider A = { {x} where x is Element of b : verum } as set ;
A10: b in dom f by A4, A6, A9, CLASSES1:def 1;
A11: A c= dom f
proof
let X be object ; :: according to TARSKI:def 3 :: thesis: ( not X in A or X in dom f )
reconsider xx = X as set by TARSKI:1;
assume X in A ; :: thesis: X in dom f
then ex x being Element of b st X = {x} ;
hence X in dom f by A9, A10, CLASSES1:def 1; :: thesis: verum
end;
now :: thesis: for X being set st X in A holds
X c= b
let X be set ; :: thesis: ( X in A implies X c= b )
assume X in A ; :: thesis: X c= b
then ex x being Element of b st X = {x} ;
hence X c= b ; :: thesis: verum
end;
then A12: union A in dom f by A9, A10, CLASSES1:def 1, ZFMISC_1:76;
reconsider A = A as Subset of (dom f) by A11;
b c= union A
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in b or x in union A )
assume x in b ; :: thesis: x in union A
then {x} in A ;
then {x} c= union A by ZFMISC_1:74;
hence x in union A by ZFMISC_1:31; :: thesis: verum
end;
then A13: f . b c= f . (union A) by A3, A10, A12, COHSP_1:def 11;
f . (union A) = union (f .: A) by A3, A12, COHSP_1:def 9;
then consider Y being set such that
A14: y in Y and
A15: Y in f .: A by A7, A13, TARSKI:def 4;
consider X being object such that
X in dom f and
A16: X in A and
A17: Y = f . X by A15, FUNCT_1:def 6;
reconsider X = X as set by A16;
consider x being Element of b such that
A18: X = {x} by A16;
reconsider x = x as set ;
take x ; :: thesis: ( x in a & y in f . {x} )
x in b ;
hence x in a by A6; :: thesis: y in f . {x}
thus y in f . {x} by A14, A17, A18; :: thesis: verum