let L be complete LATTICE; :: thesis: 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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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 )

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 ; :: thesis: 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; :: thesis: 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; :: thesis: ( ( 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 ; :: thesis: 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

hence
rng (Infs ) is directed
by WAYBEL_0:def 1; :: thesis: verum
let x, y be Element of L; :: thesis: ( 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 ) ; :: thesis: 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 S_{1}[ 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 )

ex k being object st

( k in union (rng K) & S_{1}[j,k] )

A22: dom f = J and

rng f c= union (rng K) and

A23: for j being object st j in J holds

S_{1}[j,f . j]
from FUNCT_1:sch 6(A20);

.= 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 ; :: thesis: ( z in rng (Infs ) & x <= z & y <= z )

thus z in rng (Infs ) by A26, Th13; :: thesis: ( x <= z & y <= z )

A27: x = "/\" ((rng ((Frege F) . g)),L) by A7, YELLOW_2:def 6;

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;

end;( z in rng (Infs ) & x <= z & y <= z ) )

assume that

A2: x in rng (Infs ) and

A3: y in rng (Infs ) ; :: thesis: 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 S

( ( 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

A20:
for j being object st j in J holds
let j be Element of J; :: thesis: 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 ; :: thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k )

thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A17, A19; :: thesis: verum

end;( 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 ; :: thesis: ( G . j <= (F . j) . k & H . j <= (F . j) . k )

thus ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A17, A19; :: thesis: verum

ex k being object st

( k in union (rng K) & S

proof

consider f being Function such that
let j9 be object ; :: thesis: ( j9 in J implies ex k being object st

( k in union (rng K) & S_{1}[j9,k] ) )

assume j9 in J ; :: thesis: ex k being object st

( k in union (rng K) & S_{1}[j9,k] )

then reconsider j = j9 as Element of J ;

consider k being Element of K . j such that

A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9;

take k ; :: thesis: ( k in union (rng K) & S_{1}[j9,k] )

j in J ;

then j in dom K by PARTFUN1:def 2;

then K . j in rng K by FUNCT_1:def 3;

hence k in union (rng K) by TARSKI:def 4; :: thesis: S_{1}[j9,k]

thus S_{1}[j9,k]
by A21; :: thesis: verum

end;( k in union (rng K) & S

assume j9 in J ; :: thesis: ex k being object st

( k in union (rng K) & S

then reconsider j = j9 as Element of J ;

consider k being Element of K . j such that

A21: ( G . j <= (F . j) . k & H . j <= (F . j) . k ) by A9;

take k ; :: thesis: ( k in union (rng K) & S

j in J ;

then j in dom K by PARTFUN1:def 2;

then K . j in rng K by FUNCT_1:def 3;

hence k in union (rng K) by TARSKI:def 4; :: thesis: S

thus S

A22: dom f = J and

rng f c= union (rng K) and

A23: for j being object st j in J holds

S

A24: now :: thesis: for x being object st x in dom (doms F) holds

f . x in (doms F) . x

dom f =
dom F
by A22, PARTFUN1:def 2
f . x in (doms F) . x

let x be object ; :: thesis: ( x in dom (doms F) implies f . x in (doms F) . x )

assume x in dom (doms F) ; :: thesis: f . x in (doms F) . x

then A25: x in dom F by FUNCT_6:59;

then reconsider j = x as Element of J ;

(doms F) . x = dom (F . j) by A25, FUNCT_6:22

.= K . j by FUNCT_2:def 1 ;

hence f . x in (doms F) . x by A23; :: thesis: verum

end;assume x in dom (doms F) ; :: thesis: f . x in (doms F) . x

then A25: x in dom F by FUNCT_6:59;

then reconsider j = x as Element of J ;

(doms F) . x = dom (F . j) by A25, FUNCT_6:22

.= K . j by FUNCT_2:def 1 ;

hence f . x in (doms F) . x by A23; :: thesis: verum

.= 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 ; :: thesis: ( z in rng (Infs ) & x <= z & y <= z )

thus z in rng (Infs ) by A26, Th13; :: thesis: ( x <= z & y <= z )

A27: x = "/\" ((rng ((Frege F) . g)),L) by A7, YELLOW_2:def 6;

now :: thesis: for j being Element of J holds x <= Ff . j

hence
x <= z
by YELLOW_2:55; :: thesis: y <= zlet j be Element of J; :: thesis: x <= Ff . j

A28: j in J ;

then j in dom G by FUNCT_2:def 1;

then A29: G . j in rng G by FUNCT_1:def 3;

j in dom F by A28, PARTFUN1:def 2;

then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;

then A30: G . j <= Ff . j by A23;

x is_<=_than rng G by A27, A8, YELLOW_0:def 10;

then x <= G . j by A29;

hence x <= Ff . j by A30, ORDERS_2:3; :: thesis: verum

end;A28: j in J ;

then j in dom G by FUNCT_2:def 1;

then A29: G . j in rng G by FUNCT_1:def 3;

j in dom F by A28, PARTFUN1:def 2;

then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;

then A30: G . j <= Ff . j by A23;

x is_<=_than rng G by A27, A8, YELLOW_0:def 10;

then x <= G . j by A29;

hence x <= Ff . j by A30, ORDERS_2:3; :: thesis: verum

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;

now :: thesis: for j being Element of J holds y <= Ff . j

hence
y <= z
by YELLOW_2:55; :: thesis: verumlet j be Element of J; :: thesis: y <= Ff . j

A33: j in J ;

then j in dom H by FUNCT_2:def 1;

then A34: H . j in rng H by FUNCT_1:def 3;

j in dom F by A33, PARTFUN1:def 2;

then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;

then A35: H . j <= Ff . j by A23;

y is_<=_than rng H by A32, A31, YELLOW_0:def 10;

then y <= H . j by A34;

hence y <= Ff . j by A35, ORDERS_2:3; :: thesis: verum

end;A33: j in J ;

then j in dom H by FUNCT_2:def 1;

then A34: H . j in rng H by FUNCT_1:def 3;

j in dom F by A33, PARTFUN1:def 2;

then (F . j) . (f . j) = ((Frege F) . f) . j by A26, Th9;

then A35: H . j <= Ff . j by A23;

y is_<=_than rng H by A32, A31, YELLOW_0:def 10;

then y <= H . j by A34;

hence y <= Ff . j by A35, ORDERS_2:3; :: thesis: verum