"Infimal depth" of a set Consider the following simple facts about the powerset and union operators:

Statement 1. for any $X$: $X \subset \operatorname{P} \bigcup X $
Statement 2. (generalized version): for any $X$, $X \subset \underbrace{\operatorname{P} \cdots \operatorname{P}}_{n}\underbrace{\bigcup \cdots \bigcup}_{n} X $

These are relatively easy to prove in set theories that have no urelements, but turn out to be false in a universe that has urelements. Indeed, if $\ast$ is any urelement, and $X = \{\ast\}$, then $\bigcup X$ is empty (I beleive this is correct, since $\bigcup X = \{y : y \in x \in X \text{, for some } x\}$, and this definition makes sense even if $X$ contains an urelement). Thus $\{\ast\} = X \not\subset \operatorname P \bigcup X = \operatorname P \varnothing = \{\varnothing\}$
So, in order to make the above statements true, we need some extra condition:

Statement 1a. (amended for a universe with urelements): if $X$ is a set that has no urelements, then $X \subset \operatorname{P} \bigcup X $.

For the generalized version, we need something like the following

Definition (infimal depth): for any set $X$, the infimal depth of $X$, denoted here by $\operatorname{ID}(X)$, is the infimum of the length $n$ of maximal chains $X \ni x_1 \ni x_2 \ni \cdots \ni x_n$ that can be formed with any $x_i$'s, "ending" in an urelement (so only those chains are considered where $x_n$ is not a set but an urelement).

Some notes:

*

*we can assume the axiom of regularity, so that all the chains above will have finite length; but maybe this is not even required;

*a maximal chain starting from an urelement of $X$ always has length 1, so if $X$ contains an urelement, then $\operatorname{ID}(X) = 1$.

*$\operatorname{ID}(\varnothing) = +\infty$ (because no such chains exist, so the infimum ranges over an empty set).

*in addition, any set that hereditarily contains no urelements, also has infimal depth $+\infty$;

*it seems possible and useful to technically extend the definition with $\operatorname{ID}(\ast) = 0$ (instead of $+\infty$) for any urelement $\ast$.

(if this definition is problematic for some reason, a variant can be formed inductively, starting with 0 for urelements, and then taking the infimum ranging over the elements of $X$, plus 1)
With this, the general statement becomes (hopefully):

Statement 2a. (amended for a universe with urelements) for any $X$, if $\operatorname{ID}(X) \geq n $, then $X \subset \underbrace{\operatorname{P} \cdots \operatorname{P}}_{n}\underbrace{\bigcup \cdots \bigcup}_{n} X$

This is truly a generalization of (2) in the following sense: in a universe where there is no urelement,everything is a set and all sets have infimal depth $+\infty$, so the extra condition is inherently true, thus not required at all, and we are back to (2).
I searched for something like the "infimal depth", etc., but found nothing along these lines. Usually the rank / type / depth of a set is similar, but "measures" the supremum, not the infimum and that is of no use here.
So my question is: is there a name for this "infimal depth" (what then?); has this been studied somewhere (where?), or is there something fundamentally flawed above?
 A: Rather than an answer to the main question this is an answer to the comments:

$x⊆\bigcup X$ means $x∈\mathcal{P}(\bigcup X)$

This heavily depends on your definition of $⊆$, $∈$ and $\mathcal{P}$ in ZFA(ZF+urelements).
In ZF we can define $a⊆b$ as $∀x(x∈a⇒x∈b)$, which vacuously make the $\emptyset$ be a subset of every set there is, but if you allow urelements, then the naive approach will make it so that every urelement will be a subset of every set, like the empty set, in this case, the class of urelements will be a subclass of the powerset of every set.
In this case, the proof doesn't fail at all, because $\{\ast\} = X \subseteq \mathcal P( \bigcup X) = \mathcal P(\emptyset)= \{\varnothing\}∪\mbox{the class of urelements}$.
Another, more common, approach is to change the definition of powerset of $X$ to be "the class of $a⊆X$ such that $a$ is a set", and modify the powerset axiom accordingly, in that case $x⊆\bigcup X⇒x∈\mathcal{P}(\bigcup X)$ is false and the proof fails there.
You can also add new predicate $S$ such that $S(x)⇔x$ is a set, and change the definition of $a⊆b$ to $S(a)∧∀x(x∈a⇒x∈b)$, in that case "$x \in X \implies x ⊆ \bigcup X$" is false, because $x$ need not be a set.
Or you can work with 2-sorted logic, and completely disallowing the sentence $a∈b$ for $b$ urelement, in this case $x⊆y$ makes no sense for $x$ or $y$ urelements and you again need to restrict yourself to sets only.
