let R be reflexive antisymmetric RelStr ; :: thesis: for S being RelStr holds
( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )
let S be RelStr ; :: thesis: ( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )
A1:
now assume A2:
S embeds R
;
:: thesis: ex f being Function of R,S st
( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )then consider f being
Function of
R,
S such that
f is
one-to-one
and A3:
for
x,
y being
Element of
R holds
(
[x,y] in the
InternalRel of
R iff
[(f . x),(f . y)] in the
InternalRel of
S )
by NECKLACE:def 2;
take f =
f;
:: thesis: ( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )thus
( ex
f being
Function of
R,
S st
for
x,
y being
Element of
R holds
(
[x,y] in the
InternalRel of
R iff
[(f . x),(f . y)] in the
InternalRel of
S ) iff
S embeds R )
by A2, A3;
:: thesis: verum end;
now assume
ex
f being
Function of
R,
S st
for
x,
y being
Element of
R holds
(
[x,y] in the
InternalRel of
R iff
[(f . x),(f . y)] in the
InternalRel of
S )
;
:: thesis: S embeds Rthen consider f being
Function of
R,
S such that A4:
for
x,
y being
Element of
R holds
(
[x,y] in the
InternalRel of
R iff
[(f . x),(f . y)] in the
InternalRel of
S )
;
for
x1,
x2 being
set st
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 holds
x1 = x2
proof
let x1,
x2 be
set ;
:: thesis: ( x1 in dom f & x2 in dom f & f . x1 = f . x2 implies x1 = x2 )
assume A5:
(
x1 in dom f &
x2 in dom f &
f . x1 = f . x2 )
;
:: thesis: x1 = x2
then reconsider x1 =
x1,
x2 =
x2 as
Element of
R ;
A6:
the
InternalRel of
R is_reflexive_in the
carrier of
R
by ORDERS_2:def 4;
then
[x1,x1] in the
InternalRel of
R
by A5, RELAT_2:def 1;
then
[(f . x1),(f . x2)] in the
InternalRel of
S
by A4, A5;
then
[x1,x2] in the
InternalRel of
R
by A4;
then A7:
x1 <= x2
by ORDERS_2:def 9;
[x2,x2] in the
InternalRel of
R
by A5, A6, RELAT_2:def 1;
then
[(f . x2),(f . x1)] in the
InternalRel of
S
by A4, A5;
then
[x2,x1] in the
InternalRel of
R
by A4;
then
x2 <= x1
by ORDERS_2:def 9;
hence
x1 = x2
by A7, ORDERS_2:25;
:: thesis: verum
end; then
f is
one-to-one
by FUNCT_1:def 8;
hence
S embeds R
by A4, NECKLACE:def 2;
:: thesis: verum end;
hence
( ex f being Function of R,S st
for x, y being Element of R holds
( [x,y] in the InternalRel of R iff [(f . x),(f . y)] in the InternalRel of S ) iff S embeds R )
by A1; :: thesis: verum