Axioms and Ordinals, Replacement

Replacement

the image of a set under a formula lies in another set. Let f be a formula in logic such that x and y are free variables, and r is not a free variable. Restrict x to a set d, the domain, and assume f(x) is a function, i.e. there is only one y satisfying f(x,y). The range of the function is also a set.

Like comprehension, this is an axiom scheme. It represents an axiom for each domain and function.

all d,f { all x in d { unique y { f(x,y) }} then
some r { all x,y { x ∈ d and f(x,y) then y ∈ r }}}

Use comprehension to restrict the set r to the range of the function. Now the domain and range are sets, and as an added bonus, f is also a set, a restriction of d cross r.

We can set the power set axiom aside and build the cross product of two sets using replacement. Fix x from the first set and map every y in the second set to ((x),(x,y)). Thus there is a set containing all the ordered pairs based on x. Now equate each x in the first set with its set of ordered pairs. Invoke replacement again, and there is a set of sets of ordered pairs, one set of ordered pairs for each x. Take the union to get the set of all ordered pairs, thus building the relation.