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_{1}[ object ] 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 object holds

( x in Z iff ( x in the carrier of S & S_{1}[x] ) )
from XBOOLE_0:sch 1();

Z c= the carrier of S by A4;

then reconsider Z = Z as Subset of S ;

ex Y being finite Subset of X st

( ex_sup_of Y,S & x = "\/" (Y,S) ) by A4;

then A8: Z is directed by A5, A6, Th51;

A9: ex_sup_of Z,S by A3, A5, A6, A7, Th53;

( Z = {} or Z <> {} ) ;

then A10: f preserves_sup_of Z by A1, A2, A8;

then A11: ex_sup_of f .: Z,T by A9;

A12: sup (f .: Z) = f . (sup Z) by A9, A10;

A13: sup Z = sup X by A3, A5, A6, A7, Th54;

X c= Z

A17: f .: Z is_<=_than f . (sup X) by A11, A12, A13, YELLOW_0:30;

A18: f .: X is_<=_than f . (sup X) by A16, A17;

hence sup (f .: X) = f . (sup X) by A18, A19, YELLOW_0:def 9; :: thesis: verum

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

( ex_sup_of Y,S & $1 = "\/" (Y,S) );

consider Z being set such that

A4: for x being object holds

( x in Z iff ( x in the carrier of S & S

Z c= the carrier of S by A4;

then reconsider Z = Z as Subset of S ;

A5: now :: thesis: for Y being finite Subset of X st Y <> {} holds

ex_sup_of Y,S

ex_sup_of Y,S

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;Y is Subset of S by XBOOLE_1:1;

hence ( Y <> {} implies ex_sup_of Y,S ) by YELLOW_0:54; :: thesis: verum

A6: now :: thesis: for Y being finite Subset of X st Y <> {} holds

"\/" (Y,S) in Z

A7:
for x being Element of S st x in Z holds "\/" (Y,S) in Z

let Y be finite Subset of X; :: thesis: ( Y <> {} implies "\/" (Y,S) in Z )

reconsider Y9 = Y as Subset of S by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "\/" (Y,S) in Z

then ex_sup_of Y9,S by YELLOW_0:54;

hence "\/" (Y,S) in Z by A4; :: thesis: verum

end;reconsider Y9 = Y as Subset of S by XBOOLE_1:1;

assume Y <> {} ; :: thesis: "\/" (Y,S) in Z

then ex_sup_of Y9,S by YELLOW_0:54;

hence "\/" (Y,S) in Z by A4; :: thesis: verum

ex Y being finite Subset of X st

( ex_sup_of Y,S & x = "\/" (Y,S) ) by A4;

then A8: Z is directed by A5, A6, Th51;

A9: ex_sup_of Z,S by A3, A5, A6, A7, Th53;

( Z = {} or Z <> {} ) ;

then A10: f preserves_sup_of Z by A1, A2, A8;

then A11: ex_sup_of f .: Z,T by A9;

A12: sup (f .: Z) = f . (sup Z) by A9, A10;

A13: sup Z = sup X by A3, A5, A6, A7, Th54;

X c= Z

proof

then A16:
f .: X c= f .: Z
by RELAT_1:123;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in X or x in Z )

assume A14: x in X ; :: thesis: x in Z

then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;

reconsider x = x as Element of S by A14;

Y is Subset of S by XBOOLE_1:1;

then A15: ex_sup_of Y,S by YELLOW_0:54;

x = "\/" (Y,S) by YELLOW_0:39;

hence x in Z by A4, A15; :: thesis: verum

end;assume A14: x in X ; :: thesis: x in Z

then reconsider Y = {x} as finite Subset of X by ZFMISC_1:31;

reconsider x = x as Element of S by A14;

Y is Subset of S by XBOOLE_1:1;

then A15: ex_sup_of Y,S by YELLOW_0:54;

x = "\/" (Y,S) by YELLOW_0:39;

hence x in Z by A4, A15; :: thesis: verum

A17: f .: Z is_<=_than f . (sup X) by A11, A12, A13, YELLOW_0:30;

A18: f .: X is_<=_than f . (sup X) by A16, A17;

A19: now :: thesis: for b being Element of T st f .: X is_<=_than b holds

f . (sup X) <= b

hence
ex_sup_of f .: X,T
by A18, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)f . (sup X) <= b

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

assume A20: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b

f .: Z is_<=_than b

end;assume A20: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b

f .: Z is_<=_than b

proof

hence
f . (sup X) <= b
by A11, A12, A13, YELLOW_0:30; :: thesis: verum
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 object such that

x in dom f and

A21: x in Z and

A22: a = f . x by FUNCT_1:def 6;

consider Y being finite Subset of X such that

A23: ex_sup_of Y,S and

A24: x = "\/" (Y,S) by A4, A21;

reconsider Y = Y as Subset of S by XBOOLE_1:1;

A25: f .: Y c= f .: X by RELAT_1:123;

A26: f preserves_sup_of Y by A1;

A27: b is_>=_than f .: Y by A20, A25;

A28: a = "\/" ((f .: Y),T) by A22, A23, A24, A26;

ex_sup_of f .: Y,T by A23, A26;

hence a <= b by A27, A28, YELLOW_0:def 9; :: thesis: verum

end;assume a in f .: Z ; :: thesis: a <= b

then consider x being object such that

x in dom f and

A21: x in Z and

A22: a = f . x by FUNCT_1:def 6;

consider Y being finite Subset of X such that

A23: ex_sup_of Y,S and

A24: x = "\/" (Y,S) by A4, A21;

reconsider Y = Y as Subset of S by XBOOLE_1:1;

A25: f .: Y c= f .: X by RELAT_1:123;

A26: f preserves_sup_of Y by A1;

A27: b is_>=_than f .: Y by A20, A25;

A28: a = "\/" ((f .: Y),T) by A22, A23, A24, A26;

ex_sup_of f .: Y,T by A23, A26;

hence a <= b by A27, A28, YELLOW_0:def 9; :: thesis: verum

hence sup (f .: X) = f . (sup X) by A18, A19, YELLOW_0:def 9; :: thesis: verum