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 S1[ 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 & S1[x] ) ) from XBOOLE_0:sch 1();
 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
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 :: thesis: for Y being finite Subset of X st Y <> {} 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;
A7: 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 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
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;
then A16: f .: X c= f .: Z by RELAT_1:123;
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
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
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 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;
hence f . (sup X) <= b by A11, A12, A13, YELLOW_0:30; :: thesis: verum
end;
hence ex_sup_of f .: X,T by A18, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A18, A19, YELLOW_0:def 9; :: thesis: verum