Reidemeister's theorem for oriented diagrams

The easy direction and empty case. An empty diagram represents the empty link, and the moves preserve component count. When both diagrams are empty they are already identical; neither equivalence nor a move sequence can relate an empty diagram to a nonempty one. If $D^{\mathrm{\prime }}$ is obtained from $D$ by a finite sequence of planar isotopies and oriented Reidemeister moves, then by [F1] each step is realized by an ambient isotopy of $S^3$ carrying the represented link to the next one, and [F2] makes the composition of the finitely many ambient isotopies again an equivalence; hence $D$ and $D^{\mathrm{\prime }}$ represent equivalent oriented links.

Keep the whole track off infinity. Let $L_0,L_1\subset {\mathbb{R}}^3$ realize $D,D^{\mathrm{\prime }}$; by the assumed equivalence there is an ambient isotopy $H$ of $S^3$ carrying their oriented images to one another. Reparametrize time to make its restricted link isotopy stationary near both ends. Extend that track constantly to $C\times \mathbb{R}$; its image is null by [F6]. Choose a small coordinate ball about $\mathrm{\infty }$ disjoint from $L_0\cup L_1$, and a point $q$ in that ball outside the track. A compactly supported vector field in the ball, equal to the velocity of a short coordinate path from $q$ to $\mathrm{\infty }$, gives a diffeomorphism $K$ with $K(q)=\mathrm{\infty }$ and fixing both endpoint links, by [F6]. Then $F_t=K\circ H_t{\mathrm{\mid }}_{L_0}$ is a smooth link isotopy avoiding $\mathrm{\infty }$ at every time, with exactly the original endpoint diagrams. Its compact trace is contained in a large ball in ${\mathbb{R}}^3$. The regular endpoint projections satisfy the hypothesis of [F4].

General position and the finite sequence. Apply [F4] to $F$ with a strong neighbourhood small enough to keep the end projections fixed: there is a smooth isotopy $F^{\mathrm{\prime }}$ in general position whose end projections are $D$ and $D^{\mathrm{\prime }}$. By [F5] the movement from $t=0$ to $t=1$ of the projections of $F^{\mathrm{\prime }}$ is a finite sequence of planar isotopies and oriented Reidemeister moves taking the projection of $F_0^{\mathrm{\prime }}$ to that of $F_1^{\mathrm{\prime }}$, that is, taking $D$ to $D^{\mathrm{\prime }}$ up to planar isotopy.

Conclusion. Steps 1.1 and 2.1 prove the two implications, so $D$ and $D^{\mathrm{\prime }}$ represent equivalent oriented links if and only if they are connected by planar isotopies and finitely many oriented Reidemeister moves. The axiom of countable choice is used exactly in [F6] (track avoidance by Sard) and [F4] (parametric transversality); the realization direction is choice-free.