let L1, L2 be non empty antisymmetric RelStr ; :: thesis: for f being Function of L1,L2 st f is isomorphic holds
( f is infs-preserving & f is sups-preserving )
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies ( f is infs-preserving & f is sups-preserving ) )
assume A1: f is isomorphic ; :: thesis: ( f is infs-preserving & f is sups-preserving )
then A2: rng f = the carrier of L2 by WAYBEL_0:66;
now :: thesis: for X being Subset of L1 holds f preserves_inf_of X
let X be Subset of L1; :: thesis: f preserves_inf_of X
now :: thesis: ( ex_inf_of X,L1 implies ( ex_inf_of f .: X,L2 & inf (f .: X) = f . (inf X) ) )
assume A3: ex_inf_of X,L1 ; :: thesis: ( ex_inf_of f .: X,L2 & inf (f .: X) = f . (inf X) )
then consider a being Element of L1 such that
A4: X is_>=_than a and
A5: for b being Element of L1 st X is_>=_than b holds
a >= b by YELLOW_0:16;
A6: now :: thesis: for c being Element of L2 st f .: X is_>=_than c holds
f . a >= c
let c be Element of L2; :: thesis: ( f .: X is_>=_than c implies f . a >= c )
consider e being object such that
A7: e in dom f and
A8: c = f . e by A2, FUNCT_1:def 3;
reconsider e = e as Element of L1 by A7;
assume f .: X is_>=_than c ; :: thesis: f . a >= c
then X is_>=_than e by A1, A8, Th18;
then a >= e by A5;
hence f . a >= c by A1, A8, WAYBEL_0:66; :: thesis: verum
end;
f .: X is_>=_than f . a by A1, A4, Th18;
hence ex_inf_of f .: X,L2 by A6, YELLOW_0:16; :: thesis: inf (f .: X) = f . (inf X)
A9: now :: thesis: for b being Element of L2 st b is_<=_than f .: X holds
f . (inf X) >= b
let b be Element of L2; :: thesis: ( b is_<=_than f .: X implies f . (inf X) >= b )
consider v being object such that
A10: v in dom f and
A11: b = f . v by A2, FUNCT_1:def 3;
reconsider v = v as Element of L1 by A10;
assume b is_<=_than f .: X ; :: thesis: f . (inf X) >= b
then v is_<=_than X by A1, A11, Th18;
then inf X >= v by A3, YELLOW_0:31;
hence f . (inf X) >= b by A1, A11, WAYBEL_0:66; :: thesis: verum
end;
inf X is_<=_than X by A3, YELLOW_0:31;
then f . (inf X) is_<=_than f .: X by A1, Th18;
hence inf (f .: X) = f . (inf X) by A9, YELLOW_0:31; :: thesis: verum
end;
hence f preserves_inf_of X by WAYBEL_0:def 30; :: thesis: verum
end;
hence f is infs-preserving by WAYBEL_0:def 32; :: thesis: f is sups-preserving
now :: thesis: for X being Subset of L1 holds f preserves_sup_of X
let X be Subset of L1; :: thesis: f preserves_sup_of X
now :: thesis: ( ex_sup_of X,L1 implies ( ex_sup_of f .: X,L2 & sup (f .: X) = f . (sup X) ) )
assume A12: ex_sup_of X,L1 ; :: thesis: ( ex_sup_of f .: X,L2 & sup (f .: X) = f . (sup X) )
then consider a being Element of L1 such that
A13: X is_<=_than a and
A14: for b being Element of L1 st X is_<=_than b holds
a <= b by YELLOW_0:15;
A15: now :: thesis: for c being Element of L2 st f .: X is_<=_than c holds
f . a <= c
let c be Element of L2; :: thesis: ( f .: X is_<=_than c implies f . a <= c )
consider e being object such that
A16: e in dom f and
A17: c = f . e by A2, FUNCT_1:def 3;
reconsider e = e as Element of L1 by A16;
assume f .: X is_<=_than c ; :: thesis: f . a <= c
then X is_<=_than e by A1, A17, Th19;
then a <= e by A14;
hence f . a <= c by A1, A17, WAYBEL_0:66; :: thesis: verum
end;
f .: X is_<=_than f . a by A1, A13, Th19;
hence ex_sup_of f .: X,L2 by A15, YELLOW_0:15; :: thesis: sup (f .: X) = f . (sup X)
A18: now :: thesis: for b being Element of L2 st b is_>=_than f .: X holds
f . (sup X) <= b
let b be Element of L2; :: thesis: ( b is_>=_than f .: X implies f . (sup X) <= b )
consider v being object such that
A19: v in dom f and
A20: b = f . v by A2, FUNCT_1:def 3;
reconsider v = v as Element of L1 by A19;
assume b is_>=_than f .: X ; :: thesis: f . (sup X) <= b
then v is_>=_than X by A1, A20, Th19;
then sup X <= v by A12, YELLOW_0:30;
hence f . (sup X) <= b by A1, A20, WAYBEL_0:66; :: thesis: verum
end;
sup X is_>=_than X by A12, YELLOW_0:30;
then f . (sup X) is_>=_than f .: X by A1, Th19;
hence sup (f .: X) = f . (sup X) by A18, YELLOW_0:30; :: thesis: verum
end;
hence f preserves_sup_of X by WAYBEL_0:def 31; :: thesis: verum
end;
hence f is sups-preserving by WAYBEL_0:def 33; :: thesis: verum