let X be non empty set ; for S, T being non empty Poset
for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)
let S, T be non empty Poset; for f being Function of X, the carrier of (UPS (S,T)) holds commute f is directed-sups-preserving Function of S,(T |^ X)
let f be Function of X, the carrier of (UPS (S,T)); commute f is directed-sups-preserving Function of S,(T |^ X)
A1:
the carrier of (T |^ X) = Funcs (X, the carrier of T)
by YELLOW_1:28;
A2:
f in Funcs (X, the carrier of (UPS (S,T)))
by FUNCT_2:8;
A3:
Funcs (X, the carrier of (UPS (S,T))) c= Funcs (X,(Funcs ( the carrier of S, the carrier of T)))
by Th22, FUNCT_5:56;
then
commute f in Funcs ( the carrier of S,(Funcs (X, the carrier of T)))
by A2, FUNCT_6:55;
then reconsider g = commute f as Function of S,(T |^ X) by A1, FUNCT_2:66;
A4:
rng g c= Funcs (X, the carrier of T)
by A1;
g is directed-sups-preserving
proof
let A be
Subset of
S;
WAYBEL_0:def 37 ( A is empty or not A is directed or g preserves_sup_of A )
assume
( not
A is
empty &
A is
directed )
;
g preserves_sup_of A
then reconsider B =
A as non
empty directed Subset of
S ;
A5:
T |^ X = product (X --> T)
by YELLOW_1:def 5;
then A6:
dom (g . (sup A)) = X
by WAYBEL_3:27;
assume A7:
ex_sup_of A,
S
;
WAYBEL_0:def 31 ( ex_sup_of g .: A,T |^ X & "\/" ((g .: A),(T |^ X)) = g . ("\/" (A,S)) )
now for x being Element of X holds ex_sup_of pi ((g .: A),x),(X --> T) . xlet x be
Element of
X;
ex_sup_of pi ((g .: A),x),(X --> T) . xreconsider fx =
f . x as
directed-sups-preserving Function of
S,
T by Def4;
A8:
fx preserves_sup_of B
by WAYBEL_0:def 37;
commute g = f
by A3, A2, FUNCT_6:57;
then A9:
fx .: A = pi (
(g .: A),
x)
by A4, Th8;
thus
ex_sup_of pi (
(g .: A),
x),
(X --> T) . x
by A9, A8, A7;
verum end;
hence A10:
ex_sup_of g .: A,
T |^ X
by A5, YELLOW16:31;
"\/" ((g .: A),(T |^ X)) = g . ("\/" (A,S))
A11:
now for x being object st x in X holds
(sup (g .: A)) . x = (g . (sup A)) . xlet x be
object ;
( x in X implies (sup (g .: A)) . x = (g . (sup A)) . x )assume
x in X
;
(sup (g .: A)) . x = (g . (sup A)) . xthen reconsider a =
x as
Element of
X ;
reconsider fx =
f . a as
directed-sups-preserving Function of
S,
T by Def4;
A12:
(X --> T) . a = T
;
commute g = f
by A3, A2, FUNCT_6:57;
then A13:
fx .: A = pi (
(g .: A),
a)
by A4, Th8;
fx preserves_sup_of B
by WAYBEL_0:def 37;
then
sup (pi ((g .: B),a)) = fx . (sup A)
by A13, A7;
then
fx . (sup A) = (sup (g .: B)) . a
by A5, A10, A12, YELLOW16:33;
hence
(sup (g .: A)) . x = (g . (sup A)) . x
by A3, A2, FUNCT_6:56;
verum end;
dom (sup (g .: A)) = X
by A5, WAYBEL_3:27;
hence
"\/" (
(g .: A),
(T |^ X))
= g . ("\/" (A,S))
by A11, A6;
verum
end;
hence
commute f is directed-sups-preserving Function of S,(T |^ X)
; verum