let I be set ; :: thesis: for a being object holds pr1 (I,{a}) is one-to-one

let a be object ; :: thesis: pr1 (I,{a}) is one-to-one

set f = pr1 (I,{a});

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (pr1 (I,{a})) or not y in dom (pr1 (I,{a})) or not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )

assume A1: ( x in dom (pr1 (I,{a})) & y in dom (pr1 (I,{a})) ) ; :: thesis: ( not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )

then consider i1, a1 being object such that

A2: ( i1 in I & a1 in {a} & x = [i1,a1] ) by ZFMISC_1:def 2;

consider i2, a2 being object such that

A3: ( i2 in I & a2 in {a} & y = [i2,a2] ) by A1, ZFMISC_1:def 2;

assume (pr1 (I,{a})) . x = (pr1 (I,{a})) . y ; :: thesis: x = y

then (pr1 (I,{a})) . (i1,a1) = (pr1 (I,{a})) . (i2,a2) by A2, A3;

then A4: ( i1 = (pr1 (I,{a})) . (i2,a2) & (pr1 (I,{a})) . (i2,a2) = i2 ) by A2, A3, FUNCT_3:def 4;

( a1 = a & a = a2 ) by A2, A3, TARSKI:def 1;

hence x = y by A2, A3, A4; :: thesis: verum

let a be object ; :: thesis: pr1 (I,{a}) is one-to-one

set f = pr1 (I,{a});

let x, y be object ; :: according to FUNCT_1:def 4 :: thesis: ( not x in dom (pr1 (I,{a})) or not y in dom (pr1 (I,{a})) or not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )

assume A1: ( x in dom (pr1 (I,{a})) & y in dom (pr1 (I,{a})) ) ; :: thesis: ( not (pr1 (I,{a})) . x = (pr1 (I,{a})) . y or x = y )

then consider i1, a1 being object such that

A2: ( i1 in I & a1 in {a} & x = [i1,a1] ) by ZFMISC_1:def 2;

consider i2, a2 being object such that

A3: ( i2 in I & a2 in {a} & y = [i2,a2] ) by A1, ZFMISC_1:def 2;

assume (pr1 (I,{a})) . x = (pr1 (I,{a})) . y ; :: thesis: x = y

then (pr1 (I,{a})) . (i1,a1) = (pr1 (I,{a})) . (i2,a2) by A2, A3;

then A4: ( i1 = (pr1 (I,{a})) . (i2,a2) & (pr1 (I,{a})) . (i2,a2) = i2 ) by A2, A3, FUNCT_3:def 4;

( a1 = a & a = a2 ) by A2, A3, TARSKI:def 1;

hence x = y by A2, A3, A4; :: thesis: verum