OK, but how are you going to construct a bijection from an arbitrary infinite set of undefinable numbers onto a set with a choice function without the AoC?