let X, Y be set ; :: thesis: <:(pr2 (X,Y)),(pr1 (X,Y)):> is one-to-one
set f = <:(pr2 (X,Y)),(pr1 (X,Y)):>;
let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> or not y in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> or not <:(pr2 (X,Y)),(pr1 (X,Y)):> . x = <:(pr2 (X,Y)),(pr1 (X,Y)):> . y or x = y )
assume that
A1: x in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> and
A2: y in dom <:(pr2 (X,Y)),(pr1 (X,Y)):> and
A3: <:(pr2 (X,Y)),(pr1 (X,Y)):> . x = <:(pr2 (X,Y)),(pr1 (X,Y)):> . y ; :: thesis: x = y
A4: dom <:(pr2 (X,Y)),(pr1 (X,Y)):> = [:X,Y:] by Th4;
then consider x1, x2 being object such that
A5: ( x1 in X & x2 in Y ) and
A6: x = [x1,x2] by A1, ZFMISC_1:def 2;
consider y1, y2 being object such that
A7: ( y1 in X & y2 in Y ) and
A8: y = [y1,y2] by A4, A2, ZFMISC_1:def 2;
A9: <:(pr2 (X,Y)),(pr1 (X,Y)):> . (y1,y2) = [y2,y1] by A7, Lm1;
A10: <:(pr2 (X,Y)),(pr1 (X,Y)):> . (x1,x2) = [x2,x1] by A5, Lm1;
then x1 = y1 by A3, A6, A8, A9, XTUPLE_0:1;
hence x = y by A3, A6, A8, A10, A9, XTUPLE_0:1; :: thesis: verum