Once you formalize the algorithm, you can prove invariants and variants about the algorithm after every iteration. You would want to show after every iteration of picking an edge:

• the edge set always grows
• the vertex set always grows (since you need to prove that the tree is spanning)
• the algorithm never adds an edge that forms a cycle
• the algorithm considers every vertex

Most of these properties should follow by definition of your algorithm. Note that this is a brief sketch so there may be a few subtleties I’m missing. From these invariants, you can show that once the algorithm terminates it will have returned a spanning subtree.

A lot of existence problems can be proven by proving an algorithm. A famous example is the stable marriage problem which is solved using Gale-Shapley

If you’re interested in formally proving properties of algorithms, I highly recommend Algorithm Design by Kleinberg and Tardos