let x, y be object ; ( x <> y iff <*x,y*> is one-to-one )
A1:
<*x,y*> . 2 = y
by FINSEQ_1:44;
2 in {1,2}
by TARSKI:def 2;
then A2:
2 in dom <*x,y*>
by FINSEQ_1:2, FINSEQ_1:89;
thus
( x <> y implies <*x,y*> is one-to-one )
( <*x,y*> is one-to-one implies x <> y )proof
assume A3:
x <> y
;
<*x,y*> is one-to-one
let y1,
y2 be
object ;
FUNCT_1:def 4 ( not y1 in dom <*x,y*> or not y2 in dom <*x,y*> or not <*x,y*> . y1 = <*x,y*> . y2 or y1 = y2 )
assume that A4:
y1 in dom <*x,y*>
and A5:
y2 in dom <*x,y*>
and A6:
<*x,y*> . y1 = <*x,y*> . y2
;
y1 = y2
A7:
y2 in {1,2}
by A5, FINSEQ_1:2, FINSEQ_1:89;
A8:
y1 in {1,2}
by A4, FINSEQ_1:2, FINSEQ_1:89;
hence
y1 = y2
;
verum
end;
assume that
A11:
<*x,y*> is one-to-one
and
A12:
x = y
; contradiction
1 in {1,2}
by TARSKI:def 2;
then A13:
1 in dom <*x,y*>
by FINSEQ_1:2, FINSEQ_1:89;
<*x,y*> . 1 = x
by FINSEQ_1:44;
hence
contradiction
by A11, A12, A13, A2, A1; verum