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 \mathrm{ran}A\times \mathrm{dom}A$$

Proof

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