Theorem cores2

Description: Absorption of a reverse (preimage) restriction of the second member of a class composition. (Contributed by NM, 11-Dec-2006)

	Ref	Expression
Assertion	cores2	$$⊢\mathrm{dom}A\subseteq C\to A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}=A\circ B$$

Proof

Step	Hyp	Ref	Expression
1		dfdm4	$$⊢\mathrm{dom}A=\mathrm{ran}{A}^{-1}$$
2	1	sseq1i	$$⊢\mathrm{dom}A\subseteq C\leftrightarrow \mathrm{ran}{A}^{-1}\subseteq C$$
3		cores	$$⊢\mathrm{ran}{A}^{-1}\subseteq C\to \left({B^{-1}\upharpoonright }_C\right)\circ A^{-1}=B^{-1}\circ A^{-1}$$
4	2 3	sylbi	$$⊢\mathrm{dom}A\subseteq C\to \left({B^{-1}\upharpoonright }_C\right)\circ A^{-1}=B^{-1}\circ A^{-1}$$
5		cnvco	$$⊢{\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}={{\left({B^{-1}\upharpoonright }_C\right)}^{-1}}^{-1}\circ A^{-1}$$
6		cocnvcnv1	$$⊢{{\left({B^{-1}\upharpoonright }_C\right)}^{-1}}^{-1}\circ A^{-1}=\left({B^{-1}\upharpoonright }_C\right)\circ A^{-1}$$
7	5 6	eqtri	$$⊢{\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}=\left({B^{-1}\upharpoonright }_C\right)\circ A^{-1}$$
8		cnvco	$$⊢{\left(A\circ B\right)}^{-1}=B^{-1}\circ A^{-1}$$
9	4 7 8	3eqtr4g	$$⊢\mathrm{dom}A\subseteq C\to {\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}={\left(A\circ B\right)}^{-1}$$
10	9	cnveqd	$$⊢\mathrm{dom}A\subseteq C\to {{\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}}^{-1}={{\left(A\circ B\right)}^{-1}}^{-1}$$
11		relco	$$⊢\mathrm{Rel}\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)$$
12		dfrel2	$$⊢\mathrm{Rel}\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)\leftrightarrow {{\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}}^{-1}=A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}$$
13	11 12	mpbi	$$⊢{{\left(A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}\right)}^{-1}}^{-1}=A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}$$
14		relco	$$⊢\mathrm{Rel}\left(A\circ B\right)$$
15		dfrel2	$$⊢\mathrm{Rel}\left(A\circ B\right)\leftrightarrow {{\left(A\circ B\right)}^{-1}}^{-1}=A\circ B$$
16	14 15	mpbi	$$⊢{{\left(A\circ B\right)}^{-1}}^{-1}=A\circ B$$
17	10 13 16	3eqtr3g	$$⊢\mathrm{dom}A\subseteq C\to A\circ {\left({B^{-1}\upharpoonright }_C\right)}^{-1}=A\circ B$$