Can a set have a complement in intuitionistic ZF? Does IZF (ZF formulated in intuitionistic logic) prove that for any set $a$, $\{x: x \notin a \}$ does not exist?

Consider the rank function $\operatorname{rank}$ defined by
$$\operatorname{rank} a = \bigcup\{\operatorname{rank}x + 1 \mid x\in a\}.$$
Then every element of $a$ has a rank smaller than $\operatorname{rank} a$, but you can show that any ordinal $\alpha$ has rank $\alpha$, so any ordinal greater than $\operatorname{rank} a$ is not a member of $a$.
Now I claim that the class $C=\{\beta\in\mathrm{Ord}\mid \alpha\in\beta\}$ is a proper class for any $\alpha$. Assume that $C$ is a set, then $\gamma:=\bigcup C$ is also an ordinal since $C$ is a set of ordinals. Then $\gamma\in C$, which is a contradiction since it implies $\gamma\in C\subseteq \gamma$.

Here are some remarks on my proof:

*

*$\mathsf{CZF}^-$ (Constructive ZF without Subset Collection) suffices for the proof.


*In fact, we can derive more on $C=\{\beta\in\mathrm{Ord}\mid \alpha\in\beta\}$.
Define a proper class $A$ is inexhaustible if for every subset $x\subseteq A$ of $A$ there is $y\in A$ such that $y\notin x$. (That is, $A$ is greater than every subset of it.) Classically, every proper class is inexhaustible, but $\mathsf{IZF}$ need not prove it.
We can see that if every set is subcountable (i.e., every set is an image of a subset of $\omega$), then $\mathcal{P}(1)$ is a proper class, but not an inexhaustible class. (It follows from that $\mathcal{P}(1)$ is a double complement of $2$ and no double complement of a set is inexhaustible.) However, the statement 'every set is subcountable' is not consistent with $\mathsf{IZF}$, although it is compatible with $\mathsf{CZF}$.
A slight modification of the previous proof shows $C$ is inexhaustible: let $x\subseteq C$, and take $\gamma:=\bigcup x$. Then we have $\gamma\in C$ but $\gamma\notin x$.
