It is possible to make a set that contains all the set except itself, operationally this pretty simple, I am working on creating a language programming based on set theory, so this will be an easy way to define some notion of universal set.
If you aren’t aware of it already, you might be interested to read about Russell’s paradox [1] which shows a problem with allowing sets to be defined into existence without restriction (making Frege’s life’s work the Grundgesetze stillborn). It involves using the “set” of all things that are not a member of themselves.
Unfortunately the set that contains all sets except itself doesn't exist either. If such a set X existed, then you could easily build X unioned with {X}, which would be the set of all sets, which doesn't exist. You can't really avoid Russel's paradox, it prevents you from being able to make a set that is basically all sets, minus some exceptions.
But there is a way to get around Russel's paradox, the standard way is to define a new kind of object called a class. See https://en.wikipedia.org/wiki/Class_(set_theory) . Basically a class is like a set, a set can be a member of a class, and you can do most operations with sets on classes as well (union, intersection, etc). And you can create a class which is all sets satisfying some property. From this you can't have a set of all sets, but you can have a class of all sets. Russel's paradox doesn't go away, you still can't have the set of all sets (and you can't have the class of all classes), but this still gives you enough to talk about properties of all sets. See https://en.wikipedia.org/wiki/Von_Neumann%E2%80%93Bernays%E2... for an example of how to define classes. That particular example is a conservative extension of ZFC: any statement about sets that can be proved using NBG can also be proved using ZFC and vice versa (assuming ZFC is consistent). Your statement can't involve classes, because there is no definition of classes in ZFC so it wouldn't translate, but your proof in the NBG system can make use of it
fn contain(u0:(universal, set), u1:(universal, set)){ return false }
fn contain(u:(universal, set), s:set){ return true }
but don't how much logical sense it will make