Theorem rnxpss

Description: The range of a Cartesian product is included in its second factor. (Contributed by NM, 16-Jan-2006) (Proof shortened by Andrew Salmon, 27-Aug-2011)

	Ref	Expression
Assertion	rnxpss	$$⊢\mathrm{ran}\left(A\times B\right)\subseteq B$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}\left(A\times B\right)=\mathrm{dom}{\left(A\times B\right)}^{-1}$$
2		cnvxp	$$⊢{\left(A\times B\right)}^{-1}=B\times A$$
3	2	dmeqi	$$⊢\mathrm{dom}{\left(A\times B\right)}^{-1}=\mathrm{dom}\left(B\times A\right)$$
4		dmxpss	$$⊢\mathrm{dom}\left(B\times A\right)\subseteq B$$
5	3 4	eqsstri	$$⊢\mathrm{dom}{\left(A\times B\right)}^{-1}\subseteq B$$
6	1 5	eqsstri	$$⊢\mathrm{ran}\left(A\times B\right)\subseteq B$$