Intuitively, it is clear to me why, up to isomorphism, there are at most $2^{\aleph_0}$ non-isomorphic models of Th($\mathbb{N}$): I can choose as "representative" of any countable model $\mathfrak{A}$ of Th($\mathbb{N}$) a model $\mathfrak{N}$ such that its universe is $\mathbb{N}$ and such thath $\mathfrak{A}$ and $\mathfrak{N}$ are isomorphic, using the bijection between |$\mathfrak{A}$| and $\mathbb{N}$. We can then observe, by easy cardinality considerations, that the number of countable models of Th($\mathbb{N}$) that have as universe $\mathbb{N}$ is, at most, $2^{\aleph_0}$.
Well, now, if I want to formalize in ZFC this argument, how should I proceed? In particular, how can I just express in ZFC something like " up to isomorphism, there are at most $2^{\aleph_0}$ countable models of Th($\mathbb{N}$)", wich is the claim of the theorem ? What we are saying is that, up to isomophism, the cardinality of the set of countable models of Th($\mathbb{N}$) is at most $2^{\aleph_0}$. But I cannot get (1) how to express "up to isomorphism" and (2) how to refer to the object "the set of countable models of Th($\mathbb{N}$)", because that's a proper class. Clearly, (1) e (2) are linked, and I think that the solution is to find the right expression in ZFC and resolve them togheter.
The best thing that I could find is this:
ZFC $\vdash$ [$\forall\mathfrak{A}$ $\forall\mathfrak{B}$[($\mathfrak{A}\ and\ \mathfrak{B}\ are\ isomorphic\ models\ of\ Th(\mathbb{N})$)$\rightarrow\ \mathfrak{A}=\mathfrak{B} $]] $\rightarrow \exists A(A$ is the set of countable models of $Th(\mathbb{N})$ and $|A|\ \leq 2^{\aleph_0})$
Any improvements or suggestions?
Here is one way to express this in the language of set theory: There is a set $X$ of cardinality $2^{\aleph_0}$ such that for every $\mathfrak{A}$, if $\mathfrak{A}$ is a countable model of $\mathrm{Th}(\mathbb{N})$, then there exists $\mathfrak{B}\in X$ such that $A\cong \mathfrak{B}$.
Of course, this is a natural language abbreviation for the sentence in question. If it's not clear to you how to write this in the first-order syntax, I can expand on it.
Why does this formalize the natural language statement "there are at most $2^{\aleph_0}$ non-isomorphic countable models of $\mathrm{Th}(\mathbb{N})$"? Well, letting $C$ be the class of countable models of $\mathrm{Th}(\mathbb{N})$, we can pick a well-ordering of $X$ anad define a class function $F\colon C\to X$ by mapping $\mathfrak{A}$ to the least $\mathfrak{B}\in X$ such that $\mathfrak{A}\cong \mathfrak{B}$. Then $F$ respects isomorphism, so it descends to an injective function $C/{\cong} \hookrightarrow X$, demonstrating that $|C/{\cong}|\leq 2^{\aleph_0}$.
From this formulation, it's even clear how to go about proving the statement: just let $X$ be the set of all structures in the language of arithmetic with domain $\omega$.
The language of ZFC doesn't allow us to talk directly about classes (and in particular, we can't quantify over class functions), so we have to do this kind of translation of statements about classes into equivalent formulations just about sets in order to formalize them.
The sentence you wrote has lots of problems:
Both the antecedent and the consequent of the implication are false:
So ZFC does prove the sentence you wrote down (by propositional logic - the statement is vacuously true). But this theorem is basically meaningless.