I'm looking for proof of the following statement:
"The existence of an arbitrage-free implied volatility surface is equivalent to the existence of a well-defined local volatility surface."
This is not quite true, in either direction.
If you have an arbitrage free implied vol surface, you might not have a well-defined local vol surface. An example comes from a discrete model. Consider a spot dynamics where the spot is a martingale that jumps up or down by integer amounts. The spot distribution is discrete, with zero density in between integer levels. The Dupire equation will result in division by zero trying to calculate the corresponding local vol. That is, there is no local vol model that gives exactly the same prices. Local vol models get arbitrarily close, but the limit diffusion is a "gap diffusion" -- what you get when you let the local vol be infinite.
In the other direction, there are local volatility functions which give a strict local martingale spot dynamics. For example, let the local volatility be $\sigma (S)=S $, so $dS=S^2 dW $. According to the usual theories of arbitrage pricing, this model has arbitrage. For instance there is a delta-hedging strategy to replicate $S $ at time $T $ for less cost than $S (0) $. Such local vol models are only arbitrage free under a different numeraire. For example taking a basket of one dollar and one stock as numeraire, the local vol model allows the price of the dollar to become worthless with respect to the basket, but the arbitrage is no longer present.
Unfortunately I don't know of a neat way to fix the statement to nicely clean up the edge cases. As written it is "mostly true" or "morally true" but not mathematically true.