Theorem dmco

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

	Ref	Expression
Assertion	dmco	|- dom ( A o. B ) = ( `' B " dom A )

Proof

Step	Hyp	Ref	Expression
1		dfdm4	|- dom ( A o. B ) = ran `' ( A o. B )
2		cnvco	|- `' ( A o. B ) = ( `' B o. `' A )
3	2	rneqi	|- ran `' ( A o. B ) = ran ( `' B o. `' A )
4		rnco2	|- ran ( `' B o. `' A ) = ( `' B " ran `' A )
5		dfdm4	|- dom A = ran `' A
6	5	imaeq2i	|- ( `' B " dom A ) = ( `' B " ran `' A )
7	4 6	eqtr4i	|- ran ( `' B o. `' A ) = ( `' B " dom A )
8	1 3 7	3eqtri	|- dom ( A o. B ) = ( `' B " dom A )