Theorem relfld

Description: The double union of a relation is its field. (Contributed by NM, 17-Sep-2006)

	Ref	Expression
Assertion	relfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$

Proof

Step	Hyp	Ref	Expression
1		relssdmrn	$$⊢\mathrm{Rel}R\to R\subseteq \mathrm{dom}R\times \mathrm{ran}R$$
2		uniss	$$⊢R\subseteq \mathrm{dom}R\times \mathrm{ran}R\to \bigcup R\subseteq \bigcup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
3		uniss	$$⊢\bigcup R\subseteq \bigcup \left(\mathrm{dom}R\times \mathrm{ran}R\right)\to \bigcup \bigcup R\subseteq \bigcup \bigcup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
4	1 2 3	3syl	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R\subseteq \bigcup \bigcup \left(\mathrm{dom}R\times \mathrm{ran}R\right)$$
5		unixpss	$$⊢\bigcup \bigcup \left(\mathrm{dom}R\times \mathrm{ran}R\right)\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
6	4 5	sstrdi	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R\subseteq \mathrm{dom}R\cup \mathrm{ran}R$$
7		dmrnssfld	$$⊢\mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R$$
8	7	a1i	$$⊢\mathrm{Rel}R\to \mathrm{dom}R\cup \mathrm{ran}R\subseteq \bigcup \bigcup R$$
9	6 8	eqssd	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$