let x, y be object ; :: thesis: ( 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 ) :: thesis: ( <*x,y*> is one-to-one implies x <> y )
proof
assume A3: x <> y ; :: thesis: <*x,y*> is one-to-one
let y1, y2 be object ; :: according to FUNCT_1:def 4 :: thesis: ( 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 ; :: thesis: 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;
now :: thesis: y1 = y2
per cases ( ( y1 = 1 & y2 = 1 ) or ( y1 = 2 & y2 = 2 ) or ( y1 = 1 & y2 = 2 ) or ( y1 = 2 & y2 = 1 ) ) by A8, A7, TARSKI:def 2;
suppose ( ( y1 = 1 & y2 = 1 ) or ( y1 = 2 & y2 = 2 ) ) ; :: thesis: y1 = y2
hence y1 = y2 ; :: thesis: verum
end;
suppose A9: ( y1 = 1 & y2 = 2 ) ; :: thesis: y1 = y2
then <*x,y*> . y1 = x by FINSEQ_1:44;
hence y1 = y2 by A3, A6, A9, FINSEQ_1:44; :: thesis: verum
end;
suppose A10: ( y1 = 2 & y2 = 1 ) ; :: thesis: y1 = y2
then <*x,y*> . y1 = y by FINSEQ_1:44;
hence y1 = y2 by A3, A6, A10, FINSEQ_1:44; :: thesis: verum
end;
end;
end;
hence y1 = y2 ; :: thesis: verum
end;
assume that
A11: <*x,y*> is one-to-one and
A12: x = y ; :: thesis: 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; :: thesis: verum