Theorem rncoss

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

	Ref	Expression
Assertion	rncoss	|- ran ( A o. B ) C_ ran A

Proof

Step	Hyp	Ref	Expression
1		dmcoss	|- dom ( `' B o. `' A ) C_ dom `' A
2		df-rn	|- ran ( A o. B ) = dom `' ( A o. B )
3		cnvco	|- `' ( A o. B ) = ( `' B o. `' A )
4	3	dmeqi	|- dom `' ( A o. B ) = dom ( `' B o. `' A )
5	2 4	eqtri	|- ran ( A o. B ) = dom ( `' B o. `' A )
6		df-rn	|- ran A = dom `' A
7	1 5 6	3sstr4i	|- ran ( A o. B ) C_ ran A