now :: thesis: for nm1, nm2 being object st nm1 in & nm2 in & PairFunc . nm1 = PairFunc . nm2 holds
nm1 = nm2
let nm1, nm2 be object ; :: thesis: ( nm1 in & nm2 in & PairFunc . nm1 = PairFunc . nm2 implies nm1 = nm2 )
assume that
A1: nm1 in and
A2: nm2 in and
A3: PairFunc . nm1 = PairFunc . nm2 ; :: thesis: nm1 = nm2
consider n2, m2 being object such that
A4: ( n2 in NAT & m2 in NAT ) and
A5: [n2,m2] = nm2 by ;
consider n1, m1 being object such that
A6: ( n1 in NAT & m1 in NAT ) and
A7: [n1,m1] = nm1 by ;
reconsider n1 = n1, n2 = n2, m1 = m1, m2 = m2 as Element of NAT by A6, A4;
A8: ((2 |^ n2) * ((2 * m2) + 1)) - 1 = PairFunc . nm2 by ;
A9: ((2 |^ n1) * ((2 * m1) + 1)) - 1 = PairFunc . nm1 by ;
then n1 = n2 by ;
hence nm1 = nm2 by A3, A7, A5, A9, A8, CARD_4:4; :: thesis: verum
end;
hence PairFunc is one-to-one by FUNCT_2:19; :: according to FUNCT_2:def 4 :: thesis:
now :: thesis: for i being object st i in NAT holds
i in rng PairFunc
let i be object ; :: thesis: ( i in NAT implies i in rng PairFunc )
assume i in NAT ; :: thesis:
then reconsider i9 = i as Element of NAT ;
consider n, m being Nat such that
A10: i9 + 1 = (2 |^ n) * ((2 * m) + 1) by Th1;
( n in NAT & m in NAT ) by ORDINAL1:def 12;
then A11: [n,m] in by ZFMISC_1:87;
i9 - 0 = ((2 |^ n) * ((2 * m) + 1)) - 1 by A10;
then ( dom PairFunc = & i = PairFunc . [n,m] ) by ;
hence i in rng PairFunc by ; :: thesis: verum
end;
then NAT c= rng PairFunc ;
then NAT = rng PairFunc ;
hence PairFunc is onto ; :: thesis: verum