I make self-study in class field theory and I want to prove the following popular fact:
Given a modulus $\mathfrak{m}$ of a number field $K$, the map $L\mapsto ker (\phi_{L/K,\mathfrak{m}}$) is an inclusion-reversing bijection between the set of finite abelian extensions of $K$ that admit $\mathfrak{m}$ and the set of congruence subgroups for $\mathfrak{m}$.
An extension $L/K$ admits
$\mathfrak{m}$ iff $\mathfrak{m}$ is divisible by all primes that ramify in $L$ and $ker(\phi_{L/K,\mathfrak{m}})$ is congruence subgroup where $\phi_{L/K,\mathfrak{m}}$ is the Artin map.
As a result of Takagi existence theorem, the map is surjective. But I have problem about injectivity and inclusion-reserving.