Theorem rnxp

Description: The range of a Cartesian product. Part of Theorem 3.13(x) of Monk1 p. 37. (Contributed by NM, 12-Apr-2004)

	Ref	Expression
Assertion	rnxp	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=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	1 3	eqtri	$$⊢\mathrm{ran}\left(A\times B\right)=\mathrm{dom}\left(B\times A\right)$$
5		dmxp	$$⊢A\ne \varnothing \to \mathrm{dom}\left(B\times A\right)=B$$
6	4 5	syl5eq	$$⊢A\ne \varnothing \to \mathrm{ran}\left(A\times B\right)=B$$