let f be Function; :: thesis: ( dom f is subset-closed & dom f is d.union-closed implies ( f is U-linear iff ( f is c=-monotone & ( 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} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ) ) ) )
assume A1: ( dom f is subset-closed & dom f is d.union-closed ) ; :: thesis: ( f is U-linear iff ( f is c=-monotone & ( 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} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ) ) )
then reconsider C = dom f as subset-closed d.union-closed set ;
hereby :: thesis: ( f is c=-monotone & ( 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} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ) implies f is U-linear )
A2: {} is Subset of (dom f) by XBOOLE_1:2;
assume A3: f is U-linear ; :: thesis: ( f is c=-monotone & ( 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} & ( for c being set st c c= a & y in f . c holds
x in c ) ) ) )
hence f is c=-monotone ; :: 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} & ( for c being set st c c= a & y in f . c holds
x in c ) )
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} & ( for c being set st c c= a & y in f . c holds
x in c ) ) )
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} & ( for c being set st c c= a & y in f . c holds
x in c ) )
consider b being set such that
b is finite and
A6: b c= a and
A7: y in f . b and
A8: for c being set st c c= a & y in f . c holds
b c= c by A1, A3, A4, A5, Th22;
A9: dom f = C ;
{} c= a ;
then {} in dom f by A4, A9, CLASSES1:def 1;
then f . {} = union (f .: {}) by A3, A2, Def9, ZFMISC_1:2
.= {} 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} ;
then xx c= b by ZFMISC_1:31;
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 by ZFMISC_1:31; :: thesis: verum
end;
then union A c= b by ZFMISC_1:76;
then A12: union A in dom f by A9, A10, CLASSES1:def 1;
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, Def11;
f . (union A) = union (f .: A) by A3, A12, Def9;
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;
consider x being Element of b such that
A18: X = {x} by A16;
reconsider x = x as set ;
take x = x; :: thesis: ( x in a & y in f . {x} & ( for c being set st c c= a & y in f . c holds
x in c ) )
thus ( x in a & y in f . {x} ) by A6, A14, A17, A18; :: thesis: for c being set st c c= a & y in f . c holds
x in c
let c be set ; :: thesis: ( c c= a & y in f . c implies x in c )
assume ( c c= a & y in f . c ) ; :: thesis: x in c
then ( x in b & b c= c ) by A8;
hence x in c ; :: thesis: verum
end;
assume that
A19: f is c=-monotone and
A20: 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} & ( for b being set st b c= a & y in f . b holds
x in b ) ) ; :: thesis: f is U-linear
now :: 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 & ( for c being set st c c= a & y in f . c holds
b c= c ) )
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 & ( for c being set st c c= a & y in f . c holds
b c= c ) ) )
assume ( a in dom f & y in f . a ) ; :: thesis: ex b being set st
( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) )
then consider x being set such that
A21: ( x in a & y in f . {x} ) and
A22: for b being set st b c= a & y in f . b holds
x in b by A20;
reconsider b = {x} as set ;
take b = b; :: thesis: ( b is finite & b c= a & y in f . b & ( for c being set st c c= a & y in f . c holds
b c= c ) )
thus ( b is finite & b c= a & y in f . b ) by A21, ZFMISC_1:31; :: thesis: for c being set st c c= a & y in f . c holds
b c= c
let c be set ; :: thesis: ( c c= a & y in f . c implies b c= c )
assume ( c c= a & y in f . c ) ; :: thesis: b c= c
then x in c by A22;
hence b c= c by ZFMISC_1:31; :: thesis: verum
end;
hence f is U-stable by A1, A19, Th22; :: according to COHSP_1:def 15 :: thesis: f is union-distributive
thus f is union-distributive :: thesis: verum
proof
let A be Subset of (dom f); :: according to COHSP_1:def 9 :: thesis: ( union A in dom f implies f . (union A) = union (f .: A) )
assume A23: union A in dom f ; :: thesis: f . (union A) = union (f .: A)
thus f . (union A) c= union (f .: A) :: according to XBOOLE_0:def 10 :: thesis: union (f .: A) c= f . (union A)
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f . (union A) or y in union (f .: A) )
assume y in f . (union A) ; :: thesis: y in union (f .: A)
then consider x being set such that
A24: x in union A and
A25: y in f . {x} and
for b being set st b c= union A & y in f . b holds
x in b by A20, A23;
consider a being set such that
A26: x in a and
A27: a in A by A24, TARSKI:def 4;
A28: {x} c= a by A26, ZFMISC_1:31;
then {x} in C by A27, CLASSES1:def 1;
then A29: f . {x} c= f . a by A19, A27, A28;
f . a in f .: A by A27, FUNCT_1:def 6;
hence y in union (f .: A) by A25, A29, TARSKI:def 4; :: thesis: verum
end;
now :: thesis: for X being set st X in f .: A holds
X c= f . (union A)
let X be set ; :: thesis: ( X in f .: A implies X c= f . (union A) )
assume X in f .: A ; :: thesis: X c= f . (union A)
then consider a being object such that
A30: a in dom f and
A31: a in A and
A32: X = f . a by FUNCT_1:def 6;
reconsider aa = a as set by TARSKI:1;
aa c= union A by A31, ZFMISC_1:74;
hence X c= f . (union A) by A19, A23, A30, A32; :: thesis: verum
end;
hence union (f .: A) c= f . (union A) by ZFMISC_1:76; :: thesis: verum
end;