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\times \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)\times \mathrm{ran}\left(A\circ B\right)$$
3	1 2	ax-mp	$$⊢A\circ B\subseteq \mathrm{dom}\left(A\circ B\right)\times \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)\times \mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{dom}B\times \mathrm{ran}A$$
7	4 5 6	mp2an	$$⊢\mathrm{dom}\left(A\circ B\right)\times \mathrm{ran}\left(A\circ B\right)\subseteq \mathrm{dom}B\times \mathrm{ran}A$$
8	3 7	sstri	$$⊢A\circ B\subseteq \mathrm{dom}B\times \mathrm{ran}A$$