let S, T be complete LATTICE; :: thesis: for f being sups-preserving Function of S,T st T is meet-continuous & f is meet-preserving & f is V27() holds

S is meet-continuous

let f be sups-preserving Function of S,T; :: thesis: ( T is meet-continuous & f is meet-preserving & f is V27() implies S is meet-continuous )

assume that

A1: T is meet-continuous and

A2: ( f is meet-preserving & f is V27() ) ; :: thesis: S is meet-continuous

S is satisfying_MC

S is meet-continuous

let f be sups-preserving Function of S,T; :: thesis: ( T is meet-continuous & f is meet-preserving & f is V27() implies S is meet-continuous )

assume that

A1: T is meet-continuous and

A2: ( f is meet-preserving & f is V27() ) ; :: thesis: S is meet-continuous

S is satisfying_MC

proof

hence
S is meet-continuous
; :: thesis: verum
let x be Element of S; :: according to WAYBEL_2:def 6 :: thesis: for b_{1} being Element of bool the carrier of S holds x "/\" ("\/" (b_{1},S)) = "\/" (({x} "/\" b_{1}),S)

let D be non empty directed Subset of S; :: thesis: x "/\" ("\/" (D,S)) = "\/" (({x} "/\" D),S)

A3: ( ex_sup_of D,S & f preserves_sup_of D ) by WAYBEL_0:75, WAYBEL_0:def 33;

reconsider Y = {x} as non empty directed Subset of S by WAYBEL_0:5;

A4: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0:def 33;

reconsider X = f .: D as directed Subset of T by Lm1, YELLOW_2:15;

A5: dom f = the carrier of S by FUNCT_2:def 1;

A6: {(f . x)} "/\" (f .: D) = { ((f . x) "/\" y) where y is Element of T : y in f .: D } by YELLOW_4:42;

A7: {(f . x)} "/\" (f .: D) c= f .: ({x} "/\" D)

A15: f .: ({x} "/\" D) c= {(f . x)} "/\" (f .: D)

.= (f . x) "/\" (sup X) by A3

.= sup ({(f . x)} "/\" X) by A1, WAYBEL_2:def 6

.= sup (f .: ({x} "/\" D)) by A7, A15, XBOOLE_0:def 10

.= f . (sup ({x} "/\" D)) by A4 ;

hence x "/\" (sup D) = sup ({x} "/\" D) by A2; :: thesis: verum

end;let D be non empty directed Subset of S; :: thesis: x "/\" ("\/" (D,S)) = "\/" (({x} "/\" D),S)

A3: ( ex_sup_of D,S & f preserves_sup_of D ) by WAYBEL_0:75, WAYBEL_0:def 33;

reconsider Y = {x} as non empty directed Subset of S by WAYBEL_0:5;

A4: ( ex_sup_of Y "/\" D,S & f preserves_sup_of {x} "/\" D ) by WAYBEL_0:75, WAYBEL_0:def 33;

reconsider X = f .: D as directed Subset of T by Lm1, YELLOW_2:15;

A5: dom f = the carrier of S by FUNCT_2:def 1;

A6: {(f . x)} "/\" (f .: D) = { ((f . x) "/\" y) where y is Element of T : y in f .: D } by YELLOW_4:42;

A7: {(f . x)} "/\" (f .: D) c= f .: ({x} "/\" D)

proof

A14:
{x} "/\" D = { (x "/\" y) where y is Element of S : y in D }
by YELLOW_4:42;
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in {(f . x)} "/\" (f .: D) or p in f .: ({x} "/\" D) )

assume p in {(f . x)} "/\" (f .: D) ; :: thesis: p in f .: ({x} "/\" D)

then consider y being Element of T such that

A8: p = (f . x) "/\" y and

A9: y in f .: D by A6;

consider k being object such that

A10: k in dom f and

A11: k in D and

A12: y = f . k by A9, FUNCT_1:def 6;

reconsider k = k as Element of S by A10;

x "/\" k in { (x "/\" a) where a is Element of S : a in D } by A11;

then A13: x "/\" k in {x} "/\" D by YELLOW_4:42;

f preserves_inf_of {x,k} by A2;

then p = f . (x "/\" k) by A8, A12, YELLOW_3:8;

hence p in f .: ({x} "/\" D) by A5, A13, FUNCT_1:def 6; :: thesis: verum

end;assume p in {(f . x)} "/\" (f .: D) ; :: thesis: p in f .: ({x} "/\" D)

then consider y being Element of T such that

A8: p = (f . x) "/\" y and

A9: y in f .: D by A6;

consider k being object such that

A10: k in dom f and

A11: k in D and

A12: y = f . k by A9, FUNCT_1:def 6;

reconsider k = k as Element of S by A10;

x "/\" k in { (x "/\" a) where a is Element of S : a in D } by A11;

then A13: x "/\" k in {x} "/\" D by YELLOW_4:42;

f preserves_inf_of {x,k} by A2;

then p = f . (x "/\" k) by A8, A12, YELLOW_3:8;

hence p in f .: ({x} "/\" D) by A5, A13, FUNCT_1:def 6; :: thesis: verum

A15: f .: ({x} "/\" D) c= {(f . x)} "/\" (f .: D)

proof

f . (x "/\" (sup D)) =
(f . x) "/\" (f . (sup D))
by A2, Th1
let p be object ; :: according to TARSKI:def 3 :: thesis: ( not p in f .: ({x} "/\" D) or p in {(f . x)} "/\" (f .: D) )

assume p in f .: ({x} "/\" D) ; :: thesis: p in {(f . x)} "/\" (f .: D)

then consider m being object such that

A16: m in dom f and

A17: m in {x} "/\" D and

A18: p = f . m by FUNCT_1:def 6;

reconsider m = m as Element of S by A16;

consider a being Element of S such that

A19: m = x "/\" a and

A20: a in D by A14, A17;

reconsider fa = f . a as Element of T ;

f preserves_inf_of {x,a} by A2;

then A21: p = (f . x) "/\" fa by A18, A19, YELLOW_3:8;

fa in f .: D by A5, A20, FUNCT_1:def 6;

hence p in {(f . x)} "/\" (f .: D) by A6, A21; :: thesis: verum

end;assume p in f .: ({x} "/\" D) ; :: thesis: p in {(f . x)} "/\" (f .: D)

then consider m being object such that

A16: m in dom f and

A17: m in {x} "/\" D and

A18: p = f . m by FUNCT_1:def 6;

reconsider m = m as Element of S by A16;

consider a being Element of S such that

A19: m = x "/\" a and

A20: a in D by A14, A17;

reconsider fa = f . a as Element of T ;

f preserves_inf_of {x,a} by A2;

then A21: p = (f . x) "/\" fa by A18, A19, YELLOW_3:8;

fa in f .: D by A5, A20, FUNCT_1:def 6;

hence p in {(f . x)} "/\" (f .: D) by A6, A21; :: thesis: verum

.= (f . x) "/\" (sup X) by A3

.= sup ({(f . x)} "/\" X) by A1, WAYBEL_2:def 6

.= sup (f .: ({x} "/\" D)) by A7, A15, XBOOLE_0:def 10

.= f . (sup ({x} "/\" D)) by A4 ;

hence x "/\" (sup D) = sup ({x} "/\" D) by A2; :: thesis: verum