# Metamath Proof Explorer

## Theorem cossxp

Description: Composition as a subset of the Cartesian product of factors. (Contributed by Mario Carneiro, 12-Jan-2017)

Ref Expression
Assertion cossxp ${⊢}{A}\circ {B}\subseteq \mathrm{dom}{B}×\mathrm{ran}{A}$

### Proof

Step Hyp Ref Expression
1 relco ${⊢}\mathrm{Rel}\left({A}\circ {B}\right)$
2 relssdmrn ${⊢}\mathrm{Rel}\left({A}\circ {B}\right)\to {A}\circ {B}\subseteq \mathrm{dom}\left({A}\circ {B}\right)×\mathrm{ran}\left({A}\circ {B}\right)$
3 1 2 ax-mp ${⊢}{A}\circ {B}\subseteq \mathrm{dom}\left({A}\circ {B}\right)×\mathrm{ran}\left({A}\circ {B}\right)$
4 dmcoss ${⊢}\mathrm{dom}\left({A}\circ {B}\right)\subseteq \mathrm{dom}{B}$
5 rncoss ${⊢}\mathrm{ran}\left({A}\circ {B}\right)\subseteq \mathrm{ran}{A}$
6 xpss12 ${⊢}\left(\mathrm{dom}\left({A}\circ {B}\right)\subseteq \mathrm{dom}{B}\wedge \mathrm{ran}\left({A}\circ {B}\right)\subseteq \mathrm{ran}{A}\right)\to \mathrm{dom}\left({A}\circ {B}\right)×\mathrm{ran}\left({A}\circ {B}\right)\subseteq \mathrm{dom}{B}×\mathrm{ran}{A}$
7 4 5 6 mp2an ${⊢}\mathrm{dom}\left({A}\circ {B}\right)×\mathrm{ran}\left({A}\circ {B}\right)\subseteq \mathrm{dom}{B}×\mathrm{ran}{A}$
8 3 7 sstri ${⊢}{A}\circ {B}\subseteq \mathrm{dom}{B}×\mathrm{ran}{A}$