The Relative Consistency of the Axiom of Choice - Mechanized Using Isabelle/ZF