let S, T be non empty RelStr ; :: thesis: for A being Subset of S
for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let A be Subset of S; :: thesis: for f being Function of S,T st f is isomorphic & ex_sup_of A,S holds
ex_sup_of f .: A,T
let f be Function of S,T; :: thesis: ( f is isomorphic & ex_sup_of A,S implies ex_sup_of f .: A,T )
assume A1: f is isomorphic ; :: thesis: ( not ex_sup_of A,S or ex_sup_of f .: A,T )
A2: f " (f .: A) c= A by A1, FUNCT_1:82;
A3: rng f = [#] T by A1, WAYBEL_0:66;
A4: f /" = f " by A1, TOPS_2:def 4;
given a being Element of S such that A5: A is_<=_than a and
A6: for b being Element of S st A is_<=_than b holds
b >= a and
A7: for c being Element of S st A is_<=_than c & ( for b being Element of S st A is_<=_than b holds
b >= c ) holds
c = a ; :: according to YELLOW_0:def 7 :: thesis: ex_sup_of f .: A,T
take f . a ; :: according to YELLOW_0:def 7 :: thesis: ( f .: A is_<=_than f . a & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
thus f .: A is_<=_than f . a by A1, A5, WAYBEL13:19; :: thesis: ( ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or f . a <= b1 ) ) & ( for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a ) ) )
A8: f /" is isomorphic by A1, Th10;
A9: dom f = the carrier of S by FUNCT_2:def 1;
then A c= f " (f .: A) by FUNCT_1:76;
then A10: f " (f .: A) = A by A2;
hereby :: thesis: for b1 being Element of the carrier of T holds
( not f .: A is_<=_than b1 or ex b2 being Element of the carrier of T st
( f .: A is_<=_than b2 & not b1 <= b2 ) or b1 = f . a )
let b be Element of T; :: thesis: ( f .: A is_<=_than b implies b >= f . a )
assume f .: A is_<=_than b ; :: thesis: b >= f . a
then (f /") .: (f .: A) is_<=_than (f /") . b by A8, WAYBEL13:19;
then f " (f .: A) is_<=_than (f /") . b by A1, A3, TOPS_2:55;
then (f /") . b >= a by A6, A10;
then f . ((f /") . b) >= f . a by A1, WAYBEL_0:66;
hence b >= f . a by A1, A3, A4, FUNCT_1:35; :: thesis: verum
end;
let c be Element of T; :: thesis: ( not f .: A is_<=_than c or ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A11: f .: A is_<=_than c ; :: thesis: ( ex b1 being Element of the carrier of T st
( f .: A is_<=_than b1 & not c <= b1 ) or c = f . a )
assume A12: for b being Element of T st f .: A is_<=_than b holds
b >= c ; :: thesis: c = f . a
A13: for b being Element of S st A is_<=_than b holds
b >= (f /") . c
proof
let b be Element of S; :: thesis: ( A is_<=_than b implies b >= (f /") . c )
assume A is_<=_than b ; :: thesis: b >= (f /") . c
then f .: A is_<=_than f . b by A1, WAYBEL13:19;
then f . b >= c by A12;
then (f /") . (f . b) >= (f /") . c by A8, WAYBEL_0:66;
hence b >= (f /") . c by A1, A4, A9, FUNCT_1:34; :: thesis: verum
end;
(f /") .: (f .: A) is_<=_than (f /") . c by A8, A11, WAYBEL13:19;
then A is_<=_than (f /") . c by A1, A3, A10, TOPS_2:55;
then (f /") . c = a by A7, A13;
hence c = f . a by A1, A3, A4, FUNCT_1:35; :: thesis: verum