Does the set of all ordinals strictly dominated by a given set exist in ZF? How do I prove that
$$ \{\alpha\in\mathsf{On}\,|\,\alpha\prec A\}\in V,$$
assuming $A\in V$? I know that if AC is assumed, this set is equal to $\mbox{card}(A):=\mu_\alpha(\alpha\approx A)$, and hence it exists. But in the absence of the AC, we allow the possibility of sets such that $\forall\alpha\in\mathsf{On}\ \,\alpha\not\approx A$, but it seems that if $\forall\alpha\in\mathsf{On}\ \,\alpha\prec A$, there should be some argument to prove that $A$ is "too big" to be a set. Side note: would it be possible to prove in this case that $\mathsf{On}\approx A$?
Notation notes: $A\approx B$ means that there is a bijection from $A$ to $B$, and $A\preccurlyeq B$ means there is an injection from $A$ to $B$. $\mathsf{On}$ is the proper class of ordinal numbers, and $\mu_\alpha(P)$ is the smallest ordinal $\alpha$ satisfying $P$, or $\emptyset$ if none exist.
The set $\{x\in\mathsf{On}\,|\,x\prec A\}$ (which is an ordinal) is actually a very interesting set in ZF, because it shares many properties with $\mbox{card}(A)$, but for classes which are not equinumerous to any ordinal, $\mbox{card}(A)=\emptyset$, but it can be proved by finite induction that $\omega\subseteq\{x\in\mathsf{On}\,|\,x\prec A\}$ for any such class, so in some sense it doesn't "give up" as easily as the conventional definition.
Edit: For clarification, I want to prove that $ \{\alpha\in\mathsf{On}\,|\,\alpha\prec A\}\ne\mathsf{On}$, which is equivalent to $ \{\alpha\in\mathsf{On}\,|\,\alpha\prec A\}\in V$, as well as to $\exists\alpha\in\mathsf{On}\ \,\alpha\not\prec A$.
 A: The existence of the set that you have presented is an immediate consequence of the result that a Hartogs Number exists for any set $ A $.

Theorem (ZF) Let $ \alpha $ be the class of all ordinals that inject into $ A $. Then $ \alpha $ is an ordinal that does not inject into $ A $.

Proof:


*

*By the Power-Set Axiom, the classes $ \mathcal{P}(A) $, $ A \times A $ and $ \mathcal{P}(A \times A) $ are sets.

*Let $ \mathcal{B} $ be the class of subsets of $ A $ that can be well-ordered. As $ \mathcal{B} $ is a definable subclass of $ \mathcal{P}(A) $, it is a set by the Axiom Schema of Separation.

*For each $ B \in \mathcal{B} $, let $ W(B) $ denote the class of all well-orderings on $ B $. As $ W(B) $ is a definable subclass of $ \mathcal{P}(A \times A) $, it is a set by the Axiom Schema of Separation.

*For each $ B \in \mathcal{B} $ and each $ R \in W(B) $, the well-ordered set $ (B,R) $ is order-isomorphic to a unique ordinal $ \beta $. Clearly, $ \beta $ must inject into $ A $, so $ \beta \in \alpha $.

*By the definition of $ \alpha $, any $ \beta \in \alpha $ is equipollent to some $ B \in \mathcal{P}(A) $. The well-ordering on $ \beta $ then induces a well-ordering $ R $ on $ B $.

*By the Power-Set Axiom, the class $ \mathcal{P}(A) \times \mathcal{P}(A \times A) $ is a set. As $ W := \{ (B,R) ~|~ B \in \mathcal{P}(A) \land R \in W(B) \} $ is a definable subclass of $ \mathcal{P}(A) \times \mathcal{P}(A \times A) $, it follows from the Axiom Schema of Separation that $ W $ is a set.

*By the foregoing argument, there exists a surjective class-function $ f $ from $ W $ to $ \alpha $.

*As $ W $ is a set and $ \alpha = \text{Range}(f) $, it follows from the Axiom Schema of Replacement that $ \alpha $ is a set.

*We shall now prove that $ \alpha $ is an ordinal.

*As $ \alpha $ is a set of ordinals, it is automatically well-ordered.

*Next, suppose that $ \gamma \in \beta \in \alpha $. Then as $ \beta $ is an ordinal, its transitivity yields $ \gamma \subseteq \beta $.

*As $ \beta \in \alpha $, we see that $ \beta $ injects into $ A $. Let $ \phi: \beta \to A $ be an injection.

*The restriction of $ \phi $ to $ \gamma $ is an injective class-function from $ \gamma $ to $ A $. This restriction is a definable subclass of $ \phi $, so it is an injective set-function by the Axiom Schema of Separation.

*Hence, $ \gamma \in \alpha $.

*Therefore, $ \alpha $ is transitive, which implies that it is an ordinal.

*Finally, $ \alpha $ cannot inject into $ A $, otherwise $ \alpha \in \alpha $, which is a contradiction. $ \quad \spadesuit $

Conclusion: The class $ \alpha := \{ \beta ~|~ \text{ON}(\beta) \land (\beta \prec A) \} $ is a set (in fact, an ordinal).

A: First note that every bounded class of ordinals is a set. This is trivial using the subset schema applied to any upper bound of the class. Here is a nice proof as for why such classes classes of ordinals cannot be a proper class:

Assume by contradiction that $A$ is a set such that $\{\alpha\in\mathsf{Ord}\mid\alpha\prec A\}$ is not a set. Then for every initial ordinal $\omega_\alpha$ there is a subset of $A$ of cardinality $\omega_\alpha$. Using the power set axiom there is a set $\mathcal P(A)$. We define the following function: $$f(B)=\begin{cases}\omega_\alpha & \exists\omega_\alpha\sim B\\ 0 &\text{otherwise.}\end{cases}$$
This function is well-defined because every $B$ which can be well-ordered is equipotent with exactly one initial ordinal. Using the replacement schema we know that the range of $f$ (when applied to the set $\mathcal P(A)$) is a set. But this is a contradiction because this collection should contain all the initial ordinals which is a proper class.

There are other ways of proving this class is a set, for example by exhibiting an injection from it into $\mathcal{P(P(P(}A)))$. But I like this way because it's shorter, in some sense.
