Theorem idresrnsscocnv2

Description: A class precomposed with its converse includes the identity relation restricted to its range. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	idresrnsscocnv2	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\subseteq A\circ A^{-1}$$

Proof

Step	Hyp	Ref	Expression
1		idresdmsscocnv1	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}{A}^{-1}}\subseteq {A^{-1}}^{-1}\circ A^{-1}$$
2		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
3	2	eqcomi	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A$$
4	3	reseq2i	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{dom}{A}^{-1}}={\mathrm{I}\upharpoonright }_{\mathrm{ran}A}$$
5		cocnvcnv1	$$⊢{A^{-1}}^{-1}\circ A^{-1}=A\circ A^{-1}$$
6	1 4 5	3sstr3i	$$⊢{\mathrm{I}\upharpoonright }_{\mathrm{ran}A}\subseteq A\circ A^{-1}$$