In Tao's Analysis I, one of the ways that a function can be described is as follows:
$f: X \to Y$
$f: x \mapsto f(x) = \text{ specific rule }$ (e.g. $f(x) = 2x$)
That is to say, a function can be sufficiently described by providing a domain, codomain, and a specific mapping rule.
While working through book exercises, I am running into situations where I do not yet know if a desired codomain is actually a set, and therefore I am reluctant to define functions that would otherwise help me with proofs.
For example, let's say that I need to prove some set $Y$ exists (i.e. at the start, I do not know if $Y$ is a set), but I know that all "would-be" elements of $Y$, as individual objects, certainly exist. There are times where it would be very useful for me to describe functions that map elements of a known set $X$ to these "extant" would-be elements of $Y$. However, in order to use this function, I first need to know that $Y$ exists as a set; otherwise, I do not have a codomain and cannot define the function!
From what I understand about ZFC axioms, I don't think I can just take an infinite collection of objects I know exist and slap on two surrounding set brackets and claim, "Voilia! This is a set!" (I think one can carry this out on finite collections of objects, however, by using the union axiom and the singleton & pair set axioms).
At first, I was tempted into thinking that I could just take some sort of "superset" that definitely contains these would-be elements of $Y$. However, after reading up on Cantor's theorem and Russel's paradox, I realize this strategy won't work (e.g. if my superset was defined as "the set of all sets").
Any help would be greatly appreciated!