Theorem rncoeq

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

	Ref	Expression
Assertion	rncoeq	|- ( dom A = ran B -> ran ( A o. B ) = ran A )

Proof

Step	Hyp	Ref	Expression
1		dmcoeq	|- ( dom `' B = ran `' A -> dom ( `' B o. `' A ) = dom `' A )
2		eqcom	|- ( dom A = ran B <-> ran B = dom A )
3		df-rn	|- ran B = dom `' B
4		dfdm4	|- dom A = ran `' A
5	3 4	eqeq12i	|- ( ran B = dom A <-> dom `' B = ran `' A )
6	2 5	bitri	|- ( dom A = ran B <-> dom `' B = ran `' A )
7		df-rn	|- ran ( A o. B ) = dom `' ( A o. B )
8		cnvco	|- `' ( A o. B ) = ( `' B o. `' A )
9	8	dmeqi	|- dom `' ( A o. B ) = dom ( `' B o. `' A )
10	7 9	eqtri	|- ran ( A o. B ) = dom ( `' B o. `' A )
11		df-rn	|- ran A = dom `' A
12	10 11	eqeq12i	|- ( ran ( A o. B ) = ran A <-> dom ( `' B o. `' A ) = dom `' A )
13	1 6 12	3imtr4i	|- ( dom A = ran B -> ran ( A o. B ) = ran A )