refactor(set_theory/zfc): `Union` → `sUnion` (#15352)
The current `Union` definitions more closely match `set.sUnion`. We also change the notation to match.
See [Zulip](https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/ZFC.20definable.20class/near/289406692).
