let S, T be non empty Poset; :: thesis: for f being Function of S,T st ( for X being Ideal of S holds f preserves_sup_of X ) holds

f is directed-sups-preserving

let f be Function of S,T; :: thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )

assume A1: for X being Ideal of S holds f preserves_sup_of X ; :: thesis: f is directed-sups-preserving

let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( not X is empty & X is directed implies f preserves_sup_of X )

assume that

A2: ( not X is empty & X is directed ) and

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) )

reconsider Y = X as non empty directed Subset of S by A2;

downarrow Y is Ideal of S ;

then A4: f preserves_sup_of downarrow X by A1;

A5: ex_sup_of downarrow X,S by A3, Th32;

then A6: ex_sup_of f .: (downarrow X),T by A4;

A7: sup (f .: (downarrow X)) = f . (sup (downarrow X)) by A4, A5;

A8: sup (downarrow X) = sup X by A3, Th33;

A9: f .: X c= f .: (downarrow X) by Th16, RELAT_1:123;

A10: f .: (downarrow X) is_<=_than f . (sup X) by A6, A7, A8, YELLOW_0:30;

A11: f .: X is_<=_than f . (sup X) by A9, A10;

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

f is directed-sups-preserving

let f be Function of S,T; :: thesis: ( ( for X being Ideal of S holds f preserves_sup_of X ) implies f is directed-sups-preserving )

assume A1: for X being Ideal of S holds f preserves_sup_of X ; :: thesis: f is directed-sups-preserving

let X be Subset of S; :: according to WAYBEL_0:def 37 :: thesis: ( not X is empty & X is directed implies f preserves_sup_of X )

assume that

A2: ( not X is empty & X is directed ) and

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) )

reconsider Y = X as non empty directed Subset of S by A2;

downarrow Y is Ideal of S ;

then A4: f preserves_sup_of downarrow X by A1;

A5: ex_sup_of downarrow X,S by A3, Th32;

then A6: ex_sup_of f .: (downarrow X),T by A4;

A7: sup (f .: (downarrow X)) = f . (sup (downarrow X)) by A4, A5;

A8: sup (downarrow X) = sup X by A3, Th33;

A9: f .: X c= f .: (downarrow X) by Th16, RELAT_1:123;

A10: f .: (downarrow X) is_<=_than f . (sup X) by A6, A7, A8, YELLOW_0:30;

A11: f .: X is_<=_than f . (sup X) by A9, A10;

A12: 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 A11, 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 A13: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b

f .: (downarrow X) is_<=_than b

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

f .: (downarrow X) is_<=_than b

proof

hence
f . (sup X) <= b
by A6, A7, A8, YELLOW_0:30; :: thesis: verum
let a be Element of T; :: according to LATTICE3:def 9 :: thesis: ( not a in f .: (downarrow X) or a <= b )

assume a in f .: (downarrow X) ; :: thesis: a <= b

then consider x being object such that

x in dom f and

A14: x in downarrow X and

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

downarrow X = { z where z is Element of S : ex y being Element of S st

( z <= y & y in X ) } by Th14;

then consider z being Element of S such that

A16: x = z and

A17: ex y being Element of S st

( z <= y & y in X ) by A14;

consider y being Element of S such that

A18: z <= y and

A19: y in X by A17;

A20: f is monotone by A1, Th72;

A21: f . y in f .: X by A19, FUNCT_2:35;

A22: f . z <= f . y by A18, A20;

f . y <= b by A13, A21;

hence a <= b by A15, A16, A22, ORDERS_2:3; :: thesis: verum

end;assume a in f .: (downarrow X) ; :: thesis: a <= b

then consider x being object such that

x in dom f and

A14: x in downarrow X and

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

downarrow X = { z where z is Element of S : ex y being Element of S st

( z <= y & y in X ) } by Th14;

then consider z being Element of S such that

A16: x = z and

A17: ex y being Element of S st

( z <= y & y in X ) by A14;

consider y being Element of S such that

A18: z <= y and

A19: y in X by A17;

A20: f is monotone by A1, Th72;

A21: f . y in f .: X by A19, FUNCT_2:35;

A22: f . z <= f . y by A18, A20;

f . y <= b by A13, A21;

hence a <= b by A15, A16, A22, ORDERS_2:3; :: thesis: verum

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