So basically, I need to think whether the quantified "operator" (encoded as a ZF function) has a domain that's too big to be a set
I think you need to think that TLA+ only implements a part of ZFC and doesn't allow you to quantify over
variables that you will use to "operate" over something.
When you are in doubt with a formal system, look at the formal definition of its syntax and at its system
of axioms and inference rules.
--
FL