Theorem unidmrn

Description: The double union of the converse of a class is its field. (Contributed by NM, 4-Jun-2008)

	Ref	Expression
Assertion	unidmrn	$$⊢\bigcup \bigcup A^{-1}=\mathrm{dom}A\cup \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{A}^{-1}$$
2		relfld	$$⊢\mathrm{Rel}{A}^{-1}\to \bigcup \bigcup A^{-1}=\mathrm{dom}{A}^{-1}\cup \mathrm{ran}{A}^{-1}$$
3	1 2	ax-mp	$$⊢\bigcup \bigcup A^{-1}=\mathrm{dom}{A}^{-1}\cup \mathrm{ran}{A}^{-1}$$
4	3	equncomi	$$⊢\bigcup \bigcup A^{-1}=\mathrm{ran}{A}^{-1}\cup \mathrm{dom}{A}^{-1}$$
5		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
6		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
7	5 6	uneq12i	$$⊢\mathrm{dom}A\cup \mathrm{ran}A=\mathrm{ran}{A}^{-1}\cup \mathrm{dom}{A}^{-1}$$
8	4 7	eqtr4i	$$⊢\bigcup \bigcup A^{-1}=\mathrm{dom}A\cup \mathrm{ran}A$$