set IT = Y |^ X;
now for x, y being Element of (Y |^ X) st x <= y & y <= x holds
x = ylet x,
y be
Element of
(Y |^ X);
( x <= y & y <= x implies x = y )reconsider x19 =
x,
y19 =
y as
Function of
X, the
carrier of
Y by Lm5;
reconsider x1 =
x,
y1 =
y as
Element of
(product (X --> Y)) ;
assume that A1:
x <= y
and A2:
y <= x
;
x = y
y1 in the
carrier of
(product (X --> Y))
;
then
y1 in product (Carrier (X --> Y))
by Def4;
then consider f1,
g1 being
Function such that A3:
(
f1 = y1 &
g1 = x1 )
and A4:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> Y) . i &
xi = f1 . i &
yi = g1 . i &
xi <= yi )
by A2, Def4;
x1 in the
carrier of
(product (X --> Y))
;
then
x1 in product (Carrier (X --> Y))
by Def4;
then consider f,
g being
Function such that A5:
(
f = x1 &
g = y1 )
and A6:
for
i being
object st
i in X holds
ex
R being
RelStr ex
xi,
yi being
Element of
R st
(
R = (X --> Y) . i &
xi = f . i &
yi = g . i &
xi <= yi )
by A1, Def4;
A7:
now for i being object st i in X holds
x19 . i = y19 . ilet i be
object ;
( i in X implies x19 . i = y19 . i )assume A8:
i in X
;
x19 . i = y19 . ithen consider R2 being
RelStr ,
xi2,
yi2 being
Element of
R2 such that A9:
R2 = (X --> Y) . i
and A10:
(
xi2 = f1 . i &
yi2 = g1 . i &
xi2 <= yi2 )
by A4;
A11:
Y = R2
by A8, A9, FUNCOP_1:7;
consider R1 being
RelStr ,
xi1,
yi1 being
Element of
R1 such that A12:
R1 = (X --> Y) . i
and A13:
(
xi1 = f . i &
yi1 = g . i &
xi1 <= yi1 )
by A6, A8;
Y = R1
by A8, A12, FUNCOP_1:7;
hence
x19 . i = y19 . i
by A5, A3, A13, A10, A11, ORDERS_2:2;
verum end;
(
dom x19 = X &
dom y19 = X )
by FUNCT_2:def 1;
hence
x = y
by A7, FUNCT_1:2;
verum end;
hence
Y |^ X is antisymmetric
by YELLOW_0:def 3; verum