let S, T be non empty RelStr ; for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
let f be Function of S,T; ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
hereby ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) implies f is isomorphic )
assume A1:
f is
isomorphic
;
( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )hence
f is
one-to-one
by Def38;
( rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )consider g being
Function of
T,
S such that A2:
g = f "
and A3:
g is
monotone
by A1, Def38;
A4:
(
f is
one-to-one &
f is
monotone )
by A1, Def38;
then
rng f = dom g
by A2, FUNCT_1:33;
hence
rng f = the
carrier of
T
by FUNCT_2:def 1;
for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )let x,
y be
Element of
S;
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )thus
(
x <= y implies
f . x <= f . y )
by A4;
( f . x <= f . y implies x <= y )assume A5:
f . x <= f . y
;
x <= yA6:
g . (f . x) = x
by A2, A4, FUNCT_2:26;
g . (f . y) = y
by A2, A4, FUNCT_2:26;
hence
x <= y
by A3, A5, A6;
verum
end;
assume that
A7:
f is one-to-one
and
A8:
rng f = the carrier of T
and
A9:
for x, y being Element of S holds
( x <= y iff f . x <= f . y )
; f is isomorphic
per cases
( ( not S is empty & not T is empty ) or S is empty or T is empty )
;
WAYBEL_0:def 38case
( not
S is
empty & not
T is
empty )
;
( f is one-to-one & f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) )thus
f is
one-to-one
by A7;
( f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) )thus
for
x,
y being
Element of
S st
x <= y holds
for
a,
b being
Element of
T st
a = f . x &
b = f . y holds
a <= b
by A9;
ORDERS_3:def 5 ex g being Function of T,S st
( g = f " & g is monotone )reconsider g =
f " as
Function of
T,
S by A7, A8, FUNCT_2:25;
take
g
;
( g = f " & g is monotone )thus
g = f "
;
g is monotone let x,
y be
Element of
T;
ORDERS_3:def 5 ( not x <= y or for b1, b2 being Element of the carrier of S holds
( not b1 = g . x or not b2 = g . y or b1 <= b2 ) )consider a being
object such that A10:
a in dom f
and A11:
x = f . a
by A8, FUNCT_1:def 3;
consider b being
object such that A12:
b in dom f
and A13:
y = f . b
by A8, FUNCT_1:def 3;
reconsider a =
a,
b =
b as
Element of
S by A10, A12;
A14:
g . x = a
by A7, A11, FUNCT_2:26;
g . y = b
by A7, A13, FUNCT_2:26;
hence
( not
x <= y or for
b1,
b2 being
Element of the
carrier of
S holds
( not
b1 = g . x or not
b2 = g . y or
b1 <= b2 ) )
by A9, A11, A13, A14;
verum end;