Congratulations, your proof is correct! What you have defined is called the empty function with codomain $\emptyset$.
Since the proof is right, I'll make a few comments about style.
On the whole I understood it all the way through and didn't need to do any backtracking, which is already the sign of a well-written proof!
But not to worry - there is still rom for improvement.
Structure
The statement that you are to prove consists of three parts, whose most natural ordering seems to me to be
- There exists a function mapping $\emptyset\rightarrow \emptyset$.
- Such a function is unique.
- This function is a bijection.
In your argument, you have proved 2, then 1, then 3.
It is not strictly incorrect to prove uniqueness before existence, but it can get you in trouble and is not intuitive to read.
My guess it that you wrote it in this order because that was how you reasoned about it.
That is, "what should this $f$ look like? Well, it must have an empty graph, so let's define that object."
When you're writing proofs primarily to convince a reader of the correctness of the result (for example, when writing a research paper, but not when writing a textbook, where the primary aim is exposition), you want to exclude extraneous detail, so best practice would be to introduce your candidate function $f$ without preamble.
I would write your existence argument like this:
Consider the triple $f = (\emptyset, \emptyset, \emptyset)$.
Since the domain is empty, it is vacuously true that every element in the domain has an image and moreover, that this image is unique.
Therefore, $f$ is a function.
And follow that with uniqueness:
Let $g = (\emptyset, \emptyset, G)$ be a function.
Since $G \subseteq \emptyset \times \emptyset$, it must be that $G = \emptyset$, and so that $g = f$.
Hence, $f$ is the unique function mapping $\emptyset \rightarrow \emptyset$.
Formal logic
Mathematics is written in full sentences, and strings of formal logic are very unusual in mathematical writing.
You'll notice that in my proposed examples, I have no logical symbols at all, but hopefully I was able to unambiguously convey the logical argument.
This is because formal logic is difficult to parse, and contains every piece of information about the statement, even when only a small amount is needed for the argument at hand.
Compare in my existence statement the phrase "since the domain is empty," which is the reason that everything holds vacuously to
$$
(\forall x)[x \in \emptyset \rightarrow (\exists y)(y \in \emptyset \land (x, y) \in \emptyset)],
$$
where the "$(\exists y)(y \in \emptyset \land (x, y) \in \emptyset)$" part is included in the text despite being long, complicated and completely irrelevant to the argument.
"Clearly"
Remove this word, as well as "obviously" and friends, from your mathematical vocabulary.
If something really is clear, you should have no trouble explaining it in one sentence, and that leads to a stronger text.
If you can't do this, you're using the word to cover up a messy argument.
This is a minor point, as you only write it once, and the sentence can be improved simply by erasing the word "clearly."
Nevertheless, I thought that I would raise it, as it's a good thing to keep in mind.
Best Answer
I don't see why you would need to make a special case for an injection $\emptyset\to \{\emptyset\}$, because the function $f:\emptyset\to\{\emptyset\}$ such that $f(x)=\{x\}$ for all $x\in\emptyset$ is already the empty map.
Existence of some $a\in X$ such that $f(a)=\{x\in X\,:\, x\notin f(x)\}$ comes from the assumption of $f$ being surjective. In specific cases this may result in a contradiction by other means in addition to proving that $a\in f(a)\leftrightarrow a\notin f(a)$, but the general way is still valid here: the same proof $$\exists f\text{ surjective}\Rightarrow \exists f\text{ surjective},\exists a\in X, (a\in f(a)\leftrightarrow a\notin f(a))$$ works for $X=\emptyset$ as well.