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

proof

let Y be finite Subset of A; :: according to COHSP_1:def 4 :: thesis: ex b₁ being set st
( union Y c= b₁ & b₁ in A )
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

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;

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

now :: thesis: for b being set st b in Y holds
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;

then union Y is finite by FINSET_1:7;
hence ( union Y c= union Y & union Y in A ) by A6; :: thesis: verum

end;

A7: union A = a

proof

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

proof

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;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in a or x in 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;

A10: A c= C

proof

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;

f . (union A) = union (f .: A) by A3, A7, A5, A10, AA, COHSP_1:def 10;
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