Theorem relcnvfld

Description: if R is a relation, its double union equals the double union of its converse. (Contributed by FL, 5-Jan-2009)

	Ref	Expression
Assertion	relcnvfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\bigcup \bigcup R^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		relfld	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\mathrm{dom}R\cup \mathrm{ran}R$$
2		unidmrn	$$⊢\bigcup \bigcup R^{-1}=\mathrm{dom}R\cup \mathrm{ran}R$$
3	1 2	eqtr4di	$$⊢\mathrm{Rel}R\to \bigcup \bigcup R=\bigcup \bigcup R^{-1}$$