I think your question is not as precise as you portray it.
First, let me point out that you have not actually defined
a function $z$, in the sense of giving a first order
definition of it in set theory, and you provably cannot do
so, because of Tarski's theorem on the non-definability of
truth. We simply have no way to express the relation x is
definable in the usual first-order language of set theory.
More specifically:
Theorem. If ZFC is consistent, then there are models
of ZFC in which the collection of definable natural numbers
is not a set or even a class.
Proof. If V is a model of ZFC, then let $M$ be an internal
ultrapower of $V$ by a nonprincipal ultrafilter on
$\omega$. Thus, the natural numbers of $M$ are nonstandard
relative to $V$. The definable elements of $M$ are all
contained within the range of the ultrapower map, which in
the natural numbers is a bounded part of the natural
numbers of $M$. Thus, $M$ cannot have this collection of
objects as a set or class, since it would reveal to $M$
that its natural numbers are ill-founded, contradicting
that $M$ satisfies ZFC. QED
In such a model, your definition of $z$ is not first order.
It could make sense to treat your function $z$, however, in
a model as an externally defined function, defined outside
the model (as via second-order logic). In this case, $z(n)$
only involves standard or meta-theoretic definitions, and
other problems arise.
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $z(n)$ is bounded by a constant function.
Proof. If ZFC is consistent, then so is $ZFC+\neg
Con(ZFC)$. Let $V$ be any model of this theory, so that
there are no models of ZFC there, and the second part of
the definition of $z$ becomes vacuous, so it reduces to its
definable-in-$V$ first part. Let $M$ be an internal
ultrapower of $V$ by an ultrafilter on $\omega$. Thus, $M$
is nonstandard relative to $V$. But the function $z$,
defined externally, uses only standard definitions, and the
definable elements of $M$ all lie in the range of the
ultrapower map. If $N$ is any $V$-nonstandard element of
$M$, then every definable element of $M$ is below $N$, and
so $z(n)\lt N$ for every $n$ in $M$. QED
Theorem. If ZFC is consistent, then there is a model
of ZFC in which $f(n)\lt z(10000)$ for every natural number
n in the meta-theory.
Proof. If ZFC is consistent, then so is $ZFC+\neg
Con(ZFC)+GCH$. Let $V$ be a countable model of $ZFC+\neg
Con(ZFC)+GCH$. Since $V$ has no models of ZFC, again the
second part of your definition is vacuous, and it reduces
just to the definability-in-$V$ part. Let $M$ again be an
internal ultrapower of $V$ by an ultrafilter on $\omega$,
and let $N$ be a $V$-nonstandard natural number of $M$.
Every definable element of $M$ is in the range of the
ultrapower map, and therefore below $N$. In particular, for
every meta-theoretic natural number $n$, we have $f(n)\lt
N$ in $M$, since $f(n)$ is definable. Now, let $M[G]$ be a
forcing extension in which the continuum has size
$\aleph_N^M$. Thus, $N$ is definable in $M[G]$ by a
relatively short formula; let's say 10000 symbols (but I
didn't count). Since the forcing does not affect the
existence of ZFC models or Turing computations between $M$
and $M[G]$, it follows that $f(n)\lt z(10000)$ in $M[G]$
for any natural number of $V$. QED
Theorem. If ZFC is consistent, then there is a model
of ZFC with a natural number constant $c$ in which $z(n)\lt
f(c)$ for all meta-theoretic natural numbers $n$.
Proof. Use the model $M$ (or $M[G]$) as above. This time,
let $c$ be any $V$-nonstandard natural number of $M$. Since
the definable elements of $M$ all lie in the range of the
ultrapower map, it follows that every z(n), for
meta-theoretic $n$, is included in the $V$-standard
elements of $M$, which are all less than $c$. But $M$
easily has $c\leq f(c)$, and so $z(n)\lt f(c)$ for all
these $n$. QED
Rom Maimon is describing the program of proof-theoretic ordinal analysis.
First, as you observed in your addendum, it isn't interesting to find some encoding of an ordinal whose well-foundedness implies Con(ZFC), but rather an ordinal such that the well-foundedness of any representation implies Con(ZFC). One hopes that it suffices to consider natural representations of the ordinal, which has been true in practice, but is unproven (and probably unprovable, given the difficulty of making precise what counts as a natural representation).
It's possible to prove that the smallest ordinal which ZFC fails to prove well-founded is computable by noticing that the computable notations for ordinals provably well-founded in ZFC are a $\Sigma_1$ subset of the computable notations for ordinals, so certainly $\Sigma^1_1$, and by a result of Spector, any $\Sigma_1^1$ subset of the computable notations for ordinals is bounded.
As pointed out in the answer Timothy Chow links to above, it's typically true that this notion of proof-theoretic ordinal ends up being the same as ordinals with other nice properties (like implying Con(ZFC)), but there's no proof that that will always happen (and can't be, since there are defective examples that show it's not always true), nor a proof that covers ZFC.
However it's generally believed that for "natural" theories, including ZFC, the different notions of proof-theoretic ordinal will line up.
Finding an explicit description of the ordinal for ZFC is an active problem in proof theory, but progress has been very slow. The best known results are by Rathjen and Arai (separately) at the level of $\Pi^1_2$-comprehension (a subtheory of second order arithmetic, so much, much weaker than ZFC), and after nearly 20 years, those remain unpublished. The results in the area got extremely difficult and technical, and didn't seem to provide insight into the theories the way the smaller ordinals had, so it's not nearly as active an area as it once was. Wolfram Pohlers and his students still seem to working in the area, and some other people seem to be thinking about other approaches rather than directly attacking it (Tim Carlson and Andreas Weiermann and their students come to mind).
Best Answer
In 1939, Alan Turing investigated such questions [Systems of logic based on ordinals, Proc. London Math. Soc. 45, 161-228]. It turns out that one runs into problems rather quickly due to the fact that the $(\omega+1)$-th such theory is not completely well-defined. Indeed, there are many ordinal notations for $\omega+1$ and these can be used to code a lot of information.
Turing's Completeness Theorem. If $\phi$ is a true $\Pi_1$ sentence in the language of arithmetic, then there is an ordinal notation $a$ such that $|a| = \omega+1$ and $T_a$ proves $\phi$.
This result applies to any sound recursively axiomatized extension $T$ of $PA$. In particular, this applies to (the arithmetical part of) $ZF$.
To avoid this, one might carefully choose a path through the ordinal notations, but this leads to a variety of other problems [S. Feferman and C. Spector, Incompleteness along paths in progressions of theories, J. Symbolic Logic 27 (1962), 383–390].