Theorem dmco

Description: The domain of a composition. Exercise 27 of Enderton p. 53. (Contributed by NM, 4-Feb-2004)

	Ref	Expression
Assertion	dmco	$$⊢\mathrm{dom}\left(A\circ B\right)=B^{-1}\left[\mathrm{dom}A\right]$$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}\left(A\circ B\right)=\mathrm{ran}{\left(A\circ B\right)}^{-1}$$
2		cnvco	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$
3	2	rneqi	$$⊢\mathrm{ran}{\left(A\circ B\right)}^{-1}=\mathrm{ran}\left(B^{-1}\circ A^{-1}\right)$$
4		rnco2	$$⊢\mathrm{ran}\left(B^{-1}\circ A^{-1}\right)=B^{-1}\left[\mathrm{ran}{A}^{-1}\right]$$
5		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
6	5	imaeq2i	$$⊢B^{-1}\left[\mathrm{dom}A\right]=B^{-1}\left[\mathrm{ran}{A}^{-1}\right]$$
7	4 6	eqtr4i	$$⊢\mathrm{ran}\left(B^{-1}\circ A^{-1}\right)=B^{-1}\left[\mathrm{dom}A\right]$$
8	1 3 7	3eqtri	$$⊢\mathrm{dom}\left(A\circ B\right)=B^{-1}\left[\mathrm{dom}A\right]$$