let L be complete LATTICE; :: thesis: ( L is continuous implies for S being non empty Poset st ex g being Function of L,S st

( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds

S is continuous LATTICE )

assume A1: L is continuous ; :: thesis: for S being non empty Poset st ex g being Function of L,S st

( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds

S is continuous LATTICE

let S be non empty Poset; :: thesis: ( ex g being Function of L,S st

( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE )

given g being Function of L,S such that A2: ( g is infs-preserving & g is directed-sups-preserving ) and

A3: g is onto ; :: thesis: S is continuous LATTICE

reconsider S9 = S as complete LATTICE by A2, A3, Th29;

for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds

S is continuous LATTICE )

assume A1: L is continuous ; :: thesis: for S being non empty Poset st ex g being Function of L,S st

( g is infs-preserving & g is directed-sups-preserving & g is onto ) holds

S is continuous LATTICE

let S be non empty Poset; :: thesis: ( ex g being Function of L,S st

( g is infs-preserving & g is directed-sups-preserving & g is onto ) implies S is continuous LATTICE )

given g being Function of L,S such that A2: ( g is infs-preserving & g is directed-sups-preserving ) and

A3: g is onto ; :: thesis: S is continuous LATTICE

reconsider S9 = S as complete LATTICE by A2, A3, Th29;

for J being non empty set

for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

proof

hence
S is continuous LATTICE
by Lm9; :: thesis: verum
let J be non empty set ; :: thesis: for K being V9() ManySortedSet of J

for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let F be DoubleIndexedSet of K,S9; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

assume A4: for j being Element of J holds rng (F . j) is directed ; :: thesis: Inf = Sup

consider d being Function of S,L such that

A5: [g,d] is Galois and

for t being Element of S holds d . t is_minimum_of g " (uparrow t) by A2, WAYBEL_1:14;

reconsider dF = (J => d) ** F as DoubleIndexedSet of K,L by Th31;

A6: ( ex_inf_of rng (Sups ),L & g preserves_inf_of rng (Sups ) ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

for t being Element of S holds d . t is_minimum_of g " {t} by A3, A5, WAYBEL_1:22;

then A7: g * d = id S by WAYBEL_1:23;

A8: for f being set st f in dom (Frege dF) holds

rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))

A32: for j being Element of J holds rng (dF . j) is directed

then A34: g preserves_sup_of rng (Infs ) by A2, WAYBEL_0:def 37;

reconsider gdF = (J => g) ** dF as DoubleIndexedSet of K,S ;

A35: ex_sup_of rng (Infs ),L by YELLOW_0:17;

A36: rng (Sups ) c= g .: (rng (Sups ))

.= ((J --> g) ** (J --> d)) ** F by A7, Th30

.= gdF by PBOOLE:140 ;

then Inf = inf (rng (Sups )) by YELLOW_2:def 6

.= inf (g .: (rng (Sups ))) by A36, A41, XBOOLE_0:def 10

.= g . (inf (rng (Sups ))) by A6, WAYBEL_0:def 30

.= g . (Inf ) by YELLOW_2:def 6

.= g . (Sup ) by A1, A32, Lm8

.= g . (sup (rng (Infs ))) by YELLOW_2:def 5

.= sup (g .: (rng (Infs ))) by A34, A35, WAYBEL_0:def 31

.= sup (rng (Infs )) by A24, A18, XBOOLE_0:def 10

.= Sup by YELLOW_2:def 5 ;

hence Inf = Sup ; :: thesis: verum

end;for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let K be V9() ManySortedSet of J; :: thesis: for F being DoubleIndexedSet of K,S9 st ( for j being Element of J holds rng (F . j) is directed ) holds

Inf = Sup

let F be DoubleIndexedSet of K,S9; :: thesis: ( ( for j being Element of J holds rng (F . j) is directed ) implies Inf = Sup )

assume A4: for j being Element of J holds rng (F . j) is directed ; :: thesis: Inf = Sup

consider d being Function of S,L such that

A5: [g,d] is Galois and

for t being Element of S holds d . t is_minimum_of g " (uparrow t) by A2, WAYBEL_1:14;

reconsider dF = (J => d) ** F as DoubleIndexedSet of K,L by Th31;

A6: ( ex_inf_of rng (Sups ),L & g preserves_inf_of rng (Sups ) ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

for t being Element of S holds d . t is_minimum_of g " {t} by A3, A5, WAYBEL_1:22;

then A7: g * d = id S by WAYBEL_1:23;

A8: for f being set st f in dom (Frege dF) holds

rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))

proof

A18:
rng (Infs ) c= g .: (rng (Infs ))
let f be set ; :: thesis: ( f in dom (Frege dF) implies rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) )

assume A9: f in dom (Frege dF) ; :: thesis: rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))

then reconsider f = f as Element of product (doms dF) ;

A10: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

A11: dom ((Frege dF) . f) = dom dF by A9, Th8

.= J by PARTFUN1:def 2 ;

then rng ((Frege dF) . f) c= dom g ;

then A17: dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f) by RELAT_1:27;

dom ((Frege F) . f) = dom F by A9, A10, Th8

.= J by PARTFUN1:def 2 ;

then rng ((Frege F) . f) = rng (g * ((Frege dF) . f)) by A11, A17, A12, FUNCT_1:2

.= g .: (rng ((Frege dF) . f)) by RELAT_1:127 ;

hence rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) ; :: thesis: verum

end;assume A9: f in dom (Frege dF) ; :: thesis: rng ((Frege F) . f) = g .: (rng ((Frege dF) . f))

then reconsider f = f as Element of product (doms dF) ;

A10: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

A11: dom ((Frege dF) . f) = dom dF by A9, Th8

.= J by PARTFUN1:def 2 ;

A12: now :: thesis: for i being object st i in J holds

(g * ((Frege dF) . f)) . i = ((Frege F) . f) . i

dom g = the carrier of L
by FUNCT_2:def 1;(g * ((Frege dF) . f)) . i = ((Frege F) . f) . i

let i be object ; :: thesis: ( i in J implies (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i )

assume A13: i in J ; :: thesis: (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i

then reconsider j = i as Element of J ;

A14: j in dom F by A13, PARTFUN1:def 2;

A15: j in dom dF by A13, PARTFUN1:def 2;

then f . j in dom (dF . j) by A9, Th9;

then f . j in dom (((J => d) . j) * (F . j)) by MSUALG_3:2;

then A16: f . j in dom (d * (F . j)) ;

(g * ((Frege dF) . f)) . j = g . (((Frege dF) . f) . j) by A11, FUNCT_1:13

.= g . ((dF . j) . (f . j)) by A9, A15, Th9

.= g . ((((J => d) . j) * (F . j)) . (f . j)) by MSUALG_3:2

.= g . ((d * (F . j)) . (f . j))

.= (g * (d * (F . j))) . (f . j) by A16, FUNCT_1:13

.= ((id the carrier of S) * (F . j)) . (f . j) by A7, RELAT_1:36

.= (F . j) . (f . j) by FUNCT_2:17

.= ((Frege F) . f) . j by A9, A10, A14, Th9 ;

hence (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i ; :: thesis: verum

end;assume A13: i in J ; :: thesis: (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i

then reconsider j = i as Element of J ;

A14: j in dom F by A13, PARTFUN1:def 2;

A15: j in dom dF by A13, PARTFUN1:def 2;

then f . j in dom (dF . j) by A9, Th9;

then f . j in dom (((J => d) . j) * (F . j)) by MSUALG_3:2;

then A16: f . j in dom (d * (F . j)) ;

(g * ((Frege dF) . f)) . j = g . (((Frege dF) . f) . j) by A11, FUNCT_1:13

.= g . ((dF . j) . (f . j)) by A9, A15, Th9

.= g . ((((J => d) . j) * (F . j)) . (f . j)) by MSUALG_3:2

.= g . ((d * (F . j)) . (f . j))

.= (g * (d * (F . j))) . (f . j) by A16, FUNCT_1:13

.= ((id the carrier of S) * (F . j)) . (f . j) by A7, RELAT_1:36

.= (F . j) . (f . j) by FUNCT_2:17

.= ((Frege F) . f) . j by A9, A10, A14, Th9 ;

hence (g * ((Frege dF) . f)) . i = ((Frege F) . f) . i ; :: thesis: verum

then rng ((Frege dF) . f) c= dom g ;

then A17: dom (g * ((Frege dF) . f)) = dom ((Frege dF) . f) by RELAT_1:27;

dom ((Frege F) . f) = dom F by A9, A10, Th8

.= J by PARTFUN1:def 2 ;

then rng ((Frege F) . f) = rng (g * ((Frege dF) . f)) by A11, A17, A12, FUNCT_1:2

.= g .: (rng ((Frege dF) . f)) by RELAT_1:127 ;

hence rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) ; :: thesis: verum

proof

A24:
g .: (rng (Infs )) c= rng (Infs )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Infs ) or y in g .: (rng (Infs )) )

assume y in rng (Infs ) ; :: thesis: y in g .: (rng (Infs ))

then consider f being object such that

A19: f in dom (Frege F) and

A20: y = //\ (((Frege F) . f),S) by Th13;

reconsider f = f as Element of product (doms F) by A19;

reconsider f9 = f as Element of product (doms dF) by Th32;

set X = rng ((Frege dF) . f9);

A21: ( g preserves_inf_of rng ((Frege dF) . f9) & ex_inf_of rng ((Frege dF) . f9),L ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

A22: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

then rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A19;

then y = "/\" ((g .: (rng ((Frege dF) . f))),S) by A20, YELLOW_2:def 6;

then A23: y = g . (inf (rng ((Frege dF) . f9))) by A21, WAYBEL_0:def 30

.= g . (Inf ) by YELLOW_2:def 6 ;

Inf in rng (Infs ) by A19, A22, Th13;

hence y in g .: (rng (Infs )) by A23, FUNCT_2:35; :: thesis: verum

end;assume y in rng (Infs ) ; :: thesis: y in g .: (rng (Infs ))

then consider f being object such that

A19: f in dom (Frege F) and

A20: y = //\ (((Frege F) . f),S) by Th13;

reconsider f = f as Element of product (doms F) by A19;

reconsider f9 = f as Element of product (doms dF) by Th32;

set X = rng ((Frege dF) . f9);

A21: ( g preserves_inf_of rng ((Frege dF) . f9) & ex_inf_of rng ((Frege dF) . f9),L ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

A22: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

then rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A19;

then y = "/\" ((g .: (rng ((Frege dF) . f))),S) by A20, YELLOW_2:def 6;

then A23: y = g . (inf (rng ((Frege dF) . f9))) by A21, WAYBEL_0:def 30

.= g . (Inf ) by YELLOW_2:def 6 ;

Inf in rng (Infs ) by A19, A22, Th13;

hence y in g .: (rng (Infs )) by A23, FUNCT_2:35; :: thesis: verum

proof

A31:
d is monotone
by A5, WAYBEL_1:8;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: (rng (Infs )) or y in rng (Infs ) )

assume y in g .: (rng (Infs )) ; :: thesis: y in rng (Infs )

then consider x being object such that

x in the carrier of L and

A25: x in rng (Infs ) and

A26: y = g . x by FUNCT_2:64;

consider f being object such that

A27: f in dom (Frege dF) and

A28: x = //\ (((Frege dF) . f),L) by A25, Th13;

reconsider f = f as Element of product (doms dF) by A27;

set X = rng ((Frege dF) . f);

( g preserves_inf_of rng ((Frege dF) . f) & ex_inf_of rng ((Frege dF) . f),L ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

then inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f))) by WAYBEL_0:def 30;

then A29: y = inf (g .: (rng ((Frege dF) . f))) by A26, A28, YELLOW_2:def 6;

A30: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

reconsider f9 = f as Element of product (doms F) by Th32;

rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A27;

then y = Inf by A29, YELLOW_2:def 6;

hence y in rng (Infs ) by A27, A30, Th13; :: thesis: verum

end;assume y in g .: (rng (Infs )) ; :: thesis: y in rng (Infs )

then consider x being object such that

x in the carrier of L and

A25: x in rng (Infs ) and

A26: y = g . x by FUNCT_2:64;

consider f being object such that

A27: f in dom (Frege dF) and

A28: x = //\ (((Frege dF) . f),L) by A25, Th13;

reconsider f = f as Element of product (doms dF) by A27;

set X = rng ((Frege dF) . f);

( g preserves_inf_of rng ((Frege dF) . f) & ex_inf_of rng ((Frege dF) . f),L ) by A2, WAYBEL_0:def 32, YELLOW_0:17;

then inf (g .: (rng ((Frege dF) . f))) = g . (inf (rng ((Frege dF) . f))) by WAYBEL_0:def 30;

then A29: y = inf (g .: (rng ((Frege dF) . f))) by A26, A28, YELLOW_2:def 6;

A30: dom (Frege dF) = product (doms dF) by PARTFUN1:def 2

.= product (doms F) by Th32

.= dom (Frege F) by PARTFUN1:def 2 ;

reconsider f9 = f as Element of product (doms F) by Th32;

rng ((Frege F) . f) = g .: (rng ((Frege dF) . f)) by A8, A27;

then y = Inf by A29, YELLOW_2:def 6;

hence y in rng (Infs ) by A27, A30, Th13; :: thesis: verum

A32: for j being Element of J holds rng (dF . j) is directed

proof

then
( rng (Infs ) is directed & not rng (Infs ) is empty )
by Th27;
let j be Element of J; :: thesis: rng (dF . j) is directed

(J => d) . j = d ;

then A33: rng (dF . j) = rng (d * (F . j)) by MSUALG_3:2

.= d .: (rng (F . j)) by RELAT_1:127 ;

rng (F . j) is directed by A4;

hence rng (dF . j) is directed by A31, A33, YELLOW_2:15; :: thesis: verum

end;(J => d) . j = d ;

then A33: rng (dF . j) = rng (d * (F . j)) by MSUALG_3:2

.= d .: (rng (F . j)) by RELAT_1:127 ;

rng (F . j) is directed by A4;

hence rng (dF . j) is directed by A31, A33, YELLOW_2:15; :: thesis: verum

then A34: g preserves_sup_of rng (Infs ) by A2, WAYBEL_0:def 37;

reconsider gdF = (J => g) ** dF as DoubleIndexedSet of K,S ;

A35: ex_sup_of rng (Infs ),L by YELLOW_0:17;

A36: rng (Sups ) c= g .: (rng (Sups ))

proof

A41:
g .: (rng (Sups )) c= rng (Sups )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (Sups ) or y in g .: (rng (Sups )) )

assume y in rng (Sups ) ; :: thesis: y in g .: (rng (Sups ))

then consider j being Element of J such that

A37: y = Sup by Th14;

gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2

.= g * (dF . j) ;

then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;

then A38: y = sup (g .: (rng (dF . j))) by A37, YELLOW_2:def 5;

rng (dF . j) is directed by A32;

then A39: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def 37;

ex_sup_of rng (dF . j),L by YELLOW_0:17;

then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A39, WAYBEL_0:def 31;

then A40: y = g . (Sup ) by A38, YELLOW_2:def 5;

Sup in rng (Sups ) by Th14;

hence y in g .: (rng (Sups )) by A40, FUNCT_2:35; :: thesis: verum

end;assume y in rng (Sups ) ; :: thesis: y in g .: (rng (Sups ))

then consider j being Element of J such that

A37: y = Sup by Th14;

gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2

.= g * (dF . j) ;

then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;

then A38: y = sup (g .: (rng (dF . j))) by A37, YELLOW_2:def 5;

rng (dF . j) is directed by A32;

then A39: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def 37;

ex_sup_of rng (dF . j),L by YELLOW_0:17;

then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A39, WAYBEL_0:def 31;

then A40: y = g . (Sup ) by A38, YELLOW_2:def 5;

Sup in rng (Sups ) by Th14;

hence y in g .: (rng (Sups )) by A40, FUNCT_2:35; :: thesis: verum

proof

F =
(id (J --> the carrier of S)) ** F
by MSUALG_3:4
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in g .: (rng (Sups )) or y in rng (Sups ) )

assume y in g .: (rng (Sups )) ; :: thesis: y in rng (Sups )

then consider x being object such that

x in the carrier of L and

A42: x in rng (Sups ) and

A43: y = g . x by FUNCT_2:64;

consider j being Element of J such that

A44: x = Sup by A42, Th14;

rng (dF . j) is directed by A32;

then A45: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def 37;

ex_sup_of rng (dF . j),L by YELLOW_0:17;

then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A45, WAYBEL_0:def 31;

then A46: y = sup (g .: (rng (dF . j))) by A43, A44, YELLOW_2:def 5;

gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2

.= g * (dF . j) ;

then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;

then y = Sup by A46, YELLOW_2:def 5;

hence y in rng (Sups ) by Th14; :: thesis: verum

end;assume y in g .: (rng (Sups )) ; :: thesis: y in rng (Sups )

then consider x being object such that

x in the carrier of L and

A42: x in rng (Sups ) and

A43: y = g . x by FUNCT_2:64;

consider j being Element of J such that

A44: x = Sup by A42, Th14;

rng (dF . j) is directed by A32;

then A45: g preserves_sup_of rng (dF . j) by A2, WAYBEL_0:def 37;

ex_sup_of rng (dF . j),L by YELLOW_0:17;

then sup (g .: (rng (dF . j))) = g . (sup (rng (dF . j))) by A45, WAYBEL_0:def 31;

then A46: y = sup (g .: (rng (dF . j))) by A43, A44, YELLOW_2:def 5;

gdF . j = ((J => g) . j) * (dF . j) by MSUALG_3:2

.= g * (dF . j) ;

then rng (gdF . j) = g .: (rng (dF . j)) by RELAT_1:127;

then y = Sup by A46, YELLOW_2:def 5;

hence y in rng (Sups ) by Th14; :: thesis: verum

.= ((J --> g) ** (J --> d)) ** F by A7, Th30

.= gdF by PBOOLE:140 ;

then Inf = inf (rng (Sups )) by YELLOW_2:def 6

.= inf (g .: (rng (Sups ))) by A36, A41, XBOOLE_0:def 10

.= g . (inf (rng (Sups ))) by A6, WAYBEL_0:def 30

.= g . (Inf ) by YELLOW_2:def 6

.= g . (Sup ) by A1, A32, Lm8

.= g . (sup (rng (Infs ))) by YELLOW_2:def 5

.= sup (g .: (rng (Infs ))) by A34, A35, WAYBEL_0:def 31

.= sup (rng (Infs )) by A24, A18, XBOOLE_0:def 10

.= Sup by YELLOW_2:def 5 ;

hence Inf = Sup ; :: thesis: verum