let S be sup-Semilattice; :: thesis: for T being non empty Poset
for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
let T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) holds
f is sups-preserving
let f be Function of S,T; :: thesis: ( ( for X being finite Subset of S holds f preserves_sup_of X ) & ( for X being non empty directed Subset of S holds f preserves_sup_of X ) implies f is sups-preserving )
assume that
A1: for X being finite Subset of S holds f preserves_sup_of X and
A2: for X being non empty directed Subset of S holds f preserves_sup_of X ; :: thesis: f is sups-preserving
let X be Subset of S; :: according to WAYBEL_0:def 33 :: thesis: f preserves_sup_of X
assume A3: ex_sup_of X,S ; :: according to WAYBEL_0:def 31 :: thesis: ( ex_sup_of f .: X,T & sup (f .: X) = f . (sup X) )
defpred S₁[ set ] means ex Y being finite Subset of X st
( ex_sup_of Y,S & $1 = "\/" Y,S );
consider Z being set such that
A4: for x being set holds
( x in Z iff ( x in the carrier of S & S₁[x] ) ) from XBOOLE_0:sch 1();
Z c= the carrier of S

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in Z or x in the carrier of S )
thus ( not x in Z or x in the carrier of S ) by A4; :: thesis: verum

end;

then reconsider Z = Z as Subset of S ;

A5: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies ex_sup_of Y,S )
Y is Subset of S by XBOOLE_1:1;
hence ( Y <> {} implies ex_sup_of Y,S ) by YELLOW_0:54; :: thesis: verum

end;

A6: now

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" Y,S in Z )
reconsider Y' = Y as Subset of S by XBOOLE_1:1;
assume Y <> {} ; :: thesis: "\/" Y,S in Z
then ex_sup_of Y',S by YELLOW_0:54;
hence "\/" Y,S in Z by A4; :: thesis: verum

end;

for x being Element of S st x in Z holds
ex Y being finite Subset of X st
( ex_sup_of Y,S & x = "\/" Y,S ) by A4;
then A7: ( Z is directed & ex_sup_of Z,S & sup Z = sup X & ( Z = {} or Z <> {} ) ) by A3, A5, A6, Th51, Th53, Th54;
then f preserves_sup_of Z by A1, A2;
then A8: ( ex_sup_of f .: Z,T & sup (f .: Z) = f . (sup Z) & sup Z = sup X ) by A7, Def31;
X c= Z

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )
assume A9: x in X ; :: thesis: x in Z
then reconsider Y = {x} as finite Subset of X by ZFMISC_1:37;
reconsider x = x as Element of S by A9;
Y is Subset of S by XBOOLE_1:1;
then ( ex_sup_of Y,S & x = "\/" Y,S ) by YELLOW_0:39, YELLOW_0:54;
hence x in Z by A4; :: thesis: verum

end;

then A10: f .: X c= f .: Z by RELAT_1:156;
A11: f .: Z is_<=_than f . (sup X) by A8, YELLOW_0:30;
A12: f .: X is_<=_than f . (sup X)

proof

let x be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not x in f .: X or x <= f . (sup X) )
assume x in f .: X ; :: thesis: x <= f . (sup X)
hence x <= f . (sup X) by A10, A11, LATTICE3:def 9; :: thesis: verum

end;

A13: now

let b be Element of T; :: thesis: ( f .: X is_<=_than b implies f . (sup X) <= b )
assume A14: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b
f .: Z is_<=_than b

proof

let a be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not a in f .: Z or a <= b )
assume a in f .: Z ; :: thesis: a <= b
then consider x being set such that
A15: ( x in dom f & x in Z & a = f . x ) by FUNCT_1:def 12;
consider Y being finite Subset of X such that
A16: ( ex_sup_of Y,S & x = "\/" Y,S ) by A4, A15;
reconsider Y = Y as Subset of S by XBOOLE_1:1;
( f .: Y c= f .: X & f preserves_sup_of Y ) by A1, RELAT_1:156;
then ( b is_>=_than f .: Y & a = "\/" (f .: Y),T & ex_sup_of f .: Y,T ) by A14, A15, A16, Def31, YELLOW_0:9;
hence a <= b by YELLOW_0:def 9; :: thesis: verum

end;

hence f . (sup X) <= b by A8, YELLOW_0:30; :: thesis: verum

end;

hence ex_sup_of f .: X,T by A12, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A12, A13, YELLOW_0:def 9; :: thesis: verum