let S, T be sup-Semilattice; :: thesis: for f being Function of S,T holds

( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

let f be Function of S,T; :: thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

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

thus ( f is join-preserving implies for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving )

for z, y being Element of S holds f preserves_sup_of {z,y}

( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

let f be Function of S,T; :: thesis: ( f is join-preserving iff for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) )

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

thus ( f is join-preserving implies for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) :: thesis: ( ( for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y) ) implies f is join-preserving )

proof

assume A5:
for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)
; :: thesis: f is join-preserving
assume A2:
f is join-preserving
; :: thesis: for x, y being Element of S holds f . (x "\/" y) = (f . x) "\/" (f . y)

let z, y be Element of S; :: thesis: f . (z "\/" y) = (f . z) "\/" (f . y)

A3: f preserves_sup_of {z,y} by A2;

A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_sup_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:20;

thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41

.= sup {(f . z),(f . y)} by A4, A3

.= (f . z) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum

end;let z, y be Element of S; :: thesis: f . (z "\/" y) = (f . z) "\/" (f . y)

A3: f preserves_sup_of {z,y} by A2;

A4: ( f .: {z,y} = {(f . z),(f . y)} & ex_sup_of {z,y},S ) by A1, FUNCT_1:60, YELLOW_0:20;

thus f . (z "\/" y) = f . (sup {z,y}) by YELLOW_0:41

.= sup {(f . z),(f . y)} by A4, A3

.= (f . z) "\/" (f . y) by YELLOW_0:41 ; :: thesis: verum

for z, y being Element of S holds f preserves_sup_of {z,y}

proof

hence
f is join-preserving
; :: thesis: verum
let z, y be Element of S; :: thesis: f preserves_sup_of {z,y}

A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60;

then A7: ( ex_sup_of {z,y},S implies ex_sup_of f .: {z,y},T ) by YELLOW_0:20;

sup (f .: {z,y}) = (f . z) "\/" (f . y) by A6, YELLOW_0:41

.= f . (z "\/" y) by A5

.= f . (sup {z,y}) by YELLOW_0:41 ;

hence f preserves_sup_of {z,y} by A7; :: thesis: verum

end;A6: f .: {z,y} = {(f . z),(f . y)} by A1, FUNCT_1:60;

then A7: ( ex_sup_of {z,y},S implies ex_sup_of f .: {z,y},T ) by YELLOW_0:20;

sup (f .: {z,y}) = (f . z) "\/" (f . y) by A6, YELLOW_0:41

.= f . (z "\/" y) by A5

.= f . (sup {z,y}) by YELLOW_0:41 ;

hence f preserves_sup_of {z,y} by A7; :: thesis: verum