Question: Let $T$ be any set of functions such that any two of them have disjoint domains, that is, $(\forall F)(\forall G)(F \in T \land G \in T \land F \neq G \Rightarrow dom(F) \cap dom(G) = \emptyset)$
Prove that $\bigcup_{F \in T}F$ is a function and that its domain is the union of the domains of the functions in $T$.
The book previous gave the following definition of function too: "By a function we mean a relation $F$ with the aditional property $([(x,y) \in F \land (x,z) \in F] \Rightarrow y=z)$
Here is what I have done:
First let some $t$ and $j$ be elements of $\bigcup_{F \in T}F$, then we have that
$$(\exists Z)(\exists G)(Z \in \bigcup_{F \in T}F \land t \in Z \land G \in \bigcup_{F \in T}F \land j \in G)$$
As $Z$ and $G$ are functions let $t=(x,y)$ and $j=(p,q)$
If we have $Z \neq G$ then $x \notin Dom(G)$ and $p \notin Dom(Z)$ because domain of $Z$ and $G$ are disjoint.
But if $Z=G$ and $x=p$ then $t=(x,y)=(p,q)=j$, because the additional property of function, and in the last possible case if $x \neq p$ we have $[(x,y) \in \bigcup_{F \in T}F \land (p,q) \in \bigcup_{F \in T}F]$ where $(y=q \lor y \neq q)$
Thus for any $(x,y)$ and $(p,q)$ in $\bigcup_{F \in T}F$ we have:
$$[(x,y) \in \bigcup_{F \in T}F \land (p,q) \in \bigcup_{F \in T}F] \Rightarrow [((x,y)=(p,q)) \lor (x \neq p)]$$
And from this we can conclude the union results in a function because:
$$([(x,y) \in \bigcup_{F \in T}F \land (x,z) \in \bigcup_{F \in T}F] \Rightarrow y=z)$$
For the domain part this is what i tried:
$$dom(\bigcup_{F \in T}F) = \{x : (x,y) \in \bigcup_{F \in T}F \}$$
By definition of arbitrary union we have $(x,y) \in \bigcup_{F \in T}F \Leftrightarrow (\exists G)(G \in T \land x \in G)$, thus
$$dom(\bigcup_{F \in T}F) = \{x : (\exists G)(G \in T \land (x,y) \in G) \}$$
But if $(x,y) \in G$ then $x \in dom(G)$
$$dom(\bigcup_{F \in T}F) = \{x : (\exists G)(G \in T \land x \in dom(G)) \}$$ and therefore
$$dom(\bigcup_{F \in T}F) = \bigcup_{F \in T}dom(F)$$
Best Answer
Let me start with a more concise proof.
Proving that $\bigcup_{F\in T}F$ is a function comes to proving that:
Proof of first bullet:
Let $t\in\bigcup_{F\in T}F$. Then $t\in F$ for some $F\in T$ and because $F$ is function we are allowed to conclude that $t$ is an ordered pair.
Proof of second bullet:
Let $(x,y)$ and $(x,z)$ be elements of $\bigcup_{F\in T}F$. Then $F,G\in T$ exist with $(x,y)\in F$ and $(x,z)\in G$. Then $x\in\mathsf{Dom}(F)\cap\mathsf{Dom}(G)$ and from this we are allowed to conclude that $F=G$. Then we can draw the conclusion that $y=z$ since $F=G$ is a function.
The following statements are equivalent:
This for every $x$ so that we can conclude that: $$\mathsf{Dom}(\bigcup_{F\in T}F)=\bigcup_{F\in T}\mathsf{Dom}(F)$$