Alternative algorithm for minimum spanning tree construction
It is not immediate to see whether OP’s approach can be adapted easily to a full proof.

Here is an answer to the same question but phrased differently, a local minimum in the graph of spanning trees is a (global) minimum spanning tree.

I will present  another proof, which is more flexible and probably easier to understand.

Let $G$ be an undirected connected (finite) graph with distinct costs on its edges, as in the original question. Consider the delete-heaviest-edge algorithm on $G$, which removes the heaviest edge in a cycle until no cycle remains. Just to be clearer, let me call the remaining edges at the end of the algorithm $H$. Let us show that $H$ is the minimum cost spanning tree (MST) of $G$.

$H$ is a spanning tree of $G$ because of the following.


$H$ is connected,  since $G$ is connected and all we have done is breaking cycles.
$H$ is has no cycle since the algorithm ends only if there is no cycle.
$H$ has all vertices of $G$ since no vertex of $G$ has ever been deleted.


Because of the the cycle property, any edge in any minimal cost spanning tree (MST) of $G$ is never deleted. So all edges of any MST of $G$ remain in $H$. However, any spanning tree of $G$ has the same number of edges, so $H$ must be the unique MST of $G$. (Yes, we have also proved that there is only one MST of $G$, thanks to the distinctness of the costs). 

So we have proved that the delete-heaviest-edge algorithm finds the MST. The flexibility of that algorithm is that in each step we can choose any particular cycle.

Following the OP, let $T$ be the spanning tree which we obtain at the end of OP's algorithm. Initialize $G'$ to be a copy of $G$ and $T'$ is the spanning tree of $G'$ that corresponds to $T$. Let $e'$ be an edge in $G'$ but not in $T'$. If we add $e'$ to $T'$, we will create a cycle since $T'$ is spanning. Note that $e'$ must be the unique heaviest edge in that cycle; otherwise, we can substitute $e'$ for that unique heaviest edge, which is in $T'$, to get a lighter spanning tree, which means the OP's algorithm must not end with $T$, a contradiction. Let us run the delete-heaviest-edge algorithm on $G'$ in the following way. We choose that cycle and delete $e'$ from $G'$. Repeat until all edges in $G'$ but not in $T'$ are deleted. What remains is exactly $T'$. Since $T'$ has no cycle, we have actually run the delete-heaviest-edge algorithm to the end. As we have proved, $T'$ is the MST of $G'$. That is, $T$ is the MST of $G$.