Theorem dmcocnv1

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

	Ref	Expression
Assertion	dmcocnv1	$$⊢\mathrm{dom}\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		dmcoeq	$$⊢\mathrm{dom}{A}^{-1}=\mathrm{ran}A\to \mathrm{dom}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$
4	2 3	ax-mp	$$⊢\mathrm{dom}\left(A^{-1}\circ A\right)=\mathrm{dom}A$$