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

reconsider A = A as Subset of (dom f) by A11;

b c= union A

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

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;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

now :: thesis: for X being set st X in A holds

X c= b

then A12:
union A in dom f
by A9, A10, CLASSES1:def 1, ZFMISC_1:76;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;assume X in A ; :: thesis: X c= b

then ex x being Element of b st X = {x} ;

hence X c= b ; :: thesis: verum

reconsider A = A as Subset of (dom f) by A11;

b c= union A

proof

then A13:
f . b c= f . (union A)
by A3, A10, A12, COHSP_1:def 11;
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;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

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