Theorem rnun

Description: Distributive law for range over union. Theorem 8 of Suppes p. 60. (Contributed by NM, 24-Mar-1998)

	Ref	Expression
Assertion	rnun	$$⊢\mathrm{ran}\left(A\cup B\right)=\mathrm{ran}A\cup \mathrm{ran}B$$

Proof

Step	Hyp	Ref	Expression
1		cnvun	$$⊢{\left(A\cup B\right)}^{-1}=A^{-1}\cup B^{-1}$$
2	1	dmeqi	$$⊢\mathrm{dom}{\left(A\cup B\right)}^{-1}=\mathrm{dom}\left(A^{-1}\cup B^{-1}\right)$$
3		dmun	$$⊢\mathrm{dom}\left(A^{-1}\cup B^{-1}\right)=\mathrm{dom}{A}^{-1}\cup \mathrm{dom}{B}^{-1}$$
4	2 3	eqtri	$$⊢\mathrm{dom}{\left(A\cup B\right)}^{-1}=\mathrm{dom}{A}^{-1}\cup \mathrm{dom}{B}^{-1}$$
5		df-rn	$$⊢\mathrm{ran}\left(A\cup B\right)=\mathrm{dom}{\left(A\cup B\right)}^{-1}$$
6		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
7		df-rn	$$⊢\mathrm{ran}B=\mathrm{dom}{B}^{-1}$$
8	6 7	uneq12i	$$⊢\mathrm{ran}A\cup \mathrm{ran}B=\mathrm{dom}{A}^{-1}\cup \mathrm{dom}{B}^{-1}$$
9	4 5 8	3eqtr4i	$$⊢\mathrm{ran}\left(A\cup B\right)=\mathrm{ran}A\cup \mathrm{ran}B$$