let L1, L2 be non empty RelStr ; :: thesis: for X being Subset of L1
for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let X be Subset of L1; :: thesis: for x being Element of L1
for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let x be Element of L1; :: thesis: for f being Function of L1,L2 st f is isomorphic holds
( x is_>=_than X iff f . x is_>=_than f .: X )
let f be Function of L1,L2; :: thesis: ( f is isomorphic implies ( x is_>=_than X iff f . x is_>=_than f .: X ) )
assume A1:
f is isomorphic
; :: thesis: ( x is_>=_than X iff f . x is_>=_than f .: X )
then
f is monotone
;
hence
( x is_>=_than X implies f . x is_>=_than f .: X )
by YELLOW_2:16; :: thesis: ( f . x is_>=_than f .: X implies x is_>=_than X )
A2:
f is one-to-one
by A1;
thus
( f . x is_>=_than f .: X implies x is_>=_than X )
:: thesis: verumproof
reconsider g =
f " as
Function of
L2,
L1 by A1, WAYBEL_0:67;
g is
isomorphic
by A1, WAYBEL_0:68;
then A3:
g is
monotone
;
A4:
f " (f .: X) c= X
by A2, FUNCT_1:152;
( not the
carrier of
L2 is
empty &
X c= the
carrier of
L1 )
;
then
X c= dom f
by FUNCT_2:def 1;
then A5:
X c= f " (f .: X)
by FUNCT_1:146;
A6:
g .: (f .: X) =
f " (f .: X)
by A2, FUNCT_1:155
.=
X
by A4, A5, XBOOLE_0:def 10
;
(
x in the
carrier of
L1 & not the
carrier of
L2 is
empty )
;
then A7:
x in dom f
by FUNCT_2:def 1;
assume
f . x is_>=_than f .: X
;
:: thesis: x is_>=_than X
then
g . (f . x) is_>=_than g .: (f .: X)
by A3, YELLOW_2:16;
hence
x is_>=_than X
by A2, A6, A7, FUNCT_1:56;
:: thesis: verum
end;