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
Yes, it's unclear what reasoning you are using in the highlighted step, or in the line that follows. The logic behind the second part of the proof is also obscure. In particular, the step from the fourth to the fifth line makes little sense to me. It seems to me that you are making formal manipulations about whose meaning you are not entirely certain.
The key point is the fact that there is no $x$ such that $x \in \emptyset$. That's literally the definition of the empty set. Consequently, it does not really make sense to start your proof by assuming that $x \in \emptyset$.
Instead of proving that $A \times B = \emptyset$ if and only if $A = \emptyset$ or $B = \emptyset$, you can (by elementary propositional logic) prove that $A \times B \neq \emptyset$ if and only if $A \neq \emptyset$ and $B \neq \emptyset$. In plain English, $A \times B$ is non-empty (contains some element) if and only if $A$ and $B$ are both non-empty (both contain some element).
But this is a triviality: if $A \times B$ is non-empty, then it contains some element of the form $(x, y)$ for some $x \in A$ and $y \in B$, so $A$ and $B$ are both non-empty. Conversely, if $A$ and $B$ are non-empty and contain, respectively, the elements $x$ and $y$, then $A \times B$ is non-empty because it contains the pair $(x, y)$.