let f be Function; :: thesis: ( dom f is subset-closed implies ( f is U-continuous iff ( dom f is d.union-closed & f is c=-monotone & ( 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: ( f is U-continuous iff ( dom f is d.union-closed & f is c=-monotone & ( 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 ) ) ) )

hereby :: thesis: ( dom f is d.union-closed & f is c=-monotone & ( 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 ) ) implies f is U-continuous )

assume A2: f is U-continuous ; :: thesis: ( dom f is d.union-closed & f is c=-monotone & ( for a, y being set st a in dom f & y in f . a holds
ex bb being set st
( bb is finite & bb c= a & y in f . bb ) ) )
hence ( dom f is d.union-closed & f is c=-monotone ) ; :: thesis: for a, y being set st a in dom f & y in f . a holds
ex bb being set st
( bb is finite & bb c= a & y in f . bb )
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 bb being set st
( bb is finite & bb c= a & y in f . bb ) )
assume that
A3: a in dom f and
A4: y in f . a ; :: thesis: ex bb being set st
( bb is finite & bb c= a & y in f . bb )
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 a being set st
( union Y c= a & a 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;

then union A in C by A5, Def6;
then f . (union A) = union (f .: A) by A2, A5, A10, Def10;
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 = 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

end;

assume dom f is d.union-closed ; :: thesis: ( not f is c=-monotone or ex a, y being set st
( a in dom f & y in f . a & ( for b being set holds
( not b is finite or not b c= a or not y in f . b ) ) ) or f is U-continuous )
then reconsider C = dom f as d.union-closed set ;
assume that
A15: for a, b being set st a in dom f & b in dom f & a c= b holds
f . a c= f . b and
A16: 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 ) ; :: according to COHSP_1:def 11 :: thesis: f is U-continuous
C is d.union-closed ;
hence dom f is d.union-closed ; :: according to COHSP_1:def 13 :: thesis: f is d.union-distributive
thus f is d.union-distributive :: thesis: verum

proof

let A be Subset of (dom f); :: according to COHSP_1:def 10 :: thesis: ( A is c=directed & union A in dom f implies f . (union A) = union (f .: A) )
assume that
A17: A is c=directed and
A18: union A in dom f ; :: thesis: f . (union A) = union (f .: A)
reconsider A9 = A as Subset of C ;
thus f . (union A) c= union (f .: A) :: according to XBOOLE_0:def 10 :: thesis: union (f .: A) c= f . (union A)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in f . (union A) or x in union (f .: A) )
assume x in f . (union A) ; :: thesis: x in union (f .: A)
then consider b being set such that
A19: ( b is finite & b c= union A9 ) and
A20: x in f . b by A16, A18;
consider c being set such that
A21: c in A and
A22: b c= c by A17, A19, Th13;
b in C by A1, A21, A22;
then A23: f . b c= f . c by A15, A21, A22;
f . c in f .: A by A21, FUNCT_1:def 6;
hence x in union (f .: A) by A20, A23, TARSKI:def 4; :: thesis: verum

end;

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in union (f .: A) or x in f . (union A) )
assume x in union (f .: A) ; :: thesis: x in f . (union A)
then consider B being set such that
A24: x in B and
A25: B in f .: A by TARSKI:def 4;
ex b being object st
( b in dom f & b in A & B = f . b ) by A25, FUNCT_1:def 6;
then B c= f . (union A9) by A15, A18, ZFMISC_1:74;
hence x in f . (union A) by A24; :: thesis: verum

end;