Theorem cnvresrn

Description: Converse restricted to range is converse. (Contributed by Peter Mazsa, 3-Sep-2021)

	Ref	Expression
Assertion	cnvresrn	$$⊢{R^{-1}\upharpoonright }_{\mathrm{ran}R}=R^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}R=\mathrm{dom}{R}^{-1}$$
2	1	reseq2i	$$⊢{R^{-1}\upharpoonright }_{\mathrm{ran}R}={R^{-1}\upharpoonright }_{\mathrm{dom}{R}^{-1}}$$
3		relcnv	$$⊢\mathrm{Rel}{R}^{-1}$$
4		dfrel5	$$⊢\mathrm{Rel}{R}^{-1}\leftrightarrow {R^{-1}\upharpoonright }_{\mathrm{dom}{R}^{-1}}=R^{-1}$$
5	3 4	mpbi	$$⊢{R^{-1}\upharpoonright }_{\mathrm{dom}{R}^{-1}}=R^{-1}$$
6	2 5	eqtri	$$⊢{R^{-1}\upharpoonright }_{\mathrm{ran}R}=R^{-1}$$