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;
A12: 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 A13: f .: X is_<=_than b ; :: thesis: f . (sup X) <= b
f .: (downarrow X) is_<=_than b
proof
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;
hence f . (sup X) <= b by A6, A7, A8, YELLOW_0:30; :: thesis: verum
end;
hence ex_sup_of f .: X,T by A11, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)
hence sup (f .: X) = f . (sup X) by A11, A12, YELLOW_0:def 9; :: thesis: verum