This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 (A \times B) \subseteq B$

Proof

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