Integral ideal factorisation in a number field, in ZF

The quotient $R={\mathcal{O}}_K\mathrm{/}\mathfrak{a}$ is finite, so its finite ideal lattice supplies the finite list of maximal ideals; their inverse images are exactly the primes $\mathfrak{p}$ containing $\mathfrak{a}$. The finite free integral lattice makes ${\mathcal{O}}_K$ noetherian, its definition as an integral closure makes it integrally closed, and every nonzero prime is maximal because its quotient is a finite domain. Thus $({\mathcal{O}}_K{)}_{\mathfrak{p}}$ is a DVR. Consequently $\mathfrak{a}({\mathcal{O}}_K{)}_{\mathfrak{p}}={\mathfrak{p}}^{e_{\mathfrak{p}}}({\mathcal{O}}_K{)}_{\mathfrak{p}}$ for a unique least $e_{\mathfrak{p}}>0$.

Put $\mathfrak{b}=\prod {\mathfrak{p}}^{e_{\mathfrak{p}}}$. At every maximal ideal in the finite list, step 1.1 gives ${\mathfrak{a}}_{\mathfrak{p}}={\mathfrak{b}}_{\mathfrak{p}}$; at any other maximal ideal both localisations are the unit ideal. Hence $\mathfrak{a}=\mathfrak{b}$ (otherwise a maximal ideal containing the appropriate colon ideal gives a contradictory localisation). Distinct prime powers are comaximal, so the Chinese remainder theorem reassembles this finite product. Localising a second factorisation at the same finite primes forces the same exponents. The list is finite and each exponent is the least natural number with its property, so no Choice is used.