A more rigorous proof on a Bellman-Ford's corollary

The following corollary can be found at page 653 of "Introduction to algorithms (3rd edition)"

Corollary 24.3

Let $$G = (V, E)$$ be a weighted, directed graph with source vertex $$s$$ and a weight function $$w: E \to \mathbb{R}$$. Then, for each vertex $$v > \in V$$, there is a path from $$s$$ to $$v$$ if and only if BELLMAN-FORD terminates with $$v.d < \infty$$ when it is run on $$G$$.

I have an intuition for the corollary and would formulate its proof as following:

$$\rightarrow$$: Suppose there are paths from $$s$$ to $$v$$, we call the shortest path $$p$$. The path $$p$$ is shortest and therefore simple and hence has at most $$|V| - 1$$ edges. Each edge of the path $$p$$ will be relaxed by Bellman-Ford, an operation which will only decrease $$v.d$$. Therefore we can concluse, that $$v.d < \infty$$ after the algorithm terminates.

Another argument may also include the "Path-relaxation property", which states $$v.d = \delta(s, v) < \infty$$ after relaxations of all edges of $$p$$.

$$\leftarrow$$: Suppose there is no path from $$s$$ to $$v$$ but Bellman-Ford terminates with $$v.d < \infty$$. This would be a contradiction with "No-path property", which states $$v.d = \delta(s, v) = \infty$$.

I am self-studying the book and there is a lack of feedbacks from tutor, so my question is: would my proof be sufficient in this case?