let f be Function; :: thesis: ( dom f is subset-closed & dom f is d.union-closed & f is d.union-distributive implies for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b ) )

assume A1: dom f is subset-closed ; :: thesis: ( not dom f is d.union-closed or not f is d.union-distributive or for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b ) )

assume that

A2: dom f is d.union-closed and

AA: f is d.union-distributive ; :: thesis: for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b )

reconsider C = dom f as subset-closed d.union-closed set by A1, A2;

let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex b being set st

( b is finite & b c= a & y in f . b ) )

assume that

A3: a in dom f and

A4: y in f . a ; :: thesis: ex b being set st

( b is finite & b c= a & y in f . b )

reconsider A = { b where b is Subset of a : b is finite } as set ;

A5: A is c=directed

then consider B being set such that

A11: y in B and

A12: B in f .: A by A4, A7, TARSKI:def 4;

consider b being object such that

b in dom f and

A13: b in A and

A14: B = f . b by A12, FUNCT_1:def 6;

reconsider bb = b as set by TARSKI:1;

take bb ; :: thesis: ( bb is finite & bb c= a & y in f . bb )

ex c being Subset of a st

( b = c & c is finite ) by A13;

hence ( bb is finite & bb c= a & y in f . bb ) by A11, A14; :: thesis: verum

ex b being set st

( b is finite & b c= a & y in f . b ) )

assume A1: dom f is subset-closed ; :: thesis: ( not dom f is d.union-closed or not f is d.union-distributive or for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b ) )

assume that

A2: dom f is d.union-closed and

AA: f is d.union-distributive ; :: thesis: for a, y being set st a in dom f & y in f . a holds

ex b being set st

( b is finite & b c= a & y in f . b )

reconsider C = dom f as subset-closed d.union-closed set by A1, A2;

let a, y be set ; :: thesis: ( a in dom f & y in f . a implies ex b being set st

( b is finite & b c= a & y in f . b ) )

assume that

A3: a in dom f and

A4: y in f . a ; :: thesis: ex b being set st

( b is finite & b c= a & y in f . b )

reconsider A = { b where b is Subset of a : b is finite } as set ;

A5: A is c=directed

proof

A7:
union A = a
let Y be finite Subset of A; :: according to COHSP_1:def 4 :: thesis: ex b_{1} being set st

( union Y c= b_{1} & b_{1} in A )

take union Y ; :: thesis: ( union Y c= union Y & union Y in A )

hence ( union Y c= union Y & union Y in A ) by A6; :: thesis: verum

end;( union Y c= b

take union Y ; :: thesis: ( union Y c= union Y & union Y in A )

now :: thesis: for x being set st x in Y holds

x c= a

then A6:
union Y c= a
by ZFMISC_1:76;x c= a

let x be set ; :: thesis: ( x in Y implies x c= a )

assume x in Y ; :: thesis: x c= a

then x in A ;

then ex c being Subset of a st

( x = c & c is finite ) ;

hence x c= a ; :: thesis: verum

end;assume x in Y ; :: thesis: x c= a

then x in A ;

then ex c being Subset of a st

( x = c & c is finite ) ;

hence x c= a ; :: thesis: verum

now :: thesis: for b being set st b in Y holds

b is finite

then
union Y is finite
by FINSET_1:7;b is finite

let b be set ; :: thesis: ( b in Y implies b is finite )

assume b in Y ; :: thesis: b is finite

then b in A ;

then ex c being Subset of a st

( b = c & c is finite ) ;

hence b is finite ; :: thesis: verum

end;assume b in Y ; :: thesis: b is finite

then b in A ;

then ex c being Subset of a st

( b = c & c is finite ) ;

hence b is finite ; :: thesis: verum

hence ( union Y c= union Y & union Y in A ) by A6; :: thesis: verum

proof

A10:
A c= C
thus
union A c= a
:: according to XBOOLE_0:def 10 :: thesis: a c= union A

assume x in a ; :: thesis: x in union A

then {x} c= a by ZFMISC_1:31;

then ( x in {x} & {x} in A ) by TARSKI:def 1;

hence x in union A by TARSKI:def 4; :: thesis: verum

end;proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in union A )
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union A or x in a )

assume x in union A ; :: thesis: x in a

then consider b being set such that

A8: x in b and

A9: b in A by TARSKI:def 4;

ex c being Subset of a st

( b = c & c is finite ) by A9;

hence x in a by A8; :: thesis: verum

end;assume x in union A ; :: thesis: x in a

then consider b being set such that

A8: x in b and

A9: b in A by TARSKI:def 4;

ex c being Subset of a st

( b = c & c is finite ) by A9;

hence x in a by A8; :: thesis: verum

assume x in a ; :: thesis: x in union A

then {x} c= a by ZFMISC_1:31;

then ( x in {x} & {x} in A ) by TARSKI:def 1;

hence x in union A by TARSKI:def 4; :: thesis: verum

proof

f . (union A) = union (f .: A)
by A3, A7, A5, A10, AA, COHSP_1:def 10;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in A or x in C )

assume x in A ; :: thesis: x in C

then ex b being Subset of a st

( x = b & b is finite ) ;

hence x in C by A3, CLASSES1:def 1; :: thesis: verum

end;assume x in A ; :: thesis: x in C

then ex b being Subset of a st

( x = b & b is finite ) ;

hence x in C by A3, CLASSES1:def 1; :: thesis: verum

then consider B being set such that

A11: y in B and

A12: B in f .: A by A4, A7, TARSKI:def 4;

consider b being object such that

b in dom f and

A13: b in A and

A14: B = f . b by A12, FUNCT_1:def 6;

reconsider bb = b as set by TARSKI:1;

take bb ; :: thesis: ( bb is finite & bb c= a & y in f . bb )

ex c being Subset of a st

( b = c & c is finite ) by A13;

hence ( bb is finite & bb c= a & y in f . bb ) by A11, A14; :: thesis: verum