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 \circ B) = B^{-1} [dom A]$

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

Metamath Proof Explorer