Theorem bj-cnvresrn

Description: Duplicate of cnvresrn , to be moved to the main section. The converse restricted to the range is equal to the converse. Analogue of resdmb since a converse is always a relation ( relcnv ). (Contributed by Peter Mazsa, 3-Sep-2021) Can shorten domss2 .

	Ref	Expression
Assertion	bj-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		resdmb	$$⊢\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}$$