# Metamath Proof Explorer

## Theorem dmco

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

Ref Expression
Assertion dmco ${⊢}\mathrm{dom}\left({A}\circ {B}\right)={{B}}^{-1}\left[\mathrm{dom}{A}\right]$

### Proof

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