let L be complete Semilattice; ( ( for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f)) ) implies for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume A1:
for x being Element of L
for J being set
for f being Function of J, the carrier of L holds x "/\" (Sup ) = sup (x "/\" (FinSups f))
; for x being Element of L
for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let x be Element of L; for N being prenet of L st N is eventually-directed holds
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
let N be prenet of L; ( N is eventually-directed implies x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L)))) )
assume A2:
N is eventually-directed
; x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
reconsider R = rng (netmap (N,L)) as non empty directed Subset of L by A2, Th18;
reconsider xx = {x} as non empty directed Subset of L by WAYBEL_0:5;
set f = the mapping of N;
set h = the mapping of (FinSups the mapping of N);
A3:
ex_sup_of xx "/\" R,L
by WAYBEL_0:75;
A4:
rng the mapping of (x "/\" (FinSups the mapping of N)) is_<=_than sup ({x} "/\" (rng (netmap (N,L))))
proof
let a be
Element of
L;
LATTICE3:def 9 ( not a in rng the mapping of (x "/\" (FinSups the mapping of N)) or a <= sup ({x} "/\" (rng (netmap (N,L)))) )
A5:
{x} "/\" (rng the mapping of (FinSups the mapping of N)) = { (x "/\" y) where y is Element of L : y in rng the mapping of (FinSups the mapping of N) }
by YELLOW_4:42;
assume
a in rng the
mapping of
(x "/\" (FinSups the mapping of N))
;
a <= sup ({x} "/\" (rng (netmap (N,L))))
then
a in {x} "/\" (rng the mapping of (FinSups the mapping of N))
by Th23;
then consider y being
Element of
L such that A6:
a = x "/\" y
and A7:
y in rng the
mapping of
(FinSups the mapping of N)
by A5;
for
x being
set holds
ex_sup_of the
mapping of
N .: x,
L
by YELLOW_0:17;
then
rng (netmap ((FinSups the mapping of N),L)) c= finsups (rng the mapping of N)
by Th24;
then
y in finsups (rng the mapping of N)
by A7;
then consider Y being
finite Subset of
(rng the mapping of N) such that A8:
y = "\/" (
Y,
L)
and A9:
ex_sup_of Y,
L
;
rng (netmap (N,L)) is
directed
by A2, Th18;
then consider z being
Element of
L such that A10:
z in rng the
mapping of
N
and A11:
z is_>=_than Y
by WAYBEL_0:1;
A12:
x <= x
;
"\/" (
Y,
L)
<= z
by A9, A11, YELLOW_0:30;
then A13:
x "/\" y <= x "/\" z
by A8, A12, YELLOW_3:2;
x in {x}
by TARSKI:def 1;
then
x "/\" z <= sup (xx "/\" (rng the mapping of N))
by A3, A10, YELLOW_4:1, YELLOW_4:37;
hence
a <= sup ({x} "/\" (rng (netmap (N,L))))
by A6, A13, YELLOW_0:def 2;
verum
end;
x "/\" (FinSups the mapping of N) is eventually-directed
by Th27;
then
rng (netmap ((x "/\" (FinSups the mapping of N)),L)) is directed
by Th18;
then
ex_sup_of rng the mapping of (x "/\" (FinSups the mapping of N)),L
by WAYBEL_0:75;
then
( sup (x "/\" (FinSups the mapping of N)) = "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) & "\/" ((rng the mapping of (x "/\" (FinSups the mapping of N))),L) <= sup ({x} "/\" (rng (netmap (N,L)))) )
by A4, YELLOW_0:def 9, YELLOW_2:def 5;
then A14:
x "/\" (Sup ) <= sup ({x} "/\" (rng (netmap (N,L))))
by A1;
( ex_sup_of R,L & Sup = "\/" ((rng (netmap (N,L))),L) )
by WAYBEL_0:75, YELLOW_2:def 5;
then
sup ({x} "/\" (rng (netmap (N,L)))) <= x "/\" (Sup )
by A3, YELLOW_4:53;
hence
x "/\" (sup N) = sup ({x} "/\" (rng (netmap (N,L))))
by A14, ORDERS_2:2; verum