let S, T be lower-bounded with_suprema Poset; for f being Function of S,T st f is join-preserving & f is bottom-preserving holds
f is finite-sups-preserving
let f be Function of S,T; ( f is join-preserving & f is bottom-preserving implies f is finite-sups-preserving )
assume A1:
( f is join-preserving & f is bottom-preserving )
; f is finite-sups-preserving
let X be finite Subset of S; WAYBEL34:def 15 f preserves_sup_of X
A2:
X is finite
;
defpred S1[ set ] means for Y being finite Subset of S st Y = $1 holds
f preserves_sup_of Y;
f preserves_sup_of {} S
by A1;
then A3:
S1[ {} ]
;
A4:
for x, B being set st x in X & B c= X & S1[B] holds
S1[B \/ {x}]
proof
let x,
B be
set ;
( x in X & B c= X & S1[B] implies S1[B \/ {x}] )
assume that
x in X
and
B c= X
and A5:
for
Y being
finite Subset of
S st
Y = B holds
f preserves_sup_of Y
;
S1[B \/ {x}]
let Y be
finite Subset of
S;
( Y = B \/ {x} implies f preserves_sup_of Y )
assume A6:
Y = B \/ {x}
;
f preserves_sup_of Y
A7:
B c= Y
by A6, XBOOLE_1:7;
A8:
{x} c= Y
by A6, XBOOLE_1:7;
reconsider Z =
B as
finite Subset of
S by A7, XBOOLE_1:1;
A9:
x in Y
by A8, ZFMISC_1:31;
then reconsider x =
x as
Element of
S ;
A10:
f preserves_sup_of Z
by A5;
(
f .: Z = {} or (
f .: Z <> {} &
f .: Z is
finite ) )
;
then A11:
ex_sup_of f .: Z,
T
by YELLOW_0:42, YELLOW_0:54;
A12:
ex_sup_of {(f . x)},
T
by YELLOW_0:54;
(
Z = {} or
Z <> {} )
;
then A13:
ex_sup_of Z,
S
by YELLOW_0:42, YELLOW_0:54;
A14:
f preserves_sup_of {(sup Z),x}
by A1;
A15:
sup {x} = x
by YELLOW_0:39;
A16:
ex_sup_of {x},
S
by YELLOW_0:38;
A17:
ex_sup_of Y,
S
by A9, YELLOW_0:54;
assume
ex_sup_of Y,
S
;
WAYBEL_0:def 31 ( ex_sup_of f .: Y,T & "\/" ((f .: Y),T) = f . ("\/" (Y,S)) )
thus
ex_sup_of f .: Y,
T
by A9, YELLOW_0:54;
"\/" ((f .: Y),T) = f . ("\/" (Y,S))
dom f = the
carrier of
S
by FUNCT_2:def 1;
then
Im (
f,
x)
= {(f . x)}
by FUNCT_1:59;
then A18:
f .: Y = (f .: Z) \/ {(f . x)}
by A6, RELAT_1:120;
sup {(f . x)} = f . x
by YELLOW_0:39;
hence sup (f .: Y) =
(sup (f .: Z)) "\/" (f . x)
by A11, A12, A18, YELLOW_2:3
.=
(f . (sup Z)) "\/" (f . x)
by A10, A13
.=
f . ((sup Z) "\/" x)
by A14, YELLOW_3:9
.=
f . (sup Y)
by A6, A13, A15, A16, A17, YELLOW_0:36
;
verum
end;
S1[X]
from FINSET_1:sch 2(A2, A3, A4);
hence
f preserves_sup_of X
; verum