Theorem rncoss

Description: Range of a composition. (Contributed by NM, 19-Mar-1998)

	Ref	Expression
Assertion	rncoss	$$⊢\mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{ran}A$$

Proof

Step	Hyp	Ref	Expression
1		dmcoss	$$⊢\mathrm{dom}\left(B^{-1}\circ A^{-1}\right)\subseteq \mathrm{dom}{A}^{-1}$$
2		df-rn	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{dom}{\left(A\circ B\right)}^{-1}$$
3		cnvco	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$
4	3	dmeqi	$$⊢\mathrm{dom}{\left(A\circ B\right)}^{-1}=\mathrm{dom}\left(B^{-1}\circ A^{-1}\right)$$
5	2 4	eqtri	$$⊢\mathrm{ran}\left(A\circ B\right)=\mathrm{dom}\left(B^{-1}\circ A^{-1}\right)$$
6		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
7	1 5 6	3sstr4i	$$⊢\mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{ran}A$$