Hypothesis.
(a) For visited s … dist[s] is shortest distance from source
(b) For unvisited t … dist[t] is shortest distance from source via visited nodes

Proof.
Base case: no visited nodes, dist[source]=0, dist[s]=∞ for all other nodes

Induction step:

1. If s is unvisited node with minimum dist[s], then dist[s] is shortest distance from source to s:
   • if ∃ shorter path via only visited nodes, then dist[s] would have been updated when processing the predecessor of s on this path
   • if ∃ shorter path via an unvisited node u, then dist[u]<dist[s], which is impossible if s has min distance of all unvisited nodes
2. This implies that (a) holds for s after processing s
3. (b) still holds for all unvisited nodes t after processing s:
   • if ∃ shorter path via s we would have just updated dist[t]
   • if ∃ shorter path without s we would have found it previously