let L1, L2 be non empty up-complete Poset; for f being Function of L1,L2 st f is isomorphic holds
for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
let f be Function of L1,L2; ( f is isomorphic implies for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x) )
assume A1:
f is isomorphic
; for x being Element of L1 holds f .: (compactbelow x) = compactbelow (f . x)
then reconsider g = f " as Function of L2,L1 by WAYBEL_0:67;
let x be Element of L1; f .: (compactbelow x) = compactbelow (f . x)
A2:
g is isomorphic
by A1, WAYBEL_0:68;
A3:
compactbelow (f . x) c= f .: (compactbelow x)
proof
let z be
object ;
TARSKI:def 3 ( not z in compactbelow (f . x) or z in f .: (compactbelow x) )
x in the
carrier of
L1
;
then A4:
x in dom f
by FUNCT_2:def 1;
assume
z in compactbelow (f . x)
;
z in f .: (compactbelow x)
then
z in { y where y is Element of L2 : ( f . x >= y & y is compact ) }
by WAYBEL_8:def 2;
then consider z1 being
Element of
L2 such that A5:
z1 = z
and A6:
f . x >= z1
and A7:
z1 is
compact
;
A8:
g . z1 is
compact
by A2, A7, Th28;
g . z1 <= g . (f . x)
by A2, A6, WAYBEL_0:66;
then
g . z1 <= x
by A1, A4, FUNCT_1:34;
then A9:
g . z1 in compactbelow x
by A8, WAYBEL_8:4;
z1 in the
carrier of
L2
;
then A10:
z1 in rng f
by A1, WAYBEL_0:66;
g . z1 in the
carrier of
L1
;
then
g . z1 in dom f
by FUNCT_2:def 1;
then
f . (g . z1) in f .: (compactbelow x)
by A9, FUNCT_1:def 6;
hence
z in f .: (compactbelow x)
by A1, A5, A10, FUNCT_1:35;
verum
end;
f .: (compactbelow x) c= compactbelow (f . x)
hence
f .: (compactbelow x) = compactbelow (f . x)
by A3, XBOOLE_0:def 10; verum