let L be complete LATTICE; for J being non empty set
for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let J be non empty set ; for K being V9() ManySortedSet of J
for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let K be V9() ManySortedSet of J; for F being DoubleIndexedSet of K,L st ( for j being Element of J holds rng (F . j) is directed ) holds
rng (Infs ) is directed
let F be DoubleIndexedSet of K,L; ( ( for j being Element of J holds rng (F . j) is directed ) implies rng (Infs ) is directed )
set X = rng (Infs );
assume A1:
for j being Element of J holds rng (F . j) is directed
; rng (Infs ) is directed
for x, y being Element of L st x in rng (Infs ) & y in rng (Infs ) holds
ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
proof
let x,
y be
Element of
L;
( x in rng (Infs ) & y in rng (Infs ) implies ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z ) )
assume that A2:
x in rng (Infs )
and A3:
y in rng (Infs )
;
ex z being Element of L st
( z in rng (Infs ) & x <= z & y <= z )
consider h being
object such that A4:
h in dom (Frege F)
and A5:
y = //\ (
((Frege F) . h),
L)
by A3, Th13;
reconsider h =
h as
Function by A4;
reconsider H =
(Frege F) . h as
Function of
J, the
carrier of
L by A4, Th10;
consider g being
object such that A6:
g in dom (Frege F)
and A7:
x = //\ (
((Frege F) . g),
L)
by A2, Th13;
reconsider g =
g as
Function by A6;
reconsider G =
(Frege F) . g as
Function of
J, the
carrier of
L by A6, Th10;
A8:
ex_inf_of rng ((Frege F) . g),
L
by YELLOW_0:17;
defpred S1[
object ,
object ]
means ( $1
in J & $2
in K . $1 & ( for
c being
Element of
L st
c = (F . $1) . $2 holds
( ( for
a being
Element of
L st
a = G . $1 holds
a <= c ) & ( for
b being
Element of
L st
b = H . $1 holds
b <= c ) ) ) );
A9:
for
j being
Element of
J ex
k being
Element of
K . j st
(
G . j <= (F . j) . k &
H . j <= (F . j) . k )
proof
let j be
Element of
J;
ex k being Element of K . j st
( G . j <= (F . j) . k & H . j <= (F . j) . k )
j in J
;
then A10:
j in dom F
by PARTFUN1:def 2;
then A11:
g . j in dom (F . j)
by A6, Th9;
j in J
;
then A12:
j in dom F
by PARTFUN1:def 2;
then
G . j = (F . j) . (g . j)
by A6, Th9;
then A13:
G . j in rng (F . j)
by A11, FUNCT_1:def 3;
A14:
h . j in dom (F . j)
by A4, A10, Th9;
H . j = (F . j) . (h . j)
by A4, A12, Th9;
then A15:
H . j in rng (F . j)
by A14, FUNCT_1:def 3;
rng (F . j) is
directed Subset of
L
by A1;
then consider c being
Element of
L such that A16:
c in rng (F . j)
and A17:
(
G . j <= c &
H . j <= c )
by A13, A15, WAYBEL_0:def 1;
consider k being
object such that A18:
k in dom (F . j)
and A19:
c = (F . j) . k
by A16, FUNCT_1:def 3;
reconsider k =
k as
Element of
K . j by A18;
take
k
;
( G . j <= (F . j) . k & H . j <= (F . j) . k )
thus
(
G . j <= (F . j) . k &
H . j <= (F . j) . k )
by A17, A19;
verum
end;
A20:
for
j being
object st
j in J holds
ex
k being
object st
(
k in union (rng K) &
S1[
j,
k] )
consider f being
Function such that A22:
dom f = J
and
rng f c= union (rng K)
and A23:
for
j being
object st
j in J holds
S1[
j,
f . j]
from FUNCT_1:sch 6(A20);
dom f =
dom F
by A22, PARTFUN1:def 2
.=
dom (doms F)
by FUNCT_6:59
;
then
f in product (doms F)
by A24, CARD_3:9;
then A26:
f in dom (Frege F)
by PARTFUN1:def 2;
then reconsider Ff =
(Frege F) . f as
Function of
J, the
carrier of
L by Th10;
take z =
Inf ;
( z in rng (Infs ) & x <= z & y <= z )
thus
z in rng (Infs )
by A26, Th13;
( x <= z & y <= z )
A27:
x = "/\" (
(rng ((Frege F) . g)),
L)
by A7, YELLOW_2:def 6;
hence
x <= z
by YELLOW_2:55;
y <= z
A31:
ex_inf_of rng ((Frege F) . h),
L
by YELLOW_0:17;
A32:
y = "/\" (
(rng ((Frege F) . h)),
L)
by A5, YELLOW_2:def 6;
hence
y <= z
by YELLOW_2:55;
verum
end;
hence
rng (Infs ) is directed
by WAYBEL_0:def 1; verum