Proving that the distance values extracted in Dijkstra's algorithm is non-decreasing?

I'm reviewing my old algorithms notes and have come across this proof. It was from an assignment I had and I got it correct, but I feel that the proof certainly lacks.

The question is to prove that the distance values taken from the priority queue in Dijkstra's algorithm is a non-decreasing sequen开发者_JAVA百科ce.

My proof goes as follows:

Proof by contradiction. Fist, assume that we pull a vertex from Q with d-value 'i'. Next time, we pull a vertex with d-value 'j'. When we pulled i, we have finalised our d-value and computed the shortest-path from the start vertex, s, to i. Since we have positive edge weights, it is impossible for our d-values to shrink as we add vertices to our path. If after pulling i from Q, we pull j with a smaller d-value, we may not have a shortest path to i, since we may be able to reach i through j. However, we have already computed the shortest path to i. We did not check a possible path. We no longer have a guaranteed path. Contradiction.

How could this proof be improved upon? Or better yet, is there a different approach? It just seems pretty weak :)

Edit: Sorry, in this case my priority queue is implemented with a Min-heap

---

Let's establish these (these are all true, since they are, basically, the definition of the algorithm) :

1. The Priority Queue in Dijkstra's algorithm will give you the node with the lowest d-value in each iteration of the algorithm.
2. There are no negative edge weights.
3. Once a node has been dequeued, it will never return to the queue.
4. The d-value of a node that has been dequeued is final, and will not change from that point on.

Continuing (1), the d-value of that dequeued node, assuming (2) applies, will be at the very least equal to the previous d-value extracted, since each node's d-value depends on the d-values of the nodes dequeued prior to it, which is a sort of recursive definition. Since (3) and (4) are correct, this recursive definition ends at the starting node which has d-value of 0.
So, if each node's d-value is at the very least equal to the d-value before him, and (1) still applies, the set of d-values extracted from the priority queue is non-decreasing.

(After reading through this, and what you wrote, it's basically the same, but presented a bit better I think)