Help with questionable FOL translation and a proof based on the same principle

I'm using Fitch-style proofs where ~ denotes negation sign and x shows subproof, xx subproof within subproof et.c. (Sorry about this getting a bit messy, but in lack of better ideas this is how I try to write proofs here).

Exercise:

Translate the following into First Order Language by using predicates Number, Larger, Odd, Prime and the constant symbol 2:

"There is a number which is larger than every other number"

Solution:

"

where Larger(x,y) means x is larger than y."

Is this really correct? I would like to add " ~(x=y)" in front of the conditional. Does the above given answer not imply that x is larger than every other number AND also that it is larger than itself (or at least that some number is larger than itself)?

If it is true for all objects y, then it should also be true when y refers to the same object as x.

To me this principle seems obvious. Applicated:

Another exercise/solution from the same source states that one cannot prove ~ from a set of premises, including ~ . I believe the conclusion is provable using only this premise;

1. ~

2. x assumption towards contradiction

3. xx [a] assumption towards elimination

4. xx R(a,a)

5. xx

6. x )

7. xContradiction Contradiction intro 1,6

8. ~ ~ intro 2-7

Help is much appreciated, I feel quite puzzled about this since the given solutions to the exercises contradict my reasoning and the proof...

Thanks in advance!