And the idea in the context of the original post is that this is supposed to be a parody of a formal math definition in a paper or textbook (using Jabberwocky vocabulary instead of real math vocabulary).

Not that it makes sense anyway. Somehow 𝑈⊆𝑋 and 𝑈∈𝑋.

No, the point was that 𝑈∈𝑋 is a typo and 𝑈⊆𝑋 is what was intended. Type theory will reject the mistake but set theory will accept it. This is then presented as a reason why mathematicians should prefer type-theory-based proof assistants to set-theory-based ones, since the former will catch these kinds of mistakes while the later won't.

That is exactly the point being made. That you can spot right away that something "doesn't make sense".

That’s possible. For instance, X = {{}} and U = {}. Or in general, if X_0 = {} and X_{i+1} = {X_0, ..., X_i}, then X_i is both an element and a subset of X_j whenever i < j.

That happens all the time with ordinals.