Theorem cnvco1

Description: Another distributive law of converse over class composition. (Contributed by Scott Fenton, 3-May-2014)

	Ref	Expression
Assertion	cnvco1	$$⊢{\left(A^{-1}\circ B\right)}^{-1}=B^{-1}\circ A$$

Proof

Step	Hyp	Ref	Expression
1		relcnv	$$⊢\mathrm{Rel}{\left(A^{-1}\circ B\right)}^{-1}$$
2		relco	$$⊢\mathrm{Rel}\left(B^{-1}\circ A\right)$$
3		vex	$$⊢z\in \mathrm{V}$$
4		vex	$$⊢y\in \mathrm{V}$$
5	3 4	brcnv	$$⊢z{B}^{-1}y\leftrightarrow yBz$$
6	5	bicomi	$$⊢yBz\leftrightarrow z{B}^{-1}y$$
7		vex	$$⊢x\in \mathrm{V}$$
8	3 7	brcnv	$$⊢z{A}^{-1}x\leftrightarrow xAz$$
9	6 8	anbi12ci	$$⊢\left(yBz\wedge z{A}^{-1}x\right)\leftrightarrow \left(xAz\wedge z{B}^{-1}y\right)$$
10	9	exbii	$$⊢\exists z\left(yBz\wedge z{A}^{-1}x\right)\leftrightarrow \exists z\left(xAz\wedge z{B}^{-1}y\right)$$
11	7 4	opelcnv	$$⊢⟨x,y⟩\in {\left(A^{-1}\circ B\right)}^{-1}\leftrightarrow ⟨y,x⟩\in \left(A^{-1}\circ B\right)$$
12	4 7	opelco	$$⊢⟨y,x⟩\in \left(A^{-1}\circ B\right)\leftrightarrow \exists z\left(yBz\wedge z{A}^{-1}x\right)$$
13	11 12	bitri	$$⊢⟨x,y⟩\in {\left(A^{-1}\circ B\right)}^{-1}\leftrightarrow \exists z\left(yBz\wedge z{A}^{-1}x\right)$$
14	7 4	opelco	$$⊢⟨x,y⟩\in \left(B^{-1}\circ A\right)\leftrightarrow \exists z\left(xAz\wedge z{B}^{-1}y\right)$$
15	10 13 14	3bitr4i	$$⊢⟨x,y⟩\in {\left(A^{-1}\circ B\right)}^{-1}\leftrightarrow ⟨x,y⟩\in \left(B^{-1}\circ A\right)$$
16	1 2 15	eqrelriiv	$$⊢{\left(A^{-1}\circ B\right)}^{-1}=B^{-1}\circ A$$