let W be with_non-empty_element set ; :: thesis: for a, b being LATTICE
for f being Function of a,b holds
( f in the Arrows of (W -SUP_category ) . a,b iff ( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving ) )
A1:
ex x being non empty set st x in W
by SETFAM_1:def 11;
let a, b be LATTICE; :: thesis: for f being Function of a,b holds
( f in the Arrows of (W -SUP_category ) . a,b iff ( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving ) )
let f be Function of a,b; :: thesis: ( f in the Arrows of (W -SUP_category ) . a,b iff ( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving ) )
set A = W -SUP_category ;
hereby :: thesis: ( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving implies f in the Arrows of (W -SUP_category ) . a,b )
assume
f in the
Arrows of
(W -SUP_category ) . a,
b
;
:: thesis: ( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) & a is complete & b is complete & f is sups-preserving )then consider o1,
o2 being
object of
(W -SUP_category ) such that A2:
(
o1 = a &
o2 = b &
f in <^o1,o2^> &
f is
Morphism of
o1,
o2 )
by Th12;
reconsider g =
f as
Morphism of
o1,
o2 by A2;
thus
(
a in the
carrier of
(W -SUP_category ) &
b in the
carrier of
(W -SUP_category ) )
by A2;
:: thesis: ( a is complete & b is complete & f is sups-preserving )thus
(
a is
complete &
b is
complete )
by A1, A2, Def5;
:: thesis: f is sups-preserving
(
latt o1 = a &
latt o2 = b &
@ g = f )
by A2, YELLOW21:def 7;
hence
f is
sups-preserving
by A1, A2, Def5;
:: thesis: verum
end;
assume
( a in the carrier of (W -SUP_category ) & b in the carrier of (W -SUP_category ) )
; :: thesis: ( not a is complete or not b is complete or not f is sups-preserving or f in the Arrows of (W -SUP_category ) . a,b )
then reconsider x = a, y = b as object of (W -SUP_category ) ;
A3:
( latt x = a & latt y = b )
;
assume A4:
( a is complete & b is complete & f is sups-preserving )
; :: thesis: f in the Arrows of (W -SUP_category ) . a,b
f in <^x,y^>
by A1, A3, A4, Def5;
hence
f in the Arrows of (W -SUP_category ) . a,b
by ALTCAT_1:def 2; :: thesis: verum