let L be completely-distributive LATTICE; for X being non empty Subset of L
for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
let X be non empty Subset of L; for x being Element of L holds x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
let x be Element of L; x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
set A = { (x "/\" y) where y is Element of L : y in X } ;
set J = {1,2};
set K = (1,2) --> ({1},X);
set F = (1,2) --> (({1} --> x),(id X));
A1:
((1,2) --> (({1} --> x),(id X))) . 1 = {1} --> x
by FUNCT_4:63;
A2:
dom ((1,2) --> ({1},X)) = {1,2}
by FUNCT_4:62;
A3:
((1,2) --> ({1},X)) . 2 = X
by FUNCT_4:63;
A4:
dom ((1,2) --> (({1} --> x),(id X))) = {1,2}
by FUNCT_4:62;
reconsider j1 = 1, j2 = 2 as Element of {1,2} by TARSKI:def 2;
A5:
((1,2) --> (({1} --> x),(id X))) . 2 = id X
by FUNCT_4:63;
reconsider F = (1,2) --> (({1} --> x),(id X)) as ManySortedSet of {1,2} by A4, PARTFUN1:def 2, RELAT_1:def 18;
A6:
((1,2) --> ({1},X)) . 1 = {1}
by FUNCT_4:63;
reconsider K = (1,2) --> ({1},X) as ManySortedSet of {1,2} by A2, PARTFUN1:def 2, RELAT_1:def 18;
for i being object st i in {1,2} holds
not K . i is empty
by A6, A3, TARSKI:def 2;
then reconsider K = K as non-empty ManySortedSet of {1,2} by PBOOLE:def 13;
for j being object st j in {1,2} holds
F . j is Function of (K . j),(({1,2} --> the carrier of L) . j)
then reconsider F = F as DoubleIndexedSet of K,L by PBOOLE:def 15;
rng (Infs ) is_<=_than "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
proof
let y be
Element of
L;
LATTICE3:def 9 ( not y in rng (Infs ) or y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L) )
assume
y in rng (Infs )
;
y <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
then consider f being
object such that A9:
f in dom (Frege F)
and A10:
y = //\ (
((Frege F) . f),
L)
by Th13;
reconsider f =
f as
Function by A9;
A11:
f . j2 in K . j2
by A9, Lm6;
then reconsider f2 =
f . 2 as
Element of
X by FUNCT_4:63;
A12:
f . j1 in K . j1
by A9, Lm6;
A13:
{x,f2} c= rng ((Frege F) . f)
proof
let z be
object ;
TARSKI:def 3 ( not z in {x,f2} or z in rng ((Frege F) . f) )
assume
z in {x,f2}
;
z in rng ((Frege F) . f)
then
(
z = x or
z = f . 2 )
by TARSKI:def 2;
then
(
z = (F . j1) . (f . j1) or
z = (F . j2) . (f . j2) )
by A1, A5, A6, A3, A12, A11, FUNCOP_1:7, FUNCT_1:18;
hence
z in rng ((Frege F) . f)
by A9, Lm5;
verum
end;
x "/\" f2 in { (x "/\" y) where y is Element of L : y in X }
;
then A14:
x "/\" f2 <= "\/" (
{ (x "/\" y) where y is Element of L : y in X } ,
L)
by YELLOW_2:22;
A15:
(
ex_inf_of rng ((Frege F) . f),
L &
ex_inf_of {x,(f . 2)},
L )
by YELLOW_0:17;
y = "/\" (
(rng ((Frege F) . f)),
L)
by A10, YELLOW_2:def 6;
then
y <= inf {x,f2}
by A15, A13, YELLOW_0:35;
then
y <= x "/\" f2
by YELLOW_0:40;
hence
y <= "\/" (
{ (x "/\" y) where y is Element of L : y in X } ,
L)
by A14, YELLOW_0:def 2;
verum
end;
then
sup (rng (Infs )) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
by YELLOW_0:32;
then A16:
Sup <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
by YELLOW_2:def 5;
(x "/\") .: X = { (x "/\" y) where y is Element of L : y in X }
by WAYBEL_1:61;
then reconsider A9 = { (x "/\" y) where y is Element of L : y in X } as Subset of L ;
( ex_sup_of X,L & ex_sup_of A9,L )
by YELLOW_0:17;
then A17:
x "/\" (sup X) >= sup A9
by Th25;
x "/\" (sup X) is_<=_than rng (Sups )
then
x "/\" (sup X) <= inf (rng (Sups ))
by YELLOW_0:33;
then
x "/\" (sup X) <= Inf
by YELLOW_2:def 6;
then
x "/\" (sup X) <= Sup
by Def3;
then
x "/\" (sup X) <= "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
by A16, YELLOW_0:def 2;
hence
x "/\" (sup X) = "\/" ( { (x "/\" y) where y is Element of L : y in X } ,L)
by A17, YELLOW_0:def 3; verum