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	⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵

Proof

Step	Hyp	Ref	Expression
1		df-rn	⊢ ran ( 𝐴 × 𝐵 ) = dom ◡ ( 𝐴 × 𝐵 )
2		cnvxp	⊢ ◡ ( 𝐴 × 𝐵 ) = ( 𝐵 × 𝐴 )
3	2	dmeqi	⊢ dom ◡ ( 𝐴 × 𝐵 ) = dom ( 𝐵 × 𝐴 )
4		dmxpss	⊢ dom ( 𝐵 × 𝐴 ) ⊆ 𝐵
5	3 4	eqsstri	⊢ dom ◡ ( 𝐴 × 𝐵 ) ⊆ 𝐵
6	1 5	eqsstri	⊢ ran ( 𝐴 × 𝐵 ) ⊆ 𝐵