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

Metamath Proof Explorer

Theorem cnvssrndm

Description: The converse is a subset of the cartesian product of range and domain. (Contributed by Mario Carneiro, 2-Jan-2017)

		Ref	Expression
	Assertion	cnvssrndm	$⊢ A^{-1} \subseteq ran A \times dom A$

Step	Hyp	Ref	Expression
1		relcnv	$⊢ Rel A^{-1}$
2		relssdmrn	$⊢ Rel A^{-1} \to A^{-1} \subseteq dom A^{-1} \times ran A^{-1}$
3	1 2	ax-mp	$⊢ A^{-1} \subseteq dom A^{-1} \times ran A^{-1}$
4		df-rn	$⊢ ran A = dom A^{-1}$
5		dfdm4	$⊢ dom A = ran A^{-1}$
6	4 5	xpeq12i	$⊢ ran A \times dom A = dom A^{-1} \times ran A^{-1}$
7	3 6	sseqtrri	$⊢ A^{-1} \subseteq ran A \times dom A$