let L1, L2 be non empty RelStr ; 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; 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; 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; ( f is isomorphic implies ( x is_>=_than X iff f . x is_>=_than f .: X ) )
assume A1:
f is isomorphic
; ( x is_>=_than X iff f . x is_>=_than f .: X )
hence
( x is_>=_than X implies f . x is_>=_than f .: X )
by YELLOW_2:14; ( f . x is_>=_than f .: X implies x is_>=_than X )
thus
( f . x is_>=_than f .: X implies x is_>=_than X )
verumproof
reconsider g =
f " as
Function of
L2,
L1 by A1, WAYBEL_0:67;
assume A2:
f . x is_>=_than f .: X
;
x is_>=_than X
g is
isomorphic
by A1, WAYBEL_0:68;
then A3:
g . (f . x) is_>=_than g .: (f .: X)
by A2, YELLOW_2:14;
A4:
f " (f .: X) c= X
by A1, FUNCT_1:82;
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:76;
x in the
carrier of
L1
;
then A6:
x in dom f
by FUNCT_2:def 1;
g .: (f .: X) =
f " (f .: X)
by A1, FUNCT_1:85
.=
X
by A4, A5, XBOOLE_0:def 10
;
hence
x is_>=_than X
by A1, A6, A3, FUNCT_1:34;
verum
end;