Proving the inverse of a relation exists A relation is a set of ordered pairs $(x,y)$ that relates $x$ to $y$ somehow. It's a very weak relation in the sense one thing can be related to many things. A function is a special relation where each thing in the domain is related to only one thing in the image. 
$xRy\iff(x,y)\in R$
Given a relation $R$ the inverse, $R^{-1}$ is "given by" $\{(y,x)|(x,y)\in R\}$
$\text{Dom}(R)=\{x|\exists y:xRy\}$
$\text{Ran}(R)=\{y|\exists x:xRy\}$
My problem is I cannot prove these three sets (inverse, domain and range) exist.

What have I tried?
If I write $\{x|P(x)\}$ where $P$ is some property of $x$ to show it exists I must find a set $A$ that exists, where $P(x)\implies x\in A$ - then this is (uniquely) the set $\{x\in A|P(x)\}$ - obviously the choice of $A$ isn't unique.
So I need to find a set $A$ such that $P((x,y),R)\implies (x,y)\in A$ where $P((x,y),R)$ is $(x,y)\in R$
Regarding domain (range will be essentially the same) I am having trouble building a set which contains the first thing in the ordered pairs that make up the relation - I don't have cardinality yet so I am not sure what "property" to formulate to extract them.

The Axioms I have so far:


*

*Axiom of existence: there exists a set with no elements

*Axiom of extensionality (equality basically?): if two sets have the same elements they are identical

*Lemma showing the empty set is unique

*Axiom of schema of comprehension: $\{x\in A|P(x)\}$ exists where P is a property.

*Lemma showing the set given in the comprehension axiom is unique (justifying my notation)

*Axiom of a pair: for any A, B there is a set C such that $x\in C\iff[x\in A\text{ or }x\in B]$

*Axiom of union, given a set $S$, $x\in\cup S\iff\exists A\in S:x\in A$

*Axiom of power set - I think the key is here


I am looking for a very rigorous answer 
 A: Mission Prove the existence of the inverse relation given only axioms of Set Theory
Axioms The axioms we will assume are the ones you posted. That is to say, the axioms we assume are


*

*Axiom of set existence

*Axiom of extensionality

*Axiom (schema) of specification

*Axiom of pairing

*Axiom of union

*Axiom of power


Ordered Pairs We define ordered pairs
Notation Let $X$ be a nonempty set. Let $x,y\in X$. "$\{x,y\}$" is notation for "$\{z\in X:z=x\,\vee\, z=y\}$." "$\{x\}$" is notation for "$\{ x,x \}$."
Definition Let $X$ be a nonempty set. Let $x,y\in X$. The ordered pair with first coordinate $x$ and second coordinate $y$ is $\{ \{x\},\{x,y\} \}$.
Notation Let $X$ be a nonempty set. Let $x,y\in X$. "$ (x,y)$" is notation for "ordered pair with first coordinate $x$ and second coordinate $y$."
Remark Let $X$ be a nonempty set. Let $x,y,u,v\in X$. If $(x,y)=(u,v)$, then $x=u$ and $y=v$.
Cartesian Products We define Cartesian products
Proposition For all sets $A$ and $B$, there exists a unique set whose elements are exactly those elements $(a,b)$ such that $a\in A$ and $b\in B$.
Proof Let $A$ and $B$ be arbitrary sets. Define $V\overset{\mathrm{def}}{=} \left\{\mathcal{X}\in \mathcal{P}(\mathcal{P}(A\cup B)):\exists a\in A,\exists b\in B[\mathcal{X}=(a,b)]  \right\}$. Therefore $V$ is a set whose elements are exactly those elements $(a,b)$ such that $a\in A$ and $b\in B$. By the axiom of extensionality, $V$ is unique.$\qquad\square$
Definition Let $A$ and $B$ be sets. The Cartesian product of $A$ and $B$ is the set whose elements are exactly those elements $(a,b)$ such that $a\in A$ and $b\in B$.
Notation Let $A$ and $B$ be sets. $A\times B$ is notation for "Cartesian product of $A$ and $B$."
Existence



[Sorry for posting pictures; I prefer to typeset in my LaTeX editor \newcommands + autocompletion. If you're up to the challenge, please update my post by replacing the pictures with genuine code]
A: Each ordered pair $\langle x,y\rangle\in R$ is actually a set of the form $\{\{x\},\{x,y\}\}$. Recall that $x\in\bigcup y$ if and only if there is a $z\in y$ such that $x\in z$. Thus, the elements of $\bigcup R$ are sets of the form $\{x\}$ and $\{x,y\}$ for the ordered pairs $\langle x,y\rangle\in R$, and the elements of $\bigcup\bigcup R$ are elements of the underlying set for the relation. Specifically:
$$\begin{align*}
\operatorname{dom}R&=\left\{x\in\bigcup\bigcup R:\exists y\in\bigcup\bigcup R\big(\langle x,y\rangle\in R\big)\right\}\\
\operatorname{ran}R&=\left\{y\in\bigcup\bigcup R:\exists x\in\bigcup\bigcup R\big(\langle x,y\rangle\in R\big)\right\}\;,\text{ and}\\
R^{-1}&=\left\{\langle y,x\rangle\in\left(\bigcup\bigcup R\right)\times\left(\bigcup\bigcup R\right):\langle x,y\rangle\in R\right\}\;.
\end{align*}\tag{1}$$
In each case it’s clear that the sets that I’ve defined exist, via the union axiom and comprehension schema. (I am assuming that if you have ordered pairs, you have Cartesian products.) It’s also clear that they are at least subsets of what they purport to be, e.g., that everything in my definition of the domain of $R$ actually is in what we think of as the domain of $R$. The only thing that might still be open to question is whether these definitions actually pick up everything that they ought to pick up, but the introductory comments cover that. If, for example, $\langle x,y\rangle\in R$, then $\{x,y\}\in\bigcup R$, so $x,y\in\bigcup\bigcup R$, and the definitions in $(1)$ really do pick up $x$ in $\operatorname{dom}R$, $y\in\operatorname{ran}R$, and $\langle y,x\rangle$ in $R^{-1}$.
