Theorem rncocnv1

Description: The range of a class postcomposed with its converse is equal to its domain. (Contributed by BJ, 25-Oct-2026)

	Ref	Expression
Assertion	rncocnv1	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}A=\mathrm{dom}{A}^{-1}$$
2	1	eqcomi	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A$$
3		rncoeq	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A\to \mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{ran}{A}^{-1}$$
4	2 3	ax-mp	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{ran}{A}^{-1}$$
5		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
6	4 5	eqtr4i	$$⊢\mathrm{ran}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$