Theorem cocnvcnv1

Description: A composition is not affected by a double converse of its first argument. (Contributed by NM, 8-Oct-2007)

	Ref	Expression
Assertion	cocnvcnv1	$$⊢{A^{-1}}^{-1}\circ B=A\circ B$$

Proof

Step	Hyp	Ref	Expression
1		cnvcnv2	$$⊢{A^{-1}}^{-1}={A\upharpoonright }_{\mathrm{V}}$$
2	1	coeq1i	$$⊢{A^{-1}}^{-1}\circ B=\left({A\upharpoonright }_{\mathrm{V}}\right)\circ B$$
3		ssv	$$⊢\mathrm{ran}B\subseteq \mathrm{V}$$
4		cores	$$⊢\mathrm{ran}B\subseteq \mathrm{V}\to \left({A\upharpoonright }_{\mathrm{V}}\right)\circ B=A\circ B$$
5	3 4	ax-mp	$$⊢\left({A\upharpoonright }_{\mathrm{V}}\right)\circ B=A\circ B$$
6	2 5	eqtri	$$⊢{A^{-1}}^{-1}\circ B=A\circ B$$