let x, y, z be object ; ( ( x <> y & y <> z & z <> x ) iff <*x,y,z*> is one-to-one )
set p = <*x,y,z*>;
A1:
<*x,y,z*> . 1 = x
by FINSEQ_1:45;
A2:
<*x,y,z*> . 3 = z
by FINSEQ_1:45;
thus
( x <> y & y <> z & z <> x implies <*x,y,z*> is one-to-one )
( <*x,y,z*> is one-to-one implies ( x <> y & y <> z & z <> x ) )proof
assume that A3:
x <> y
and A4:
y <> z
and A5:
z <> x
;
<*x,y,z*> is one-to-one
{x,y} /\ {z} = {}
proof
set y1 = the
Element of
{x,y} /\ {z};
assume A6:
not
{x,y} /\ {z} = {}
;
contradiction
then
the
Element of
{x,y} /\ {z} in {x,y}
by XBOOLE_0:def 4;
then A7:
( the
Element of
{x,y} /\ {z} = x or the
Element of
{x,y} /\ {z} = y )
by TARSKI:def 2;
the
Element of
{x,y} /\ {z} in {z}
by A6, XBOOLE_0:def 4;
hence
contradiction
by A4, A5, A7, TARSKI:def 1;
verum
end;
then {} =
(rng <*x,y*>) /\ {z}
by FINSEQ_2:127
.=
(rng <*x,y*>) /\ (rng <*z*>)
by FINSEQ_1:38
;
then A8:
rng <*x,y*> misses rng <*z*>
;
A9:
<*z*> is
one-to-one
by Th91;
<*x,y*> is
one-to-one
by A3, Th92;
then
<*x,y*> ^ <*z*> is
one-to-one
by A8, A9, Th89;
hence
<*x,y,z*> is
one-to-one
by FINSEQ_1:43;
verum
end;
A10:
<*x,y,z*> . 2 = y
by FINSEQ_1:45;
1 in {1,2,3}
by ENUMSET1:def 1;
then A11:
1 in dom <*x,y,z*>
by Th1, FINSEQ_1:89;
3 in {1,2,3}
by ENUMSET1:def 1;
then A12:
3 in dom <*x,y,z*>
by Th1, FINSEQ_1:89;
2 in {1,2,3}
by ENUMSET1:def 1;
then A13:
2 in dom <*x,y,z*>
by Th1, FINSEQ_1:89;
assume
<*x,y,z*> is one-to-one
; ( x <> y & y <> z & z <> x )
hence
( x <> y & y <> z & z <> x )
by A11, A13, A12, A1, A10, A2; verum